Proof-terms for classical and intuitionistic resolution
From MaRDI portal
Publication:4647497
DOI10.1007/3-540-61511-3_66zbMath1415.03029MaRDI QIDQ4647497
Eike Ritter, Lincoln Wallen, David J. Pym
Publication date: 15 January 2019
Published in: Automated Deduction — Cade-13 (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/3-540-61511-3_66
03B35: Mechanization of proofs and logical operations
03B20: Subsystems of classical logic (including intuitionistic logic)
03B40: Combinatory logic and lambda calculus
Related Items
Some pitfalls of LK-to-LJ translations and how to avoid them, On the semantics of classical disjunction
Cites Work
- First-order modal tableaux
- Gentzen-type systems, resolution and tableaux
- Untersuchungen über das logische Schliessen. I
- Uniform proofs as a foundation for logic programming
- Theorem Proving via General Matings
- On Matrices with Connections
- On the intuitionistic force of classical search (Extended abstract)
- A Machine-Oriented Logic Based on the Resolution Principle
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item