Simplifying proofs in Fitch-style natural deduction systems

DOI10.1007/s10817-005-9000-3zbMath1108.03016OpenAlexW2104785859MaRDI QIDQ851139

Konstantine Arkoudas

Publication date: 17 November 2006

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-005-9000-3

zbMATH Keywords

first-order logicnatural deductiondenotational proof language

Mathematics Subject Classification ID

Classical first-order logic (03B10) Mechanization of proofs and logical operations (03B35)

Uses Software

• Isabelle
• ML
• VAMPIRE
• HOL
• Hyperproof

Cites Work

• Don't eliminate cut
• Automated natural deduction in THINKER
• The anatomy of vampire. Implementing bottom-up procedures with code trees
• A Brief History of Natural Deduction
• A framework for defining logics
• Theories of Programming Languages
• On Tarski's formalization of predicate logic with identity
• Relational and Kleene-Algebraic Methods in Computer Science
• 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
• Unnamed Item
• Unnamed Item
• Unnamed Item