Abstract
We propose an algorithm to prove a definite clause is modeled by an intended minimal model of a set of definite clauses. In the algorithm, no induction scheme will be used explicitly, although in effect a mathematical induction is implied. This algorithm corresponds to an inductionless induction method using the Knuth-Bendix algorithm in an equation problem. It resembles the completion algorithm, but in fact it is a completely different algorithm.
This paper is a revised and extended version of [12]
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Apt, K.R. and van Emden, M.H.: Contribution to the theory of logic programming, J. ACM 29 (1982) 841–862
Boyer, R.S. and Moore, J.S.: Proving Theorems About LISP Functions, J. ACM 22 (1975) 129–144
van Emden, M.H. and Kowalski, R.A.: The semantics of predicate logic as a programming language, J. ACM 23 (1976) 733–742
Hsiang, J.: Refutational Theorem Proving using Term-Rewriting System, Artificial Intelligence 25 (1985) 255–300
Hsiang, J. and Srivas, M.: Automatic Inductive Theorem Proving using Prolog, Theoretical Computer Science 54 (1987) 3–28
Huet, G. and Hullot, J-M.: Proofs by Induction in Equational Theories with Constructors, Comput. Syst. Sci. 25 (1982) 239–266
Kanamori, T. and Fujita, H.: Formulation of induction formulas in verification of Prolog programs, ICOT Technical Report TR-094 (1984)
Kapur, D. and Musser, D.R.: Proof by Consistency, Artificial Intelligence 31 (1987) 125–157
Lassez, J.-L. and Maher, M.J.: Closures and fairness in the semantics of programming logic, Theoretical Computer Science 29 (1984) 167–184
Lloyd, J.W.: Foundations of Logic Programming, Springer-Verlag (1984)
Paul, E.: On solving the Equality Problem in Theories Defined by Horn Clauses, Theoretical Computer Science 44 (1986) 127–153
Sakurai, A. and Motoda, H.: Inductionless Induction Method in Prolog, Proc. 4th Conference Proceedings of Japan Society of Software Science and Technology (1987) 231–234
Tamaki, H. and Sato, T.: Unfold/fold transformation of logic programs, Proc. 2nd International Logic Programming Conference (1984) 127–138
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1989 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Sakurai, A., Motoda, H. (1989). Proving definite clauses without explicit use of inductions. In: Furukawa, K., Tanaka, H., Fujisaki, T. (eds) Logic Programming '88. LP 1988. Lecture Notes in Computer Science, vol 383. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-51564-X_52
Download citation
DOI: https://doi.org/10.1007/3-540-51564-X_52
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-51564-7
Online ISBN: 978-3-540-46654-3
eBook Packages: Springer Book Archive