Logic Reasoner is a software tool that verifies the truth of statements in first-order logic with equality, serving as a theorem prover.
The software provides a wide range of techniques that can be easily combined or replaced to create configurations with different properties. Some of the techniques that the software offers include 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, and indexing based on perfect discrimination trees and feature vectors.
The software also offers proving algorithms based on Otter and Discount loops. Logic Reasoner has been implemented in standard C++, and it requires Boost, Antlr 2.7.7, and CppUnit.
Overall, Logic Reasoner is a powerful and flexible software that provides a wide range of proving techniques. With its generic infrastructure for theorem proving, users can easily create configurations that best suit their needs.
Version 0.1: N/A