Human-centered automated proof search

DOI10.1007/S10817-021-09594-ZMaRDI QIDQ2069871zbMATH OpenOpenAlexFDO

Authors Wilfried Sieg, Farzaneh Derakhshan

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)

Recommendations

• scientific article; zbMATH DE number 4203762
• Automated search for Gödel's proofs
• Automated search for Gödel's proofs
• Proof planning: A practical approach to mechanized reasoning in mathematics
• Searching for proofs (and uncovering capacities of the mathematical mind)

Cites work

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

Cited in

(3)

• Automatic acquisition of search control knowledge from multiple proof attempts.
• Proofs as Objects
• Automated search for Gödel's proofs

Describes a project that uses

Uses Software

• Mizar

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2069871)