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
and the other
- It can read files in CNF tptp
- 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