Deductive Generalization and Meta-Reasoning or How to Formalize Genesis
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.
Unable to display preview. Download preview PDF.
- [Bi 88]
- [CF 89]
- [CL 73]
- [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
- [De 90]
- [Gid 75]The Gideons, eds. The Holy Bible. National Publishing Company, 1975.Google Scholar
- [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
- [La 89]
- [Lo 78]D. W. Loveland. Automated Theorem Proving: A Logical Basis., North Holland, Amsterdam, 1978.Google Scholar
- [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
- [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
- [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
- [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
- [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
- [Ro 65a]
- [Ro 65b]
- [Sa 90a]G. Salzer. Deductive Generalization for Clause Logic. Year-book of the Kurt- Godel-Society 1989, 47–59, Wien, 1990.Google Scholar
- [Sa 90b]G. Salzer. Unification of Strings with Repetitions. TR E1803/S03, Technische Universität Wien, 1990.Google Scholar
- [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
- [SBV 89]
- [SI 74]
- [Wo 67]