Abstract
We interpret Horn clauses as conditional rewrite rules. Then we give sufficient conditions so that the word problem can be decided by conditional normalization in some Horn theory. We also show how to prove theorems in the initial models of Horn theories.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
8. References
FRIBOURG L. SLOG: A logic programming language interpreter based on clausal superposition and rewriting. Proc. of the 1985 Symposium on Logic Programming. Boston, MA pp. 172–184, july 1985.
DERSHOWITZ. N Termination. In: Rewriting Techniques and Applications, J.P. Jouannaud, ed., Lect. Notes in Comp. Sci., vol.202, Springer, 180–224, 1985
GANZINGER. H Ground Term Confluence in Parametric Conditional Equational Specifications, Proceeding of 4th Symposium on Theoretical Aspects of Computer Science Passau, RFA, February 1987
GOGUEN J., MESEGUER J. Eqlog: Equality, Types, and Generic Modules for Logic Programming. J. of Logic Programming, Vol.1, Number 2, pages 179–210, 1984.
HSIANG. J., RUSINOWITCH M. On word problems in equational theories. ICALP 1987
JOUANNAUD J. P., KOUNALIS E. Automatic proofs by induction in equational theories without constructors. Proc. of the Symposim on Logic in Computer Science, Cambridge, MA, pp 358–366, June 1986.
JOUANNAUD. J.P, WALDMANN. B Reductive Conditional Term Rewriting Systems, Proc. 3rd IFIP Conf. on Formal Description of Programming Concepts Lyngby, Danemark, 1986
HUET G., Confluent reduction: abstract properties and applications to term-rewriting systems. JACM 27, 797–821. (1980).
KAPLAN S. Simplifying Conditional Term Rewriting Systems: Unification, Termination Confluence, to appear in J. of Symb Comp.
KNUTH. D, BENDIX. P Simple Word Problems in Abstract Algebra, Leech J.ed, Pergamon Press, pp. 263–297, 1970
KOUNALIS E., RUSINOWITCH M., On words problems in Horn theories, to appear as rapport INRIA. Nancy (1988).
KUCHLIN, W. A confluence criterion based on the generalised Newman lemma. proc. of EUROCAL, B.Caviness, LNCS 204, (1985) pp. 390–399.
LANKFORD D. S. Canonical inference. Memo ATP-32, Dept. of Math. and Comp. Sc., University of Texas, Austin, Texas, 1975.
PADAWITZ P. Horn Clause specifications: a uniform framework for abstract data types and logic programming. Universitat Passau, MIP-8516 December 1985.
PLOTKIN, G. Building-in equational theories, Machine Intelligence 7, B. Meltzer and D. Mitchie,eds, American Elsevier, New-York (1972) pp. 73–90.
REITER R. On closed world databases, in "Logic and databases. eds Gallaire H., Minker J. Plenum Press, New York 55–76(1978).
REMY, J.L Etude des syste`mes de re'e'criture conditionnelle et applications aux types abstraits alge'briques, The`se d'Etat, I.N.P.L, Nancy, 1982
RUSINOWITCH. M, Demonstration automatique par des techniques de Re'e'criture. Thesis. Universite' de Nancy 1, 1987.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1988 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kounalis, E., Rusinowitch, M. (1988). On word problems in Horn theories. In: Lusk, E., Overbeek, R. (eds) 9th International Conference on Automated Deduction. CADE 1988. Lecture Notes in Computer Science, vol 310. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0012854
Download citation
DOI: https://doi.org/10.1007/BFb0012854
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-19343-2
Online ISBN: 978-3-540-39216-3
eBook Packages: Springer Book Archive