Normal natural deduction proofs (in classical logic)

DOI10.1023/A:1005091418752zbMath0954.03015MaRDI QIDQ1577339

Wilfried Sieg, John Byrnes

Publication date: 4 September 2000

Published in: Studia Logica (Search for Journal in Brave)

zbMATH Keywords

normal formautomated theorem provingproof searchclassical predicate logicnatural deduction calculi

Mathematics Subject Classification ID

Classical first-order logic (03B10) Mechanization of proofs and logical operations (03B35) Cut-elimination and normal-form theorems (03F05)

Related Items

Proofs as Objects, Proof-Search in Natural Deduction Calculus for Classical Propositional Logic, Shortening of Proof Length is Elusive for Theorem Provers, Correspondence analysis and automated proof-searching for first degree entailment, Goal-oriented proof-search in natural deduction for intuitionistic propositional logic, Focusing in Linear Meta-logic, A framework for proof systems, Automated search for Gödel's proofs, 1999 Spring Meeting of the Association for Symbolic Logic, Unnamed Item, The Cantor–Bernstein theorem: how many proofs?, Automated Proof-searching for Strong Kleene Logic and its Binary Extensions via Correspondence Analysis, A Curry–Howard View of Basic Justification Logic, Human-centered automated proof search, NATURAL FORMALIZATION: DERIVING THE CANTOR-BERNSTEIN THEOREM IN ZF

Uses Software

• Nuprl