Resolution is cut-free
From MaRDI portal
Publication:972424
DOI10.1007/s10817-009-9153-6zbMath1197.03010MaRDI QIDQ972424
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
rewriting; resolution; cut rule; Skolemization; deduction modulo; cut-free; classical sequent calculus; ENAR; Skolem theorem
03B35: Mechanization of proofs and logical operations
Related Items
Uses Software
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