Resolution is cut-free

DOI10.1007/s10817-009-9153-6zbMath1197.03010MaRDI QIDQ972424

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

rewriting; resolution; cut rule; Skolemization; deduction modulo; cut-free; classical sequent calculus; ENAR; Skolem theorem

Mathematics Subject Classification ID

03B35: Mechanization of proofs and logical operations

Related Items

Unnamed Item, Complexity of translations from resolution to sequent calculus, Clausal presentation of theories in deduction modulo, First-order automated reasoning with theories: when deduction modulo theory meets practice

Uses Software

• VAMPIRE
• Zenon

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Linear logic
• The predicate calculus with \(\varepsilon\)-symbol
• Proof theory. 2nd ed
• Constructivism in mathematics. An introduction. Volume I
• Theorem proving modulo
• Untersuchungen über das logische Schliessen. I
• HOL-λσ: an intentional first-order expression of higher-order logic
• Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs
• Focusing and Polarization in Intuitionistic Logic
• On Constructive Cut Admissibility in Deduction Modulo
• Logic Programming with Focusing Proofs in Linear Logic
• Proof normalization modulo
• Automated Reasoning
• A Semantic Completeness Proof for TaMeD
• Cut Elimination in Deduction Modulo by Abstract Completion
• A Machine-Oriented Logic Based on the Resolution Principle
• Resolution in type theory
• Term Rewriting and Applications
• Typed Lambda Calculi and Applications