Abstract
We propose in this paper a slight modification of the Knuth and Bendix algorithm for solving the equality problem in non-equational theories defined by a set of Horn clauses. We prove that the completeness property of the algorithm is then preserved, provided that a weak axiomatization of boolean calculus and equality has been given to the algorithm. In particular, we need only the reflexivity axiom for equality.
This algorithm can also be interpreted as the extension to Horn clauses of the resolution/narrowing algorithm proposed by Lankford [LA], which applies only when the equality predicate does not occur positively in non-unit clauses. We give some examples of theorems proved by this method, which show its efficiency in comparison with other paramodulation-based methods.
Another application of the Knuth and Bendix algorithm is the proof by induction (Musser [MU], Huet-Hullot [HH], and others). We show that our version of the completion algorithm can be used for proving universally quantified formulas (not only equations) in the initial model defined by a set of Horn clauses.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Brand D: Proving theorems with the modification method. SIAM J. of Computing, 4 (1975), pp.412–430.
Chang C.L.: The unit proof and the input proof in theorem proving. JACM 17,4 (1970), pp 698–707.
Chang C.L. and Lee R.C.: Symbolic logic and mechanical theorem proving. Academic Press, New-York (1973).
van Emden M.H. and Kowalski R.A.: the Semantics of Predicate Logic as a Programming Language. JACM 23,4 (1976) pp 733–742.
Fribourg L.: oriented equational clauses as a programming language. To appear in Proc. ICALP 84.
Fribourg L.: a narrowing procedure for theories with constructors. Proc. CADE-7, Napa, California, 1984, in Springer-Verlag, Lecture Notes in Computer Science 170, edited by R.E. Shostak.
Hsiang J. and Dershowitz N.: Rewrite methods for clausal and non-clausal theorem proving. Proc. ICALP 83, Spain (1983).
Huet G. and Hullot J.M.: Proofs by induction in equational theories with constructors. JCSS 25-2 (1982).
Huet G., Oppen D.C., Equations and rewrite rules: a survey. In Formal Languages: Perspectives and Open Problems, Edition R.Book, Academic Press (1980).
Huet G.: A complete proof of correctness of the Knuth-Bendix completion algorithm. JCSS 23,1, pp 11–21 (1981).
Henschen L. and Wos L.: Unit Refutations and Horn Sets. JACM, Vol.21, No 4, Oct. 1974, pp. 590–605.
Jouannaud J.P. and Kirchner H.: Completion of a set of rules modulo a set of equations. Proc of POPL (1984).
Knuth D. and Bendix P.: Simple word problems in universal algebra. Computational problems in abstract algebra, Ed. Leech J., Pergamon Press, 1970, 263–297.
Kirchner H. A general inductive completion algorithm and application to abstract data types. Proc. CADE-7, Napa, California, 1984, in Springer-Verlag, Lecture Notes in Computer Science 170, edited by R.E.Shostak.
Lankford D.S.: Canonical inference, Report ATP-32, Department of Mathematics and Computer Science, University of Texas at Austin, Dec.1975.
McCharen J.D., Overbeek R.A. and Wos L.: Problems and Experiments for and with Automated Theorem-Proving Programs. IEEE Transactions on Computers, vol. C-25, No 8, August 1976.
Musser D.R.: On proving inductive properties of abstract data types. Proc. 7th POPL Conference, Las Vegas (1980).
Paul E.: A new interpretation of the resolution principle. Proc. CADE-7, Napa, California, 1984, in Springer-Verlag, Lecture Notes in Computer Science 170, edited by R.E.Shostak. To be published in "Journal of Symbolic Computation"
Paul E.: Proof by induction in equational theories with relations between constructors. Proc. 9th Colloquium on trees in algebra and programming, Bordeaux (March 1984). Cambridge University Press, edited by B.Courcelle.
Peterson G.: A Technique for Establishing Completeness Results in Theorem Proving with Equality. SIAM J. of Computing, 12 (1983), pp 82–100.
Plotkin G.: Building-in equational theories. Machine Intelligence, pp 73–90 (1972). Edinburgh Publisher.
Peterson G. and Stickel M.: Complete sets of reductions for some equational theories. JACM, Vol.28, No2, Avril 1981, pp 233–264.
Remy J.L.: Etude des systemes de reecriture conditionnels et application aux types abstraits algebriques. These docteur es sciences, Centre de recherche en informatique de Nancy, July 1982.
Robinson J.A: A machine-oriented logic based on the resolution principle. JACM, Vol.12, No1, Janvier 1965, pp 23–41
Slagle J.R.: Automatic theorem proving for theories with simplifiers, commutativity and associativity. JACM 21, pp.622–642. (1974)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1985 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Paul, E. (1985). On solving the equality problem in theories defined by Horn clauses. In: Caviness, B.F. (eds) EUROCAL '85. EUROCAL 1985. Lecture Notes in Computer Science, vol 204. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-15984-3_292
Download citation
DOI: https://doi.org/10.1007/3-540-15984-3_292
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-15984-1
Online ISBN: 978-3-540-39685-7
eBook Packages: Springer Book Archive