Using Examples, Case Analysis, and Dependency Graphs in Theorem Proving

  • David A. Plaisted
Part of the Lecture Notes in Computer Science book series (LNCS, volume 170)


The use of examples seems to be fundamental to human methods of proving and understanding theorems. Whether the examples are drawn on paper or simply visualized, they seem to be more common in theorem proving and understanding by humans than in textbook proofs using the syntactic transformations of formal logic. What is the significance of this use of examples, and how can it be exploited to get better theorem provers and better interaction of theorem provers with haman users? We present a theorem proving strategy which seems to mimic the human tendency to use examples, and has other features in common with human theorem proving methods. This strategy may be useful in itself, as well as giving insight into human thought processes. This strategy proceeds by finding relevant facts, connecting them together by causal relations, and abstracting the causal dependencies to obtain a proof. The strategy can benefit by examining several examples to observe common features in their causal dependencies before abstracting to obtain a general proof. Also, the strategy often needs to perform a case analysis to obtain a proof, with different examples being used for each case, and a systematic method of linking the proofs of the cases to obtain a general proof. The method distinguishes between positive and negative literals in a nontrivial way, similar to the different perceptions people have of the logically equivalent statements AB and (¬ B) ⊃ (¬ A). This work builds on earlier work of the author on abstraction strategies [17] and problem redaction methods [18], and also on recent artificial intelligence work on annotating facts with explanatory information [6,7,9]. This method differs from the abstraction strategy in that it is possible to choose a different abstraction for each case in a case analysis proof; there are other differences as well. For other recent work concerning the use of examples in theorem proving see [1] and [2].


Goal Node Causal Relation Theorem Prove Dependency Graph Causal Chain 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Ballantyne, A., and Bledsoe, W., On generating and using examples in proof discovery, Machine Intelligence 10 (Harwood, Chichester, 1982) 3–39.Google Scholar
  2. 2.
    Bledsoe, W., Using examples to generate instantiations for set variables, IJCAI(1983)892–901.Google Scholar
  3. 3.
    Brand, D., Proving theorems with the modification method, SIAM J. Comput. 4 (1975)412–430.MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Chang, C., The decomposition principle for theorem proving systems, Proc. Tenth Annual Allerton Conference on Circuit and System Theory, University of Illinois(1972)20–28.Google Scholar
  5. 5.
    Chang, C. and Lee, R., Symbolic Logic and Mechanical Theorem Proving (Academic Press, New York, 1973).zbMATHGoogle Scholar
  6. 6. Charniak, E., Riesbeck, C., and McDermott, D., Data dependencies, Artificial Intelligence Programming (Lawrence Erlbaum Associates, Hillsdale, N.J., 1980) 193–226Google Scholar
  7. 7.
    Doyle, J., A truth maintenance system, Artificial Intelligence 12 (1979) 231–272.MathSciNetCrossRefGoogle Scholar
  8. 8.
    Fay, M., First-order unification in an equational theory, Proceedings 4th Workshop on Automated Deduction, Austin, Texas (1979)161–167.Google Scholar
  9. 9.
    Fikes, R., Deductive retrieval mechanisms for state description models, Proceedings of the Fourth International Joint Conference on Artificial Intelligence, Tbilisi, Georgia, USSR (1975) 99–106.Google Scholar
  10. 10.
    Gelernter, H., Realization of a geometry theorem-proving machine, Proe. IFIP Congr. (1959)273–282.Google Scholar
  11. 11.
    Henschen, L. and Wos, L., Unit refutations and Horn sets, J. ACM 21(1974)590–605.MathSciNetCrossRefzbMATHGoogle Scholar
  12. 12.
    Huet, G., An algorithm to generate the basis of solutions to homogeneous linear diophantine equations, Information Processing Letters 17 (1978)144–147.MathSciNetCrossRefzbMATHGoogle Scholar
  13. 13.
    Huet, G. and Oppen, D., Equations and rewrite rules: a survey, in Formal Languages: Perspectives and Open Problems (R. Book, ed.), Academic Press, New York, 1980.Google Scholar
  14. 14.
    Lankford, D., Canonical algebraic simplification in computational logic, Memo ATP-25, Automatic Theorem Proving Project, University of Texas, Austin, TX, 1975.Google Scholar
  15. 15.
    Loveland, D., Automated Theorem Proving: A Logical Basis (North-Holland, New York, 1978).zbMATHGoogle Scholar
  16. 16.
    Plaisted, D., An efficient relevance criterion for mechanical theorem proving, Proceedings of the First Annual National Conference on Artificial Intelligence, Stanford University, August, 1980.Google Scholar
  17. 17.
    Plaisted, D., Theorem proving with abstraction, Artificial Intelligence 16 (1981) 47–108.MathSciNetCrossRefzbMATHGoogle Scholar
  18. 18.
    Plaisted, D., A simplified problem reduction format, Artificial Intelligence 18 (1982)227–261.MathSciNetCrossRefzbMATHGoogle Scholar
  19. 19.
    Reiter, R., A semantically guided deductive system for automatic theorem proving, Proc. 3rd IJCAI (1973 41–46.Google Scholar
  20. 20.
    Slagle, J., Automatic theorem proving with renamable and semantic resolution, J. ACM 14 (1967) 687–697.MathSciNetCrossRefzbMATHGoogle Scholar
  21. 21.
    Stickel, M., A unification algorithm for associative-commutative functions, J. ACM 28 (1981)423–434.MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1984

Authors and Affiliations

  • David A. Plaisted
    • 1
  1. 1.Department of Computer ScienceUniversity of IllinoisUrbana

Personalised recommendations