Afonin A. Complete methods of inference search in logic programming systems

The dissertation is devoted to the construction of inference search methods for first-order classical logic and for logic programming systems and their investigation on soundness and completeness. Classical logic was considered both for formulas with equality and for formulas without it. The following investigations were performed. For classical logic without equality, a new sequent approach to inference search was constructed, which gave a possibility for proving a sequent form of Herbrand's theorem not requiring preliminary skolemization and, as a result, for the construction of a family of sound and complete sequent-type calculi for inference search in the signature of an initial first-order theory. Using it, the soundness and completeness of a goal-oriented sequent calculus were proven.