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.