Resolution is cut-free
type: Item
instance of: scholarly article
title: Resolution is cut-free
zbMATH Open document ID: 1197.03010
author: Olivier Hermant
published in: Journal of Automated Reasoning
publication date: 2010-05-26T00:00:00Z
review text: The paper proves through syntactic translation that the extension of the resolution proof system to deduction modulo is equivalent to the cut-free fragment of the sequent calculus modulo. The resolution method in deduction modulo, called ENAR, is proved to be sound with respect to the cut-free fragment of sequent calculus. However, in order to prove completeness of ENAR with respect to the original sequent calculus, extra assumptions are needed. Due to the expressiveness of deduction modulo, the results obtained in this paper can be applied to higher-order resolution, Peano arithmetic and Zermelo set theory.
reviewed by: Emilio Muñoz-Velasco
Mathematics Subject Classification ID: 03B35
zbMATH DE Number: 5711939
zbMATH Keywords: classical sequent calculus
zbMATH Keywords: cut-free
zbMATH Keywords: cut rule
zbMATH Keywords: deduction modulo
zbMATH Keywords: ENAR
zbMATH Keywords: resolution
zbMATH Keywords: rewriting
zbMATH Keywords: Skolemization
zbMATH Keywords: Skolem theorem
describes a project that uses: VAMPIRE
describes a project that uses: Zenon
MaRDI profile type: Publication
full work available at URL: s10817-009-9153-6
OpenAlex ID: W2096711734
cites work: Resolution in type theory
cites work: Logic Programming with Focusing Proofs in Linear Logic
cites work: Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs
cites work: A Semantic Completeness Proof for TaMeD
cites work: On Constructive Cut Admissibility in Deduction Modulo
cites work: Cut Elimination in Deduction Modulo by Abstract Completion
cites work: Automated Reasoning
cites work: HOL-\(\lambda\sigma\): An intentional first-order expression of higher-order logic
cites work: Theorem proving modulo
cites work: Q4474846
cites work: The inverse method
cites work: Proof normalization modulo
cites work: Term Rewriting and Applications
cites work: Q4863622
cites work: Untersuchungen über das logische Schliessen. I
cites work: Linear logic
cites work: Typed Lambda Calculi and Applications
cites work: Q5813181
cites work: Focusing and Polarization in Intuitionistic Logic
cites work: The predicate calculus with \(\varepsilon\)-symbol
cites work: Q5579476
cites work: Q3972527
cites work: Q4846259
cites work: Computing small clause normal forms
cites work: A Machine-Oriented Logic Based on the Resolution Principle
cites work: Handbook of automated reasoning. In 2 vols
cites work: Q3150300
cites work: Q4716271
cites work: Q4539606
cites work: Q5610986
cites work: Proof theory. 2nd ed
cites work: Q4364504
cites work: Constructivism in mathematics. An introduction. Volume I
DOI: 10.1007/S10817-009-9153-6
description: scientific article; zbMATH DE number 5711939