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.