CMU Artificial Intelligence Repository
Theorem Proving and Automated Reasoning Systems
coq/ Coq: Calculus of Inductive Constructions
dtp/ DTP: General theorem prover with
domain-independent control of inference.
elf/ Elf: LF Logical Framework
frapps/ FRAPPS: Framework for Resolution-based Automated
ft/ FT: Theorem Prover for Intuitionistic Predicate
hiper/ HIPER: Term rewriting E-completion system
isabelle/ Isabelle: Automated generic theorem prover
keim/ KEIM: Tools for Building Theorem Provers
lcf/ LCF: Automated generic theorem prover
leantap/ LeanTaP: Tableau-based Theorem Prover for FOL
mkrp/ MKRP: Markgraf Karl Refutation Procedure
mvl/ MVL: Multi-Valued Logic
nqthm/ NQTHM: The Boyer-Moore theorem prover.
nuprl/ Nuprl: Proof Development System
otter/ Otter: Resolution-based theorem prover.
plaisted/ Plaisted: Theorem Prover in Prolog
qu_pl/ Qu-Prolog and Ergo: Prototyping of Interactive
rrl/ RRL: Rewrite Rule Laboratory
setheo/ SETHEO: SEquential THEOrem prover
thm/ THM: Boyer-Moore Theorem Prover
xpnet/ XPNet: X Proof Net
This directory contains theorem proving and automated reasoning systems.
CD-ROM: Prime Time Freeware for AI, Issue 1-1
Automated Reasoning, Reasoning!Automated Reasoning,
Last Web update on Mon Feb 13 10:27:43 1995