Yu. I. Vtorushin, “Evidence algorithm for first-order logic with equality”, Intelligent systems. Theory and applications, 2021, Volume 25, Issue 1,Pages <nobr>21

Part 1. General problems of the intellectual systems theory

Evidence algorithm for first-order logic with equality

Yu. I. Vtorushin

DSS Lab

Abstract: The article is a continuation of the article [1]. An algorithm for verifying formalized mathematical proofs for first-order predicate logic with equality is considered. Theorems about its correctness and completeness are proved.

Keywords: automated theorem proving, system for automated deduction, first order language, predicate calculus, production system, artificial intelligence.