TY - CHAP

T1 - Best-Path Theorem Proving

T2 - Compiling Derivations

AU - Frické, Martin

N1 - Publisher Copyright:
© 2012, Springer Science+Business Media B.V.

PY - 2012

Y1 - 2012

N2 - When computers answer our questions in mathematics and logic they need also to be able to supply justification and explanatory insight. Typical theorem provers do not do this. The paper focuses on tableau theorem provers for First Order Predicate Calculus. The paper introduces a general construction and a technique for converting the tableau data structures of these to human friendly linear proofs using any familiar rule set and ‘laws of thought’. The construction uses a type of tableau in which only leaf nodes are extended. To produce insightful proofs, improvements need to be made to the intermediate output. Dependency analysis and refinement, ie compilation of proofs, can produce benefits. To go further, the paper makes other suggestions including a perhaps surprising one: the notion of best proof or insightful proof is an empirical matter. All possible theorems, or all possible proofs, distribute evenly, in some sense or other, among the possible uses of inference steps. However, with the proofs of interest to humans this uniformity of distribution does not hold. Humans favor certain inferences over others, which are structurally very similar. The author’s research has taken many sample questions and proofs from logic texts, scholastic tests, and similar sources, and analyzed the best proofs for them (‘best’ here usually meaning shortest). This empirical research gives rise to some suggestions on heuristic. The general point is: humans are attuned to certain forms inference, empirical research can tell us what those are, and that empirical research can educate as to how tableau theorem provers, and their symbiotic linear counterparts, should run. In sum, tableau theorem provers, coupled with transformations to linear proofs and empirically sourced heuristic, can provide transparent and accessible theorem proving.

AB - When computers answer our questions in mathematics and logic they need also to be able to supply justification and explanatory insight. Typical theorem provers do not do this. The paper focuses on tableau theorem provers for First Order Predicate Calculus. The paper introduces a general construction and a technique for converting the tableau data structures of these to human friendly linear proofs using any familiar rule set and ‘laws of thought’. The construction uses a type of tableau in which only leaf nodes are extended. To produce insightful proofs, improvements need to be made to the intermediate output. Dependency analysis and refinement, ie compilation of proofs, can produce benefits. To go further, the paper makes other suggestions including a perhaps surprising one: the notion of best proof or insightful proof is an empirical matter. All possible theorems, or all possible proofs, distribute evenly, in some sense or other, among the possible uses of inference steps. However, with the proofs of interest to humans this uniformity of distribution does not hold. Humans favor certain inferences over others, which are structurally very similar. The author’s research has taken many sample questions and proofs from logic texts, scholastic tests, and similar sources, and analyzed the best proofs for them (‘best’ here usually meaning shortest). This empirical research gives rise to some suggestions on heuristic. The general point is: humans are attuned to certain forms inference, empirical research can tell us what those are, and that empirical research can educate as to how tableau theorem provers, and their symbiotic linear counterparts, should run. In sum, tableau theorem provers, coupled with transformations to linear proofs and empirically sourced heuristic, can provide transparent and accessible theorem proving.

KW - Leaf Node

KW - Natural Deduction

KW - Skolem Function

KW - Standard Tableau

KW - Theorem Prover

UR - http://www.scopus.com/inward/record.url?scp=85145057901&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85145057901&partnerID=8YFLogxK

U2 - 10.1007/978-94-007-3983-3_18

DO - 10.1007/978-94-007-3983-3_18

M3 - Chapter

AN - SCOPUS:85145057901

T3 - Studies in History and Philosophy of Science(Netherlands)

SP - 255

EP - 274

BT - Studies in History and Philosophy of Science(Netherlands)

PB - Springer Science and Business Media B.V.

ER -