Computer-Oriented Calculi of Sequent Trees

The problem of construction of a computer-oriented technique for inference search based on a certain sequent formalism for first-order classical logic with equality is solved. For this, special calculi of so-called sequent trees are constructed. The following features are inherent to the tree calculi: (i) preliminary skolemization is used for increasing their proof search efficiency with the help of a technique for finding the most general simultaneous unifier, (ii) every calculus is completely induced by a correspondent sequent calculus, (iii) any transformation of a sequent tree is defined by an appropriate (propositional) rule, and what’s more, (iv) certain kinds of the paramodulation rule are added to the sequent tree calculi. For all the calculi, some results about their soundness and completeness are given. Note that an approach under consideration can give a possibility to incorporate the proposed paramodulution technique into, for example, different modifications of the model elimination method, of goal-oriented sequent calculi, and of the tableaux method.