Normal natural deduction proofs (in classical logic)
From MaRDI portal
Publication:1577339
DOI10.1023/A:1005091418752zbMath0954.03015MaRDI QIDQ1577339
Publication date: 4 September 2000
Published in: Studia Logica (Search for Journal in Brave)
normal form; automated theorem proving; proof search; classical predicate logic; natural deduction calculi
03B10: Classical first-order logic
03B35: Mechanization of proofs and logical operations
03F05: Cut-elimination and normal-form theorems
Related Items
Unnamed Item, 1999 Spring Meeting of the Association for Symbolic Logic, The Cantor–Bernstein theorem: how many proofs?, A framework for proof systems, Goal-oriented proof-search in natural deduction for intuitionistic propositional logic, Automated search for Gödel's proofs, A Curry–Howard View of Basic Justification Logic, Proof-Search in Natural Deduction Calculus for Classical Propositional Logic, Focusing in Linear Meta-logic
Uses Software