CreuSAT - A formally verified SAT solver written in Rust and verified with Creusot.
LatPlan : A domain-independent, image-based classical planner
A Machine-to-Machine Interaction System for Lean 4.
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)
A Lean tactic for Canonical, a search procedure for terms in dependent type theory.
Canonical is a performant sound and complete type inhabitation solver for dependent type theory.
MachSMT: An ML-Driven Algorithm Selection tool for SMT Solvers
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
An automated deductive program verifier based on concurrent separation logic
Reasoner for the description logic EL+.
Imandra Modelling Language CME MDP Model
Bayesian Ontology Reasoner
Julia wrapper around SWI Prolog
A novel approach to learning concept embeddings and approximate reasoning in ALC knowledge bases with neural networks
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."