An Algorithm for Automatic Demonstration of Logical Theorems
Orlando Zaldivar-Zamorategui, Jorge Carrera-Bolaños · 2009
The automatic demonstration of theorems (ADT) is and has been an area of intensive development in Artificial Intelligence (AI). There are actually a variety of procedures, some already implemented as software, that offer the possibility to establish the truth value of a given formula (theorem) in a given contextual system. In this paper we present also an ADT system for first order logic (proposicional calculus). This system is at least as powerful as any other actually available, but simpler and easy to program. It is presented in algorithmic form. The presentation offers also an opportunity to make some considerations about the relation of theoretical logic to its applications and of the meaning of the concepts of theorem and demonstration. Specially, an effort has been made to give an adequate definition in this context of a sufficient, a and a sufficient and necessary condition.