automated-reasoning 开源项目推荐（183 个）

sarsko /CreuSAT

CreuSAT——一个正式验证的SAT求解器，用Rust编写并通过Creusot验证。

frenzymath /Danus

Orchestrating Mathematical Reasoning Agents with Fact-Graph Memory

DebarghaG /proofofthought

Proof of thought : LLM-based reasoning using Z3 theorem proving with multiple backend support (SMT2 and JSON DSL)

stanford-centaur /PyPantograph

A Machine-to-Machine Interaction System for Lean 4.

chasenorman /CanonicalLean

A Lean tactic for Canonical, a search procedure for terms in dependent type theory.

chasenorman /Canonical

Canonical is a performant sound and complete type inhabitation solver for dependent type theory.

guicho271828 /latplan

LatPlan : A domain-independent, image-based classical planner

dex3r /GPT-Codemaster

Automatic programming by creating Pull Requests from Issues using LLMs

NationalSecurityAgency /Foundation

Foundation is a repository of formal cryptographic specifications

Tractables /LogicCircuits.jl

Logic Circuits from the Juice library

aws-samples /sample-automated-reasoning-formalization

ARchitect helps non-technical users create Automated Reasoning policies from their document

conp-solutions /mergesat

configurable, high-performance SAT solver, implementing incremental solving interface of MiniSat and IPASIR. Based on MiniSat (minisat.se)

ansumandas441 /mathematical-discovery-engine

This is a mathematical discovery engine, which searches new mathematics applying techniques to existing results

nyu-acsys /raven

An automated deductive program verifier based on concurrent separation logic

MachSMT /MachSMT

MachSMT: An ML-Driven Algorithm Selection tool for SMT Solvers

no-way-labs /residue

Hamiltonian decomposition of Z_m^3 Cayley digraphs for all m > 2 — a complete solution to Knuth's "Claude's Cycles," found by LLM agents under a structured exploration prompt. Constructions, proofs, Lean formalization, and a verification suite.

mafait /Thinknowlogy

Automated reasoning based on the Laws of Intelligence naturally embedded in the human language • Open source software • Multilingual, including Chinese

julianmendez /cel

A lightweight Description Logic reasoner for large-scale biomedical ontologies

bio-ontology-research-group /onto2vec

Representation learning for ontologies and their annotations

julianmendez /born

Bayesian Ontology Reasoner