Abstract:
An algorithm for verification of formalized mathematical proofs is considered. Its main part is described in the framework of some production system with metavariables. Theorems of soundness and completeness are proved.
Keywords:automated theorem proving, system for automated deduction, first order language, predicate calculus, production system, artificial intelligence.
Fulltext:
PDF file (422 kB)