Logic Reasoner

Logic Reasoner is a theorem prover for first-order logic with equality.

The main objective leading the development of Logic Reasoner has been the creation of a flexible architecture: in particular the program has been designed as a generic infrastructure for theorem proving, which forms the basis for a collection of specific proving techniques. These techniques can be easily combined or replaced to create configurations with different properties.

The main techniques that are currently implemented are:

  • Formula representation using perfectly shared DAGs and flatterms.
  • Calculus based on ordered resolution with selection and superposition.
  • Knuth-Bendix term ordering.
  • Simplifications like subsumption, demodulation, subsumption resolution, etc.
  • Indexing based on perfect discrimination trees and feature vectors.
  • Proving algorithms based on Otter and Discount loops.

Logic Reasoner is implemented in standard C++, and requires Boost, Antlr 2.7.7 and CppUnit.


Source code