Automatic Programming Systems Dedicated for Proving of Theorems

摘要

The paper presents a short version of the fully automated programmed systems, intended for proving of theorems in the first-order predicate calculus. Proofs in the form of refutations are based on the following rules of derivation: the orderly linear resolution with marked literals (OL- resolution), the rules of binary induction (P- rule) and the rules of symmetry. The ATP system was conducted by the application of the Expert System CORAL-2000 at the Faculty of Electrical Engineering, at the University of Podgorica, during the period from 1996 to 2004.