Abstract
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)
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
Preview
Unable to display preview. Download preview PDF.
References
W. Bibel. Advanced Topics in Automated Deduction. Advanced Topics in Artificial Intelligence, LNCS 345, 41–59. Springer Verlag, New York, 1988.
M. Clausen and A. Fortenbacher. Efficient Solution of Linear Diophantine Equations. J. Symbolic Computation 8 (1989), 201–216.
C. L. Chang and R. C. T. Lee. Symbolic Logic and Mechanical Theorem Proving. Academic Press, New York, 1973.
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.
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.
The Gideons, eds. The Holy Bible. National Publishing Company, 1975.
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.
D. Lankford. Non-negative Integer Basis Algorithms for Linear Equations with Integer Coefficients. J. Automated Reasoning 5 (1989), 25–35.
D. W. Loveland. Automated Theorem Proving: A Logical Basis., North Holland, Amsterdam, 1978.
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.
G. D. Plotkin. A Note on Inductive Generalization. Machine Intelligence Vol. 5 (B. Meitzer and D. Mitchie eds.), 153–163. Edinburgh University Press, 1970.
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.
P. Purdom. Detecting Looping Simplifications. 2nd Int. Conf. on Rewriting Techniques and Applications #x0027;87, LNCS 256, 54–61. Springer Verlag, New York, 1987.
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.
J. A. Robinson. A Machine Oriented Logic based on the Resolution Principle. J. ACM Vol 12 No. 1 (1965), 23–41.
J. A. Robinson. Automatic Deduction with Hyper-Resolution. Int. J. Comput. Math. 1 (1965), 227–234.
G. Salzer. Deductive Generalization for Clause Logic. Year-book of the Kurt- Godel-Society 1989, 47–59, Wien, 1990.
G. Salzer. Unification of Strings with Repetitions. TR E1803/S03, Technische Universität Wien, 1990.
G. Salzer. Unique Representation of the Nonnegative Solutions of Linear Dio-phantine Equations. TR E1803/S04, Technische Universität Wien, 1991.
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.
J. R. Slagle. Automated Theorem-Proving for Theories with Simplifiers, Commutativity, and Associativity. J. ACM Vol. 21 No. 4 (1974), 622–642.
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.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Salzer, G. (1991). Deductive Generalization and Meta-Reasoning or How to Formalize Genesis. In: Kaindl, H. (eds) 7. Österreichische Artificial-Intelligence-Tagung / Seventh Austrian Conference on Artificial Intelligence. Informatik-Fachberichte, vol 287. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-46752-3_12
Download citation
DOI: https://doi.org/10.1007/978-3-642-46752-3_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-54567-5
Online ISBN: 978-3-642-46752-3
eBook Packages: Springer Book Archive