Generating theorem proving procedures from axioms of Truncated Predicate Calculus
Grzegorz Wiaderek, Iwona Skalna · arXiv (Cornell University) · 2019
We present a~novel approach to the problem of automated theorem proving. Polynomial cost procedures that recognise sentences belonging to a theory are generated on a basis of a set of axioms of the so-called Truncated Predicate Calculus being a~subset of standard predicate calculus. Several exemplary problems are included to show the performance of the proposed approach.