Logic Reasoner software 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.