Resolution is cut-free

DOI10.1007/S10817-009-9153-6MaRDI QIDQ972424zbMATH OpenOpenAlexFDO

Authors Olivier Hermant

Publication date 26 May 2010

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10817-009-9153-6

zbMATH Keywords

classical sequent calculuscut rulecut-freededuction moduloENARresolutionrewritingSkolem theoremSkolemization

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

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.

Recommendations

• Theorem proving modulo
• Clausal presentation of theories in deduction modulo
• Cut Elimination in Deduction Modulo by Abstract Completion
• Cut rule for the resolution method
• Cut Admissibility by Saturation

Cites work

• A Machine-Oriented Logic Based on the Resolution Principle
• A Semantic Completeness Proof for TaMeD
• Automated Reasoning
• Computing small clause normal forms
• Constructivism in mathematics. An introduction. Volume I
• Cut Elimination in Deduction Modulo by Abstract Completion
• Focusing and Polarization in Intuitionistic Logic
• Handbook of automated reasoning. In 2 vols
• HOL-\(\lambda\sigma\): An intentional first-order expression of higher-order logic
• scientific article; zbMATH DE number 1809861 (Why is no real title available?)
• scientific article; zbMATH DE number 15881 (Why is no real title available?)
• scientific article; zbMATH DE number 1088191 (Why is no real title available?)
• scientific article; zbMATH DE number 2079034 (Why is no real title available?)
• scientific article; zbMATH DE number 1765670 (Why is no real title available?)
• scientific article; zbMATH DE number 949290 (Why is no real title available?)
• scientific article; zbMATH DE number 789391 (Why is no real title available?)
• scientific article; zbMATH DE number 837700 (Why is no real title available?)
• scientific article; zbMATH DE number 3296224 (Why is no real title available?)
• scientific article; zbMATH DE number 3333259 (Why is no real title available?)
• scientific article; zbMATH DE number 3074068 (Why is no real title available?)
• Linear logic
• Logic Programming with Focusing Proofs in Linear Logic
• On Constructive Cut Admissibility in Deduction Modulo
• Proof normalization modulo
• Proof theory. 2nd ed
• Resolution in type theory
• Term Rewriting and Applications
• The inverse method
• The predicate calculus with -symbol
• Theorem proving modulo
• Typed Lambda Calculi and Applications
• Untersuchungen über das logische Schliessen. I
• Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs

Cited in

(8)

• First-order automated reasoning with theories: when deduction modulo theory meets practice
• Translation of resolution proofs into short first-order proofs without choice axioms
• Linking focusing and resolution with selection
• Linking focusing and resolution with selection
• Complexity of translations from resolution to sequent calculus
• Translation of resolution proofs into short first-order proofs without choice axioms.
• From modal sequent calculi to modal resolution
• Clausal presentation of theories in deduction modulo

Describes a project that uses

Uses Software

• VAMPIRE
• Zenon

This page was built for publication: Resolution is cut-free

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q972424)