Logic Reasoner 0.1

Logic Reasoner is a theorem prover for first-order logic with equality.

  Add it to your Download Basket!

 Add it to your Watch List!

0/5

Rate it!
send us
an update
LICENSE TYPE:
GPL v3 
USER RATING:
3.3/5 20
DEVELOPED BY:
Lorenzo Castelli
HOMEPAGE:
lcastelli.googlepages.com
CATEGORY:
ROOT \ Science and Engineering \ Artificial Intelligence
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

#theorem prover #formula representation #subsumption resolution #theorem #prover #calculus #subsumption

Add your review!

SUBMIT