nanoCoP: Natural Non-clausal Theorem Proving

nanoCoP: Natural Non-clausal Theorem Proving

Jens Otten

Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence
Best Sister Conferences. Pages 4924-4928. https://doi.org/10.24963/ijcai.2017/695

Most efficient fully automated theorem provers implement proof search calculi that require the input formula to be in a clausal form, i.e. disjunctive or conjunctive normal form. The translation into clausal form introduces a significant overhead to the proof search and modifies the structure of the original formula. Translating a proof in clausal form back into a more readable non-clausal proof of the original formula is not straightforward. This paper presents a non-clausal automated theorem prover for classical first-order logic. It is based on a non-clausal connection calculus and implemented with a few lines of Prolog code. Working entirely on the original structure of the input formula yields not only a speed up of the proof search, but the resulting non-clausal proofs are also shorter.
Keywords:
Artificial Intelligence: knowledge representation and reasoning
Artificial Intelligence: artificial intelligence