Software

ACL2 Version 2.7

cs.utexas.edu

A programming language in which you can model computer systems and a tool to help prove properties of those models. Available under GPL and runs on various platforms. Includes re…

81 visits May 20, 2025 Details

Automated Reasoning Project

cslab.anu.edu.au

Web resource provided by research group. Includes access to software developed by the team, coverering such projects as FINDER (Finite Domain Enumerator), MaGIC (Matrix Generator …

199 visits Jul 15, 2024 Details

Bertrand

humnet.ucla.edu

First-order satisfiability checker and prover for the Macintosh.

498 visits Dec 12, 2024 Details

Church

alcyone.com

Program understands the different types of lambda expressions, can extract lists of variables (both free and bound) and subterms, and can simplify complicated expressions. Uses Py…

419 visits Aug 3, 2025 Details

CrocoPat: Simple and Efficient Relational Programming

mtc.epfl.ch

CrocoPat manipulates relations of any arity, including graphs (which are binary relations). Its simple and expressive query and manipulation language is based on first-order predic…

40 visits Feb 10, 2024 Details

Database of Existing Mechanized Reasoning Systems

-formal.stanford.edu

A list (&gt;50 entries) of automatic resolution provers (like Otter), interactive provers (like PVS) and other mechanized reasoning tools.

457 visits Nov 5, 2025 Details

DC Proof Online

dcproof.com

New proof-writing software to teach the fundamentals of logic and proof. Enables users/students to write error-free proofs by selecting rules of inference, axioms, etc. from conven…

300 visits Jun 16, 2025 Details

DELORES

dfki.uni-kl.de

A forward-chaining reasoning engine for defeasible logic, a less expressive but more efficient nonmonotonic logic.

84 visits Dec 8, 2024 Details

Gateway to Logic

logik.phl.univie.ac.at

A collection of web-based logic programs offering a number of logical functions: interactively or automatically build proofs, check theorems, and operate on propositional logic for…

314 visits Jan 16, 2024 Details

Isabelle

cl.cam.ac.uk

A generic theorem proving environment developed at Cambridge University (Larry Paulson) and TU Munich (Tobias Nipkow). Includes logic, documentation and free download.

164 visits Nov 26, 2024 Details

llprover

bach.scitec.kobe-u.ac.jp

A linear logic prover that searches a cut-free proof for the given two-sided sequent of first-order linear logic.

245 visits Mar 3, 2024 Details

Logic Software from CSLI

-csli.stanford.edu

By Jon Barwise and John Etchemendy.

475 visits Dec 17, 2024 Details

LOOM

isi.edu

A language and environment for constructing intelligent applications. It is a research project in the Artificial Intelligence research group at the University of Southern Califor…

75 visits Mar 29, 2025 Details

Ludwig

mintlogic.com

Application that draws truth-tables for propositional logic formulae. Available for free download and web use.

341 visits Mar 5, 2024 Details

LWB

lwb.unibe.ch

Logics Workbench.

225 visits Jan 13, 2026 Details

ModLeanTAP: Lean Tableau-based Deduction for Propositional Modal Logics

i12www.ira.uka.de

Lean Tableau-based Deduction for Propositional Modal Logics. By Bernhard Beckert.

196 visits May 3, 2023 Details

MUltlog

logic.at

Takes as input the specification of a finitely-valued first-order logic and produces a sequent calculus, a natural deduction system, and clause formation rules for this logic.

432 visits Apr 18, 2023 Details

MUltseq

logic.at

A generic sequent prover for propositional finitely-valued logics.

119 visits Aug 31, 2024 Details

Paradox

cs.chalmers.se

A tool that processes first-order logic problems and tries to find finite-domain models for them; written by Koen Claessen and Niklas SÃ¶rensson. Haskell and C++; free download un…

305 visits Jul 3, 2024 Details

Proof General

proofgeneral.inf.ed.ac.uk

Comprehensive Gnu-Emacs and XEmacs interface for several theorem provers including Coq, Isabelle, Lego, and Phox.

420 visits Jun 1, 2024 Details

Category Info