Human-centered automated proof search

DOI10.1007/S10817-021-09594-ZOpenAlexW3191531957MaRDI QIDQ2069871FDOQ2069871

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

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)

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)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Untersuchungen über das logische Schliessen. II
• Gentzen's Proof of Normalization for Natural Deduction
• Title not available (Why is that?)
• The consistency of arithmetics
• Gentzen and Jaśkowski natural deduction: fundamentally similar but importantly different
• Title not available (Why is that?)
• On the rules of suppositions in formal logic
• Title not available (Why is that?)
• Searching for proofs (and uncovering capacities of the mathematical mind)
• Hilbert's Twenty-Fourth Problem
• Title not available (Why is that?)
• Toward Mechanical Mathematics
• Title not available (Why is that?)
• A fully automatic theorem prover with human-style output
• A Brief History of Natural Deduction
• Non-resolution theorem proving
• Normal natural deduction proofs (in classical logic)
• More on the problem of finding a mapping between clause representation and natural-deduction representation
• Automated natural deduction in THINKER
• Natural deduction
• Automated search for Gödel's proofs
• Title not available (Why is that?)
• Mechanizing Mathematical Reasoning
• Title not available (Why is that?)
• The role of the Mizar mathematical library for interactive proof development in Mizar
• Sir Timothy Gowers Interview
• 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

Cited In (3)

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

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)