**CMU Artificial Intelligence Repository**

` `

## Theorem Proving and Automated Reasoning Systems

areas/reasonng/atp/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
Proof Procedures
ft/ FT: Theorem Prover for Intuitionistic Predicate
Logic
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
Theorem Provers
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
Keywords:
Automated Reasoning, Reasoning!Automated Reasoning,
Theorem Proving

Last Web update on Mon Feb 13 10:27:43 1995

AI.Repository@cs.cmu.edu