Logic Reasoner 0.1

Logic Reasoner is a theorem prover for first-order logic with equality.
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.

last updated on:
October 25th, 2007, 20:57 GMT
developed by:
Lorenzo Castelli
license type:
GPL v3 
ROOT \ Science and Engineering \ Artificial Intelligence


In a hurry? Add it to your Download Basket!

user rating 20



Rate it!

Add your review!