Automatic Theorem Prover (ATP)

As a part of a course project, for Functional Programming, we have made a small Automatic Theorem Prover, which we call ATP, available here.

It is merely 700 lines of Haskell code, and it may require Cabal for installation. The salient features are:

• It employs Resolution as the only inference rule.
• It does not do any support set manipulation, nor checking of consistency of the initial set of axioms.
• Two implementations of Unification algorithm, one employing Lists and the other Maps .
• It can read files in CNF tptp format.
• It does not deal with Equality yet.
• It allows for interactive suggestions of the initial support set.

`We' here refers to:

• Piyush Srivastava
• Jitesh Jain
• Utkarsh Upadhyay
• Sajal Kumar Jain
• Shashank Kapoor

Back to Home