Deductive Generalization and Meta-Reasoning or How to Formalize Genesis

  • Gernot Salzer
Conference paper
Part of the Informatik-Fachberichte book series (INFORMATIK, volume 287)


When using resolution for showing the unsatisfiability of logic formulas one often encounters infinite sequences of structurally similar clauses. We suggest to use deductive generalization to derive a small number of meta-clauses subsuming these infinite sequences. Resolution is extended by meta-unification in order to resolve meta-clauses instead of ordinary ones.

As a step towards a unification procedure for general meta-terms we investigate the unification of monadic ones. We describe an algorithm yielding a finite, complete and orthonormal set of unifiers. First experiments show the usefulness of our approach: theorem provers save space as well as time, proofs become considerably shorter.

And the Lord God formed man from the dust of the ground and breathed into his nostrils the breath of life; and man became a living soul.

(Genesis 2:1)


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [Bi 88]
    W. Bibel. Advanced Topics in Automated Deduction. Advanced Topics in Artificial Intelligence, LNCS 345, 41–59. Springer Verlag, New York, 1988.CrossRefGoogle Scholar
  2. [CF 89]
    M. Clausen and A. Fortenbacher. Efficient Solution of Linear Diophantine Equations. J. Symbolic Computation 8 (1989), 201–216.MathSciNetzbMATHCrossRefGoogle Scholar
  3. [CL 73]
    C. L. Chang and R. C. T. Lee. Symbolic Logic and Mechanical Theorem Proving. Academic Press, New York, 1973.zbMATHGoogle Scholar
  4. [Da 68]
    J. L. Darlington. Automatic Theorem Proving with Equality Substitutions and Mathematical Induction. Machine Intelligence Vol. 3 (B. Meitzer and D. Mitchie eds.), 113–127. Edinburgh University Press, 1968.Google Scholar
  5. [De 90]
    P. Devienne. Weighted graphs: a tool for studying the halting problem and time complexity in term rewriting systems and logic programming. Theoretical Computer Science 75 (1990), 157–215.MathSciNetzbMATHCrossRefGoogle Scholar
  6. [Gid 75]
    The Gideons, eds. The Holy Bible. National Publishing Company, 1975.Google Scholar
  7. [KB 70]
    D. E. Knuth and P. B. Bendix. Simple Word Problems in Universal Algebra. Computational Problems in Abstract Algebra (J. Leech ed.), 263–297. Pergamon Press, 1970.Google Scholar
  8. [La 89]
    D. Lankford. Non-negative Integer Basis Algorithms for Linear Equations with Integer Coefficients. J. Automated Reasoning 5 (1989), 25–35.MathSciNetzbMATHCrossRefGoogle Scholar
  9. [Lo 78]
    D. W. Loveland. Automated Theorem Proving: A Logical Basis., North Holland, Amsterdam, 1978.Google Scholar
  10. [Ma77]
    G. S. Makanin. The Problem of Solvability of Equations in a Free Semigroup. Mat. Sb. 103(145) (1977), 147–236. English translation in Math. USSR Sb. 32.Google Scholar
  11. [PI 70]
    G. D. Plotkin. A Note on Inductive Generalization. Machine Intelligence Vol. 5 (B. Meitzer and D. Mitchie eds.), 153–163. Edinburgh University Press, 1970.Google Scholar
  12. [PI 71]
    G. D. Plotkin. A Further Note on Inductive Generalization. Machine Intelligence Vol. 6 (B. Meitzer and D. Mitchie eds.), 101–124. Edinburgh University Press, 1971.Google Scholar
  13. [Pu 87]
    P. Purdom. Detecting Looping Simplifications. 2nd Int. Conf. on Rewriting Techniques and Applications #x0027;87, LNCS 256, 54–61. Springer Verlag, New York, 1987.Google Scholar
  14. [Re 70]
    J. C. Reynolds. Transformational Systems and the Algebraic Structure of Atomic Formulas. Machine Intelligence Vol. 5 (B. Meitzer and D. Mitchie eds.), 135–151. Edinburgh University Press, 1970.Google Scholar
  15. [Ro 65a]
    J. A. Robinson. A Machine Oriented Logic based on the Resolution Principle. J. ACM Vol 12 No. 1 (1965), 23–41.zbMATHCrossRefGoogle Scholar
  16. [Ro 65b]
    J. A. Robinson. Automatic Deduction with Hyper-Resolution. Int. J. Comput. Math. 1 (1965), 227–234.zbMATHGoogle Scholar
  17. [Sa 90a]
    G. Salzer. Deductive Generalization for Clause Logic. Year-book of the Kurt- Godel-Society 1989, 47–59, Wien, 1990.Google Scholar
  18. [Sa 90b]
    G. Salzer. Unification of Strings with Repetitions. TR E1803/S03, Technische Universität Wien, 1990.Google Scholar
  19. [Sa 91a]
    G. Salzer. Unique Representation of the Nonnegative Solutions of Linear Dio-phantine Equations. TR E1803/S04, Technische Universität Wien, 1991.Google Scholar
  20. [SBV 89]
    D. Schreye, M. Bruynooghe, K. Verschaetse. On the Existence of Nonterminating Queries for a Restricted Class of Prolog-Clauses. Artificial Intelligence 41 (1989/90), 237–248.MathSciNetzbMATHCrossRefGoogle Scholar
  21. [SI 74]
    J. R. Slagle. Automated Theorem-Proving for Theories with Simplifiers, Commutativity, and Associativity. J. ACM Vol. 21 No. 4 (1974), 622–642.MathSciNetzbMATHCrossRefGoogle Scholar
  22. [Wo 67]
    L. Wos, G. A. Robinson, D. F. Carson and L. Shalla. The Concept of Demodulation in Theorem Proving. J. ACM Vol. 14 No. 4 (1967), 698–709.zbMATHCrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1991

Authors and Affiliations

  • Gernot Salzer
    • 1
  1. 1.Technische Universität WienWienAustria

Personalised recommendations