Abstract
The standard semantics of a logical program described by a set of predicative Horn clauses is minimal model semantics. To reason about negation in this context, Clark proposed to enrich the description in such a way that all Herbrand models but the minimal one are excluded. This predicate completion is used in explicit negation as failure, and also for example by Comon and Nieuwenhuis in inductive theorem proving.
In this article, I extend predicate completion to a class of non-Horn clause sets. These may have several minimal models and I show how predicate completion with respect to a ground total reduction ordering singles out the same model as the model construction procedure by Bachmair and Ganzinger.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. J. of Logic and Computation 4(3), 217–247 (1994)
Bachmair, L., Plaisted, D.A.: Associative path orderings. In: Jouannaud, J.-P. (ed.) RTA 1985. LNCS, vol. 202, pp. 241–254. Springer, Heidelberg (1985)
Clark, K.L.: Negation as failure. In: Gallaire, H., Minker, J. (eds.) Logic and Data Bases, pp. 293–322. Plenum Press, New York (1977)
Comon, H., Delor, C.: Equational formulae with membership constraints. Information and Computation 112(2), 167–216 (1994)
Comon, H., Lescanne, P.: Equational problems and disunification. Journal of Symbolic Computation 7(3-4), 371–425 (1989)
Comon, H., Nieuwenhuis, R.: Induction = I-Axiomatization + First-Order Consistency. Information and Computation 159(1/2), 151–186 (2000)
Ganzinger, H., Stuber, J.: Inductive theorem proving by consistency for first-order clauses. In: Rusinowitch, M., Remy, J.-L. (eds.) CTRS 1992. LNCS, vol. 656, pp. 226–241. Springer, Heidelberg (1993)
Gelfond, M., Lifschitz, V.: Representing action and change by logic programs. Journal of Logic Programming 17(2/3&4), 301–321 (1993)
Horbach, M.: Disunification for ultimately periodic interpretations. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS (LNAI), vol. 6355, pp. 290–311. Springer, Heidelberg (2010)
Horbach, M.: System description: SPASS-FD. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 315–321. Springer, Heidelberg (2011)
Horbach, M., Weidenbach, C.: Decidability results for saturation-based model building. In: Schmidt, R. (ed.) CADE-22. LNCS (LNAI), vol. 5663, pp. 404–420. Springer, Heidelberg (2009)
Horbach, M., Weidenbach, C.: Superposition for fixed domains. ACM Transactions on Computational Logic 11(4), 27:1–27:35 (2010)
Ludwig, M., Hustadt, U.: Resolution-based model construction for PLTL. In: Lutz, C., Raskin, J.-F. (eds.) TIME 2009, pp. 73–80. IEEE Computer Society, Los Alamitos (2009)
McCarthy, J.: Applications of circumscription to formalizing common sense knowledge. Artificial Intelligence 28, 89–116 (1986)
Nie, X.: Non-horn clause logic programming. Artificial Intelligence 92(1-2), 243–258 (1997)
Reiter, R.: A logic for default reasoning. Artificial Intelligence 13(1-2), 81–132 (1980)
Reiter, R.: Circumscription implies predicate completion (sometimes). In: Waltz, D.L. (ed.) AAAI, pp. 418–420. AAAI Press, Menlo Park (1982)
Stuckey, P.J.: Constructive negation for constraint logic programming. In: LICS, pp. 328–339. IEEE Computer Society, Los Alamitos (1991)
Togashi, A., Hou, B.-H., Noguchi, S.: Generalized predicate completion. In: Ramani, S., Anjaneyulu, K., Chandrasekar, R. (eds.) KBCS 1989. LNCS, vol. 444, pp. 286–295. Springer, Heidelberg (1990)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Horbach, M. (2011). Predicate Completion for non-Horn Clause Sets. In: Bjørner, N., Sofronie-Stokkermans, V. (eds) Automated Deduction – CADE-23. CADE 2011. Lecture Notes in Computer Science(), vol 6803. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-22438-6_24
Download citation
DOI: https://doi.org/10.1007/978-3-642-22438-6_24
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-22437-9
Online ISBN: 978-3-642-22438-6
eBook Packages: Computer ScienceComputer Science (R0)