Human-centered automated proof search

DOI10.1007/s10817-021-09594-zOpenAlexW3191531957MaRDI QIDQ2069871

Farzaneh Derakhshan, Wilfried Sieg

Publication date: 21 January 2022

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

Full work available at URL: https://doi.org/10.1007/s10817-021-09594-z

zbMATH Keywords

natural deductionautomated theorem provingproof searchFitch diagramsmachine-oriented proof methodsnatural intercalation calculusnormal proofs

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (1)

Proofs as Objects

Uses Software

• Mizar

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• More on the problem of finding a mapping between clause representation and natural-deduction representation
• Non-resolution theorem proving
• Automated natural deduction in THINKER
• Normal natural deduction proofs (in classical logic)
• Natural deduction
• The role of the Mizar mathematical library for interactive proof development in Mizar
• Automated search for Gödel's proofs
• Untersuchungen über das logische Schliessen. II
• On the rules of suppositions in formal logic
• Gentzen and Jaśkowski natural deduction: fundamentally similar but importantly different
• A fully automatic theorem prover with human-style output
• A Brief History of Natural Deduction
• Sir Timothy Gowers Interview
• Toward Mechanical Mathematics
• Gentzen's Proof of Normalization for Natural Deduction
• Hilbert's Twenty-Fourth Problem
• The automation of proof: a historical and sociological exploration
• NATURAL FORMALIZATION: DERIVING THE CANTOR-BERNSTEIN THEOREM IN ZF
• The AProS Project: Strategic Thinking & Computational Logic
• Mechanizing Mathematical Reasoning
• The consistency of arithmetics

This page was built for publication: Human-centered automated proof search