Resolution is cut-free

DOI10.1007/S10817-009-9153-6zbMATH Open1197.03010OpenAlexW2096711734MaRDI QIDQ972424FDOQ972424

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

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

zbMATH Keywords

resolutionrewritingcut ruleSkolemizationdeduction modulocut-freeclassical sequent calculusENARSkolem theorem

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Cites Work

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

Cited In (7)

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

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)