GitPlanet

Cheap and reliable Node.js hosting starts at $3/month, and $1/month static HTML hosting

Created with love in Canada, visit hostnodejs.com today

Feel like to post an Ad? Learn Details
All Projects → newca12 → awesome-rust-formalized-reasoning

newca12 / awesome-rust-formalized-reasoning

Licence: MIT license
An exhaustive list of all Rust resources regarding automated or semi-automated formalization efforts in any area, constructive mathematics, formal algorithms, and program verification.

Labels

logictheorem-provingformal-verificationproverautomated-theorem-proversreasoningtheorem-proverconstructive-mathematicsproof-assistants

Projects that are alternatives of or similar to awesome-rust-formalized-reasoning

Leo-III
An Automated Theorem Prover for Classical Higher-Order Logic with Henkin Semantics
Stars: ✭ 29 (-84.32%)
Mutual labels:  logic, theorem-proving, reasoning
pyprover
Resolution theorem proving for predicate logic in pure Python.
Stars: ✭ 71 (-61.62%)
Mutual labels:  theorem-proving, prover, theorem-prover
fm-notes
Unassorted scribbles on formal methods, type theory, category theory, and so on, and so on
Stars: ✭ 19 (-89.73%)
Mutual labels:  theorem-proving, formal-verification
ostrich
An SMT Solver for string constraints
Stars: ✭ 18 (-90.27%)
Mutual labels:  theorem-proving, theorem-prover
cicada
Cicada Language
Stars: ✭ 9 (-95.14%)
Mutual labels:  prover, theorem-prover
typedb
TypeDB: a strongly-typed database
Stars: ✭ 3,152 (+1603.78%)
Mutual labels:  logic, reasoning
typeql
TypeQL: the query language of TypeDB - a strongly-typed database
Stars: ✭ 157 (-15.14%)
Mutual labels:  logic, reasoning
Grakn
TypeDB: a strongly-typed database
Stars: ✭ 2,947 (+1492.97%)
Mutual labels:  logic, reasoning
Imove
Move your mouse, generate code from flow chart
Stars: ✭ 3,282 (+1674.05%)
Mutual labels:  logic
agda-fragment
Algebraic proof discovery in Agda
Stars: ✭ 28 (-84.86%)
Mutual labels:  formal-verification
Philosophy
A list of philosophy books and resources.
Stars: ✭ 206 (+11.35%)
Mutual labels:  logic
Limbo
A Reasoning System for a First-Order Logic of Limited Belief, written in C++
Stars: ✭ 233 (+25.95%)
Mutual labels:  logic
klever
Read-only mirror of the Klever Git repository
Stars: ✭ 18 (-90.27%)
Mutual labels:  formal-verification
Latte
LaTTe : a Laboratory for Type Theory experiments (in clojure)
Stars: ✭ 210 (+13.51%)
Mutual labels:  logic
ciao
Ciao is a modern Prolog implementation that builds up from a logic-based simple kernel designed to be portable, extensible, and modular.
Stars: ✭ 190 (+2.7%)
Mutual labels:  logic
Acl2
ACL2 System and Books as Maintained by the Community
Stars: ✭ 200 (+8.11%)
Mutual labels:  logic
Mesecons
Mod for minetest that adds digital circuitry [=minecraft redstone]
Stars: ✭ 165 (-10.81%)
Mutual labels:  logic
awesome-philosophy
A curated list of awesome philosophy
Stars: ✭ 119 (-35.68%)
Mutual labels:  logic
pomagma
An inference engine for extensional untyped λ-calculus
Stars: ✭ 15 (-91.89%)
Mutual labels:  theorem-proving
rusty-razor
Razor is a tool for constructing finite models for first-order theories
Stars: ✭ 54 (-70.81%)
Mutual labels:  theorem-proving
View All Similar Projects ➔

About

An exhaustive list of all Rust resources regarding automated or semi-automated formalization efforts in any area, constructive mathematics, formal algorithms, and program verification.

As of May 29, 2022, proof of computation & cryptographic stuff are considered off-topic.

awesome-rust-formalized-reasoning is an EDLA project.

The purpose of edla.org is to promote the state of the art in various domains.

Contents

Legend

  • Actively maintened 🔥
  • Archived 💀
  • Benchmark ⌚
  • Best in Class ♦️
  • Book implementation 📖
  • Crate(s) 📦
  • Crates keyword fully listed 💯
  • Deleted by author ♻️
  • Exhumated 👻
  • Inactive 💤
  • List of resources ℹ️
  • Popular ⭐
  • Research paper implementation 🥼
  • Toy project 🐤
  • Video 📺
  • WIP 🚧

Projects

Provers and Solvers

Provers TPTP compliant

  • CoP 📦 - reimplement automated theorem provers of the leanCoP family, such as leanCoP and nanoCoP.
  • lazyCoP ⌚💤 - automatic theorem prover for first-order logic with equality.
  • lerna 💀 - proves theorems.
  • lickety - prototype system for linear resolution with splitting.
  • meancop 📦♻️ - became CoP.
  • Serkr 👻 ⭐ - automated theorem prover for first order logic with equality.

SAT Solver

  • BatSat 📦⭐ - solver forked from ratsat, a reimplementation of MiniSat.
  • CreuSAT ⭐ - formally verified SAT solver verified with Creusot.
  • Debug-SAT 📦 - debuggable automatic theorem prover for boolean satisfiability problems (SAT).
  • dpll-sat - naïve SAT solver implementing the classic DPLL algorithm.
  • msat 📦💀 - MaxSAT Solver.
  • RatSat 📦📦⭐💤 - reimplementation of MiniSat.
  • rsat 📦💀 - SAT Solver.
  • rustsat 🐤 - toy Rust SAT solver.
  • SATCoP - theorem prover for first-order logic based on connection tableau and SAT solving.
  • Satire 📦 - educational SAT solver.
  • SAT-MICRO 🥼 - reimplementation of the SAT-solver described in 'SAT-MICRO: petit mais costaud!'.
  • scrapsat 🚧 - CDCDL SAT Solver.
  • screwsat 📦⭐ - simple CDCL SAT Solver.
  • slp 📦♻️ - became SolHOP.
  • SolHOP 📦💀 - aims to be a SAT and MaxSAT solver. Currently, a CDCL based SAT.
  • Splr 📦♦️⭐ - modern CDCL SAT solver.
  • starlit 🚧 - CDCL SAT solver.
  • Stevia ⭐💤 - simple (unfinished) SMT solver for QF_ABV.
  • UASAT-RS - SAT solver based calculator for discrete mathematics and universal algebra.
  • Varisat📦📦📦📦📦📦📦📦⭐💤 - CDCL based SAT solver.

Proof assistant

  • hakim - hacky interactive theorem prover.
  • cobalt ♻️👻 - a wip minimal proof assistant.
  • Esther 🚧 - simple automated proof assistant.
  • LSTS 📦⭐🔥 - proof assistant that is also a programming language.
  • Noq 📺⭐ - Not Coq. Simple expression transformer that is not Coq.
  • Poi 📦⭐ - pragmatic point-free theorem prover assistant.
  • qbar 📦 - experimental automated theorem verifier/prover and proof assistant.

Misc

  • Avalog 📦⭐ - experimental implementation of Avatar Logic with a Prolog-like syntax.
  • Caso 📦 - category Theory Solver for Commutative Diagrams.
  • Cosette Prover ⭐🥼 - reimplementation of the Cosette prover in Rust.
  • cyclegg - cyclic theorem prover for equational reasoning using egraph.
  • gpp-solver 📦 - small hybrid push-pull solver/planner that has the best of both worlds.
  • hoice ⭐ - ICE-based Constrained Horn Clause (CHC) solver.
  • linear_solver 📦⭐ - linear solver designed to be easy to use with Rust enums.
  • Logic solver ⭐ - logic solver.
  • Mikino 📦📦 - simple induction and BMC engine.
  • minilp 📦⭐💀 - linear programming solver.
  • Monotonic-Solver 📦⭐ - monotonic solver designed to be easy to use with Rust enum expressions.
  • Obvious 💤 - simple little logic solver and calculator.
  • pocket_prover 📦📦⭐ - fast, brute force, automatic theorem prover for first order logic.
  • prover 💀 - first-order logic prover.
  • prover(2) 🐤💤 - experiment with integer relation prover.
  • reachability_solver 📦 - linear reachability solver for directional edges.
  • relsat-rs 🐤 - Experiments with provers.
  • Sequent solver 🐤💤 - simple sequent solver.
  • shari - the 🍣 prover.
  • stupid-smt 🐤💤 - SMT library. Mainly project at the verification course in THU.
  • Totsu 📦📦📦📦📦⭐ - first-order conic solver for convex optimization problems .

Verification

Static Analysis & Rust verification tools

Misc

Libraries

Parser

  • CNF Parser 📦 - efficient and customizable parser for the .cnf file format.
  • DIMACS Parser 📦 - utilities to parse files in DIMACS .cnf or .sat file format.
  • Exec-SAT 📦🐤 - provides routines to parse SAT solver output and to execute SAT solver.
  • Flussab CNF 📦 - parsing and writing of the DIMACS CNF file format.
  • FRAT-rs 🥼 - toolchain for processing and transforming files in the FRAT format.
  • lalrpop-lambda 📦⭐ - λ-calculus Parser (using LALRPOP).
  • Lambda Term Parsing - explores different parser designs for a simple lambda term grammar.
  • mmb-parser 📦 - parser for the Metamath Zero binary proof format.
  • olean-rs - parser/viewer for olean files.
  • smt2 📦 - SMT-LIB 2 parsing library.
  • tptp 📦♦️ - parse the TPTP format.

Bindings

Translator

  • anthem - translate answer set programs to first-order theorem prover language.
  • CNFGEN 📦 - create boolean formulae from boolean expressions and integer expressions.
  • Cnfpack 📦 - converts between DIMACS CNF file format and the compressed binary Cnfpack format.
  • hz-to-mm0 - translator from HOL Zero / Common HOL to Metamath Zero.
  • rust-smt-ir 📦📦⭐ - intermediate representation (IR) in Rust for SMT-LIB queries.

Misc

Books code

There is numerous implementations of TAPL 📖, we keep only the most popular and keep an eye on implementations that worth attention.

Programming Language

Kanren

  • Canrun 📦⭐ - logic programming library inspired by the *Kanren family of language DSLs.
  • miniKANREN 📦 - miniKANREN as a DSL.
  • rslogic 📦⭐ - logic programming framework for Rust inspired by µKanren.
  • rust-kanren ⭐ - loose interpretation of miniKanren and cKanren.
  • µKanren-rs 📦⭐ - implementation of µKanren.

Lambda Calculus

Propositional logic

  • Chevre ♻️ - small propositional logic interpreter.
  • logic 📦 🐤 - crate for propositional logic.
  • logic-resolver 🐤 - toy implementation of resolution for propositional logic.
  • plc - propositional logic calculator.
  • Plogic ⭐ - propositional logic evaluator and rule-based pattern matcher.
  • Prop 📦 - library for theorem proving with Intuitionistic Propositional Logic.
  • Propositional Tableaux Solver 📦 - solver using the propositional tableaux method.
  • Resolution Prover - resolution prover library for propositional logic.
  • resolution-prover - Uses propositional resolution to prove statements and proofs on discord.
  • rs-logik 👻 - propositional logic interpreter.
  • rusty-logic 🐤 - propositional logic analysis.
  • simple-proof-assistant 🐤 - a proof assistant kernel for minimal propositional logic.
  • validator - small utility to test a propositional logic theorem prover.

Unclassified

  • formal-systems-learning-rs - simulations to learn formal systems as typed first-order term rewriting systems.
  • list-routine-learning-rs - simulations to learn typed first-order term rewriting systems that perform list routines.
  • Minimal models - uses a SAT solver to find minimal partial assignments that are model of a CNF formula.
  • n-queens-sat - modelling n-queens problem as conjunctive normal form and solving it with DPLL algorithm.
  • nonogrid 📦 - lightning fast nonogram solver.
  • peano 🥼 - An environment for learning formal mathematical reasoning from scratch.
  • rummy_to_sat - implementation of a solver for Rummy.
  • rust-z3-practice - solving a number of SAT problems using Z3.
  • sudoku_sat - solve Sudoku variants with SAT solvers.
  • Supermux - reduction of the superpermutation problem to Quantified Boolean Formula.
  • Supersat - attempt to find superpermutations by reducing the problem to SAT.
  • tarpit-rs ⭐ - type-level implementation of Smallfuck in Rust. Turing-completeness proof for Rust's type system.

Resources

Books

Research Paper & Thesis

Demos

Blogs

Posts

Crates keywords

Community

Note that the project description data, including the texts, logos, images, and/or trademarks, for each open source project belongs to its rightful owner. If you wish to add or remove any projects, please contact us at [email protected].