\(M\)-calculus -- a sequent method for automatic theorem proving (Q1899898)

Systems based on the resolution method and its modifications are currently the most popular for automatic theorem proving. Results associated with automatic use of equality are also important in this field. Despite all this, the idea of using calculi other than the resolution method for automatic theorem proving retains its attractiveness. One of the possibilities is to use Gentzen-like calculi without the cut rule. The \(M\)-calculus developed in this paper is exactly a calculus of this type: it is a restricted version of the sequent calculus. We consider the intuitionistic and classical versions of this calculus.