CreuSAT - A formally verified SAT solver written in Rust and verified with Creusot.
Proof of thought : LLM-based reasoning using Z3 theorem proving with multiple backend support (SMT2 and JSON DSL)
A Machine-to-Machine Interaction System for Lean 4.
A Lean tactic for Canonical, a search procedure for terms in dependent type theory.
LatPlan : A domain-independent, image-based classical planner
Canonical is a performant sound and complete type inhabitation solver for dependent type theory.
Automatic programming by creating Pull Requests from Issues using LLMs
Logic Circuits from the Juice library
configurable, high-performance SAT solver, implementing incremental solving interface of MiniSat and IPASIR. Based on MiniSat (minisat.se)
MachSMT: An ML-Driven Algorithm Selection tool for SMT Solvers
An automated deductive program verifier based on concurrent separation logic
Representation learning for ontologies and their annotations
A lightweight Description Logic reasoner for large-scale biomedical ontologies
Distributed constraint satisfaction with recursive message-passing agents
Reasoner for the description logic EL+.
Bayesian Ontology Reasoner
Imandra Modelling Language CME MDP Model
A novel approach to learning concept embeddings and approximate reasoning in ALC knowledge bases with neural networks
Julia wrapper around SWI Prolog
Imandra Protocol Language example models
Add a description, image, and links to the automated-reasoning topic page so that developers can more easily learn about it.
To associate your repository with the automated-reasoning topic, visit your repo's landing page and select "manage topics."