Abstract
In writing a computer program, the programmer often uses procedures or subroutines to carry out frequently-occurring subsidiary tasks. These tasks range from simple bookkeeping and updating to the seeking of the generalization of two given formulas. Problems that one wishes to solve with the assistance of an automated theorem-proving program likewise often involve subsidiary tasks and the corresponding need for procedures (or their equivalent) to accomplish them. It is reasonable to conjecture that employment of procedures either requires the use of external programs or requires substantial modification of the existing theorem-proving program itself. In this paper we give examples that show that neither is the case. Demodulation is the key to implementing the procedures that accomplish such frequently-occurring tasks.
We give here sets of demodulators for accomplishing a wide variety of tasks. The most complex given demodulator set enables the program to find the least general subsumer of two given unit clauses. We also consider questions of counting and classifying, bookkeeping and updating, and cleanup after case analysis. Finally, we give a set of demodulators for coping with set-theory in an efficient and natural way.
The material presented here is but a sample of the additional possibilities for the use of demodulation. Since it was not known how to accomplish some of the cited tasks purely within the context of automated theorem proving, the examples given here may lead to an expanded use of automated theorem-proving programs in general. Thus, although the use of demodulation for both simplification and canonicalization demonstrates its value, it turns out that demodulation is even more powerful than was realized.
This work was supported in part by the Applied Mathematical Sciences Research Program (KC-04-02) of the Office of Energy Research of the U.S. Department of Energy under Contract W-31-109-Eng-38 (Argonne National Laboratory, Argonne, IL 60439) and in part by NSF grant MCS79-03870 (Northern Illinois University, DeKalb, IL 60115).
Preview
Unable to display preview. Download preview PDF.
References
Allen, J. and Luckham, D., “An interactive theorem-proving program,” Machine Intelligence, Vol. 5(1970), Meltzer and Michie (eds), American Elsevier, New York, pp. 321–336.
Kalman, J., “A shortest single axiom for the classical equivalential calculus,” Notre Dame Journal of Formal Logic, Vol. 19, No. 1, January 1978, pp. 141–144.
Lukasiewicz, J., “Der Aquivalenzenkalkul,” Collectanea Logica, Vol. 1 (1939), pp. 145–169. English translation in [McCall], pp. 88–115 and in [Lukasiewicz/Borkowski], pp. 250–277.
Lukasiewicz, J., Jan Lukasiewicz: Selected Works, ed. by L. Borkowski, North-Holland Publishing Co., Amsterdam (1970).
Lusk, E. and Overbeek, R., “Data structures and control architecture for implementation of theorem-proving programs,” 5th Conference on Automated Deduction, Vol. 87, Lecture Notes in Computer Science, ed. W. Bibel and R. Kowalski, Springer-Verlag, Berlin, 1980, pp. 232–249.
Lusk, E., “Input translator for the environmental theorem prover — user's guide,” to be published as an Argonne National Laboratory technical report.
McCall, S., Polish Logic, 1920–1939, Clarendon Press, Oxford (1967).
McCharen, J., Overbeek, R. and Wos, L., “Problems and experiments for and with automated theorem proving programs,” IEEE Transactions on Computers, Vol. C-25(1976), pp. 773–782.
McCharen, J., Overbeek, R. and Wos, L., “Complexity and related enhancements for automated theorem-proving programs,” Computers and Mathematics with Applications, Vol. 2(1976), pp. 1–16.
Overbeek, R., “An implementation of hyper-resolution,” Computers and Mathematics with Applications, Vol. 1(1975), pp. 201–214.
Peterson, J., “Shortest single axioms for the equivalential calculus,” Notre Dame Journal of Formal Logic, Vol. 17(1976), pp. 267–271.
Peterson, J., “An automatic theorem prover for substitution and detachment systems,” Notre Dame Journal of Formal Logic, Vol. XIX, Jan. 1978, pp. 119–122.
Robinson, J., “A machine-oriented logic based on the resolution principle,” J. ACM, Vol. 12(1965), pp. 23–41.
Robinson, J., “Automatic deduction with hyper-resolution,” International Journal of Computer Mathematics, Vol. 1(1965), pp. 227–234.
Smith, B., “Reference manual for the environmental theorem prover,” to be published as an Argonne National Laboratory technical report.
Veroff, R., “Canonicalization and demodulation,” Argonne National Laboratory, Technical Report ANL-81-6, Argonne, Illinois, February 1981.
Winker, S. and Wos, L., “Automated generation of models and counterexamples and its application to open questions in ternary Boolean algebra,” Proc. of the Eighth International Symposium on Multiple-valued Logic, Rosemont, Illinois, 1978, IEEE and ACM Publ., pp. 251–256.
Winker, S., Wos, L. and Lusk, E., “Semigroups, antiautomorphisms, and involutions: a computer solution to an open problem, I,” Mathematics of Computation, Vol. 37 (1981), pp. 533–545.
Winker, S., “Generation and verification of finite models and counterexamples using an automated theorem prover answering two open questions,” to appear in J. ACM.
Winker, S., Wos, L. and Lusk, E., “Semigroups, anti automorphisms, and involutions: a computer solution to an open problem, II,” in preparation.
Wojciechowski, W. and Wojcik, A., “Multiple-valued logic design by theorem proving,” Proc. of the Ninth International Symposium on Multiple-valued Logic, Bath, England, 1979.
Wos, L., Carson, D. and Robinson, G., “The unit preference strategy in theorem proving,” Proc. of the Fall Joint Computer Conference, 1964, Thompson Book Company, New York, pp. 615–621.
Wos, L., Carson, D. and Robinson, G., “Efficiency and completeness of the set-of-support strategy in theorem proving,” J. ACM, Vol. 12(1965), pp. 536–541.
Wos, L., Robinson, G., Carson, D. and Shalla, L., “The concept of demodulation in theorem proving,” J. ACM, Vol. 14(1967), pp. 698–709.
Wos, L., Winker, S., and Lusk, E., “An automated reasoning system,” AFIPS Conference Proceedings, Vol. 50 (1981), National Computer Conference (Chicago, Ill., 1981), AFIPS Press, pp. 697–702.
Wos, L., Winker, S., Veroff, R., Smith, B. and Henschen, L., “Questions concerning possible shortest single axioms in equivalential calculus: an application of automated theorem proving to infinite domains,” submitted to the Notre Dame Journal of Formal Logic for consideration for publication, May 1981.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1982 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Winker, S.K., Wos, L. (1982). Procedure implementation through demodulation and related tricks. In: Loveland, D.W. (eds) 6th Conference on Automated Deduction. CADE 1982. Lecture Notes in Computer Science, vol 138. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0000054
Download citation
DOI: https://doi.org/10.1007/BFb0000054
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-11558-8
Online ISBN: 978-3-540-39240-8
eBook Packages: Springer Book Archive