Abstract:
Automated proof search in single-conclusion sequential variant of classical predicate calculus is considered. In this algorithm, metavariables and partial skolemization are used. Theorems of soundness and completeness for the considered algorithm are proved.
Keywords:automated theorem proving, mechanical proof search, first order language, predicate calculus, sequent calculus, production system, artificial intelligence.
Fulltext:
PDF file (551 kB)