Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
We can omit discussion of identity from this paper; it is something of a special case and none of the techniques explained here have any distinctive insights concerning it.
- 2.
Space precludes further detailed description of those in this paper, and the question of automatically closing tableaux is not the present target.
- 3.
And the technique is easily adapted if the focus of interest is consistency or simultaneous satisfiability etc.
- 4.
Although the premises are being depicted here as something of a list, conceptually they are a set. (There is no need to complicate this with ‘structural’ rules.)
- 5.
Here the notation ‘P1&P2’ is being used as a pattern to show a formula with & as its main connective and P1 and P2 as subformulas. The premises are a set, but writing the formula that is being processed first helps draw attention to it.
- 6.
The extension steps correspond to one or more lines in a linear proof.
References
Bergmann, M., J. Moor, and J. Nelson. 1998. The logic book, 4th ed. New York: McGraw-Hill.
Beth, E.W. 1969. Semantic entailment and formal derivability. In The philosophy of mathematics, ed. J. Hintikka, 9–41. London: Oxford University Press.
Black, P.E. 2005. British Museum technique. Dictionary of algorithms and data structures. Retrieved July 2009, from http://www.itl.nist.gov/div897/sqg/dads/HTML/britishMuseum.html.
Copeland, B.J., and D.R. Murdoch. 1991. The Arthur Prior memorial conference: Christchurch 1989. The Journal of Symbolic Logic 56(1): 372–382.
D’Agostino, M., et al. (eds.). 1999. Handbook of tableau methods. Dordrecht: Kluwer Academic Publishers.
Fitting, M. 1996. First-order logic and automated theorem proving, 2nd ed. Berlin: Springer.
Fitting, M. 1998. Introduction. In Handbook of tableau methods, ed. M. D’Agostino et al. Dordrecht: Kluwer Academic Publishers.
Frické, M. 1989a. Derivation planner. Dunedin: Unisoft.
Frické, M. 1989b. Deriver plus. Ventura: Kinko’s Academic Courseware Exchange.
Gallier, J.H. 1986. Logic for computer science: Foundations of automatic theorem proving. New York: Harper Row.
Gentzen, G. 1935. Investigations into logical deduction. In The collected papers of Gerhard Gentzen, ed. M.E. Szabo. Amsterdam: North-Holland.
Hähnle, R. 2001. Tableaux and related methods. In Handbook of automated reasoning, ed. J.A. Robinson and A. Voronkov. Cambridge: MIT Press.
Howson, C. 1997. Logic with trees: An introduction to symbolic logic. London: Routledge.
Jeffrey, R.C. 1967. Formal logic: Its scope and limits. New York: McGraw Hill.
Letz, R. 1999. First-order tableau methods. In Handbook of tableau methods, ed. M. D’Agostino et al. Dordrecht: Kluwer Academic Publishers.
Lindstrom, P. 1969. On extensions of elementary logic. Theoria 35: 1–11.
Manzano, M. 1996. Extensions of first-order logic. Cambridge: Cambridge University Press.
Mill, J.S. 1869. II. Of the liberty of thought and discussion. In On liberty, ed. J.S. Mill. London: Longman, Roberts & Green.
Quine, W.V. 1970. Philosophy of logic, 2nd ed. Oxford: Oxford University Press.
Robinson, J.A., and A. Voronkov (eds.). 2001. Handbook of automated reasoning. Cambridge: MIT Press.
Sieg, W., and J. Byrnes. 1998. Normal natural deduction proofs (in classical logic). Studia Logica 60: 67–106.
Smullyan, R. 1968. First order logic. Berlin: Springer.
Wolfram, S. 2002. A new kind of science. Champaign: Wolfram Media, Inc.
Zalta, E.N. 2009. Achieving Leibniz’s goal of a computational metaphysics. The 2009 North American Conference on Computing and Philosophy. Bloomington.
Zalta, E.N., B. Fitelson, and P. Oppenheimer. 2011. Computational metaphysics. Retrieved 18 November 2011, from http://mally.stanford.edu/cm/.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Appendices
Appendix A: The Extension Heuristic
This is a heuristic (and algorithm) for the construction of tableaux that seems to do well, on average, on the linear proofs that it will generate, across a wide range of proofs. Details can differ, depending on what rules are available. But this is the core.
The overriding control principle looks through everything available, as extendable formulas in a leaf sequent label, in a series of ‘sweeps’.Footnote 6
If any sweep produces a step or extension that can be made, that step is made and the whole series of sweeps is started again on the resulting formulas.
-
Sweep 1:
-
any formula signed true that has implication as its main connective, provided that its ‘if clause’ can be proved (this is tested for, recursively). This is Modus Ponens.
-
-
Sweep 2:
-
any formula signed true that is a double negation, an and, or an equivalence. These steps are Double Negation Elimination, And Elimination, and Equivalence Elimination.
-
-
Sweep 3:
-
any formula signed false that is an implication, a negation, or an equivalence. These steps are Conditional Proof, Reductio, and Equivalence Introduction
-
-
Sweep 4:
-
any formula signed true that is an or. This step is Or Elimination.
-
-
Sweep 5:
-
any formula signed true that has the existential quantifier as its main connective, and which can be instantiated without change of bound variable. This step is Existential Instantiation (without change of variable).
-
-
Sweep 6:
-
any formula signed true that has the existential quantifier as its main connective. This step is Existential Instantiation (with change of variable—sweep 5 picks up the ones that do not need it).
-
-
Sweep 7:
-
any formula signed false that has the universal quantifier as its main connective, and which can be generalized to without change of bound variable. This step is Universal Generalization (without change of variable).
-
-
Sweep 8:
-
any formula signed false that has the universal quantifier as its main connective. This step is Universal Generalization (with change of variable—sweep 7 picks up the ones that do not need it).
-
-
Sweep 9:
-
any formula signed false which is a double negation, an and, or an or. These steps are Double Negation Introduction, And Introduction, and Or Introduction.
-
-
Sweep 10:
-
any formula signed true that has the universal quantifier as its main connective, and which can be instantiated without change of bound variable. This step is Universal Instantiation (without change of variable).
-
-
Sweep 11:
-
any formula signed false that has the existential quantifier as its main connective. This step is Existential Generalization.
-
-
Sweep 12:
-
any formula signed true that has the universal quantifier as its main connective. This step is Universal Instantiation.
-
-
Sweep 13:
-
any formula signed true that is the negation of a universally quantified formula or the negation of an existentially quantified formula. This step is Negation of Quantifier (usually a rewrite).
-
-
Sweep 14:
-
any formula signed true that is an implication, the negation of an and, the negation of an or, the negation of an equivalence or the negation of a implication. These steps are usually complex lemmas.
-
-
Sweep 15:
-
any formula signed true EXCEPT atomic and the negation of atomic formulas. (The default catch-all.)
-
-
Sweep 16:
-
any formula signed false EXCEPT atomic and the negation of atomic formulas. (The default catch-all.)
-
Appendix B: A Small Example
Here is one running implementation being asked to permute existential quantifiers (Fig. 18.13).
Starting to automatically derive (∃x)(∃y)Fxy ⊃ (∃y)(∃x)Fxy
And this is the output when using Introduction-Elimination rules (Fig. 18.14).
An automatic derivation of (∃x)(∃y)Fxy ⊃ (∃y)(∃x)Fxy using Introduction-Elimination Rules
And here is the same theorem/proof provided using Copi-style linear rules (Fig. 18.15).
The same derivation using Copi style rules
These are quite different in that Copi brings in equivalence by definition, or replacement, from conjoined conjunctions, and it has its own version of Existential Instantiation (which it calls ‘Elimination’). The Intro-Elim rule set makes much more extensive use of sub-proofs.
This is a small example. The point of it is not that one rule set is better than another. Rather it is that the User can choose whatever they would like, and suitable software can provide it for them.
The reader of this paper can try examples of their own derivations at
http://softoption.us/content/node/165 for Intro-Elim
and
Rights and permissions
Copyright information
© 2012 Springer Science+Business Media B.V.
About this chapter
Cite this chapter
Frické, M. (2012). Best-Path Theorem Proving: Compiling Derivations. In: Maclaurin, J. (eds) Rationis Defensor. Studies in History and Philosophy of Science, vol 28. Springer, Dordrecht. https://doi.org/10.1007/978-94-007-3983-3_18
Download citation
DOI: https://doi.org/10.1007/978-94-007-3983-3_18
Published:
Publisher Name: Springer, Dordrecht
Print ISBN: 978-94-007-3982-6
Online ISBN: 978-94-007-3983-3
eBook Packages: Humanities, Social Sciences and LawPhilosophy and Religion (R0)