Automated Reasoning
Showing 15 of 15 projects
A high-performance theorem prover and satisfiability modulo theories (SMT) solver from Microsoft Research.
A curated collection of Monte Carlo tree search research papers with implementations from top AI conferences.
An automated solver for proving the equivalence of SQL queries using formal verification.
An automated reasoning hammer tool for Rocq that combines learning with external provers to automate proofs in dependent type theory.
An open-source Hierarchical Task Network (HTN) AI planner written in Common Lisp, supporting PDDL and HDDL.
A Coq plugin that checks proof witnesses from external SAT/SMT solvers and provides certified decision procedures.
A Coq library for deductive synthesis of correct-by-construction abstract data types and parsers.
A Java library for creating, manipulating, and solving Boolean and Pseudo-Boolean formulas with a focus on memory efficiency and performance.
A strongly-typed genetic programming framework for Python that makes evolutionary algorithms accessible and fun.
A modular relation algebra library for Rocq (Coq) with reflexive decision tactics for Kleene algebra with tests and related theories.
A Rocq/Coq library providing formal definitions and mechanically verified proofs for rewriting theory, λ-calculus, and termination analysis.
A Coq plugin providing tactics for rewriting universally quantified equations modulo associativity and commutativity.
Extends Coq's zify tactic to support Mathematical Components library definitions for arithmetic solving.
A generic goal preprocessing tool for proof automation tactics in Coq.
Ada binding to the Z3 theorem prover for formal verification and constraint solving.
Related Tags
Found a gem we're missing?
Open-Awesome is built by the community, for the community. Submit a project, suggest an awesome list, or help improve the catalog on GitHub.