\(M\)-calculus -- a sequent method for automatic theorem proving
type: Item
instance of: scholarly article
title: \(M\)-calculus -- a sequent method for automatic theorem proving
zbMATH Open document ID: 0835.68108
DOI: 10.1007/BF01130096
author: A. V. Mantsivoda
published in: Cybernetics and Systems Analysis
publication date: 1995-11-02T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 03B35
zbMATH DE Number: 803884
zbMATH Keywords: \(M\)-calculus
zbMATH Keywords: sequent calculus
MaRDI profile type: Publication
cites work: Q5679729
cites work: Q3782836
cites work: Non-resolution theorem proving
cites work: Q3954845
Recommended article: Q4871733
Recommended article: A sequent calculus for automated reasoning in symbolic computation systems
Recommended article: Q4013071
Recommended article: A formal framework for specifying sequent calculus proof systems
Recommended article: Generic Methods for Formalising Sequent Calculi Applied to Provability Logic
Recommended article: A sequent calculus and a theorem prover for standard conditional logics
Recommended article: Q2753786
Recommended article: An automata theoretic decision procedure for the propositional mu- calculus
Recommended article: A calculus for conditional inductive theorem proving
Recommended article: Automata for the modal μ-calculus and related results
description: scientific article; zbMATH DE number 803884