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