Inference Engines

From SIGSEM

Jump to: navigation, search

Contents

Theorem Provers (FOL)

  • Bliksem (Resolution based Theorem Prover for FOL)
  • Equinox
  • FDPLL/Darwin (First-Order Davis-Putnam-Loveland-Logeman Theorem Prover / Model Evolution Calculus)
  • SPASS (Theorem Prover for First-Order Logic with Equality)
  • LeanTaP (Tableau-based Deduction)
  • Otter
  • Prover9 (Otter's successor)
  • Vampire

Model Builders

  • MACE (model builder for FOL)
  • Paradox (model builder for FOL)
  • Kimba (higher-order logic model builder) [no longer actively maintained]

Description Logic Provers

  • FaCT/FaCT++ (Fast Classification of Terminologies)
  • RACE/RACER/RacerPro (Reasoner for ABoxes and Concept Expressions / OWL reasoner and inference server)

Other types of inference engines

  • Alligator (Theorem Prover for Dependent Type Systems using backward and forward Natural Deduction)
  • DLP (Experimental Description Logic System and Propositional Modal Logic Satisfiability Checker)
  • Isabelle (theorem proving environment)
  • MathWeb (Distributed Theorem Proving)
  • Molle (Tableaux algorithm for the K modal logic in Java)

You may also want to read the Wikipedia article Automated theorem proving.

Retrieved from "http://www.sigsem.org/wiki/Inference_Engines"
Personal tools