Hostname: page-component-586b7cd67f-dlnhk Total loading time: 0 Render date: 2024-11-27T22:15:19.456Z Has data issue: false hasContentIssue false
  • English
  • Français

FO(FD): Extending classical logic with rule-based fixpoint definitions

Published online by Cambridge University Press:  09 July 2010

PING HOU ,
BROES DE CAT  and
MARC DENECKER
PING HOU
Affiliation:
Department of Computer Science, K.U. Leuven, Belgium (e-mail: [email protected], [email protected], [email protected])
BROES DE CAT
Affiliation:
Department of Computer Science, K.U. Leuven, Belgium (e-mail: [email protected], [email protected], [email protected])
MARC DENECKER
Affiliation:
Department of Computer Science, K.U. Leuven, Belgium (e-mail: [email protected], [email protected], [email protected])
Get access Rights & Permissions [Opens in a new window]

Abstract

We introduce fixpoint definitions, a rule-based reformulation of fixpoint constructs. The logic FO(FD), an extension of classical logic with fixpoint definitions, is defined. We illustrate the relation between FO(FD) and FO(ID), which is developed as an integration of two knowledge representation paradigms. The satisfiability problem for FO(FD) is investigated by first reducing FO(FD) to difference logic and then using solvers for difference logic. These reductions are evaluated in the computation of models for FO(FD) theories representing fairness conditions and we provide potential applications of FO(FD).

Keywords

fixpoint constructsfixpoint definitionsclassical logic extensions
Type
Regular Papers
Information
Theory and Practice of Logic Programming , Volume 10 , Special Issue 4-6: 26th International Conference on Logic Programming , July 2010 , pp. 581 - 596
Copyright
Copyright © Cambridge University Press 2010

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Abiteboul, S., Hull, R., and Vianu, V. 1995. Foundations of Databases. Addison-Wesley.Google Scholar
Baader, F., Calvanese, D., McGuinness, D. L., Nardi, D., and Patel-Schneider, P. F., Eds. 2003. The Description Logic Handbook: Theory, Implementation, and Applications. Cambridge University Press.Google Scholar
Baelde, D. and Miller, D. 2007. Least and greatest fixed points in linear logic. In LPAR, Derschowitz, N. and Voronkov, A., Eds. LNCS, vol. 4790. Springer, 92–106.Google Scholar
Baral, C. 2003. Knowledge Representation, Reasoning and Declarative Problem Solving. Cambridge University Press.CrossRefGoogle Scholar
Barwise, J. and Moss, L. S., Eds. 1996. Vicious Circles: On the mathematics of Non-Wellfounded Phenomena. University of Chicago Press.Google Scholar
Bradfield, J. C. 1996. The modal mu-calculus alternation hierarchy is strict. In CONCUR, Montanari, U. and Sassone, V., Eds. LNCS, vol. 1119. Springer, 233–246.Google Scholar
Clark, K. L. 1978. Negation as failure. In Logic and Data Bases. Plenum Press, 293–322.Google Scholar
Cotton, S. and Maler, O. 2006. Fast and flexible difference constraint propagation for DPLL(T). In SAT, Biere, A. and Gomes, C. P., Eds. LNCS, vol. 4121. Springer, 170–183.Google Scholar
Denecker, M. 2000. Extending classical logic with inductive definitions. In CL, Lloyd, J. W., Dahl, V., Furbach, U., Kerber, M., Lau, K.-K., Palamidessi, C., Pereira, L. M., Sagiv, Y., and Stuckey, P. J., Eds. LNCS, vol. 1861. Springer, 703–717.Google Scholar
Denecker, M. and Ternovska, E. 2008. A logic of nonmonotone inductive definitions. ACM Transactions on Computational Logic (TOCL) 9, 2, Article 14.CrossRefGoogle Scholar
Friedmann, O. and Lange, M. 2009. Solving parity games in practice. In ATVA, Liu, Z. and Ravn, A. P., Eds. LNCS, vol. 5799. Springer, 182–196.Google Scholar
Gupta, G., Bansal, A., Min, R., Simon, L., and Mallya, A. 2007. Coinductive logic programming and its applications. In ICLP, Dahl, V. and Niemelä, I., Eds. LNCS, vol. 4670. Springer, 27–44.Google Scholar
Janhunen, T., Niemelä, I., and Sevalnev, M. 2009. Computing stable models via reductions to difference logic. In LPNMR, Erdem, E., Lin, F., and Schaub, T., Eds. LNCS, vol. 5753. Springer, 142–154.Google Scholar
Kakas, A. C., Kowalski, R. A., and Toni, F. 1992. Abductive logic programming. Journal of Logic and Computation 2, 6, 719–770.CrossRefGoogle Scholar
Keinänen, M. and Niemelä, I. 2004. Solving alternating boolean equation systems in answer set programming. In INAP/WLP, Seipel, D., Hanus, M., Geske, U., and Bartenstein, O., Eds. LNCS, vol. 3392. Springer, 134–148.Google Scholar
Liu, X., Ramakrishnan, C. R., and Smolka, S. A. 1998. Fully local and efficient evaluation of alternating fixed points (extended abstract). In TACAS, Steffen, B., Ed. LNCS, vol. 1384. Springer, 5–19.Google Scholar
McCarthy, J. 1986. Applications of circumscription to formalizing common-sense knowledge. Artificial Intelligence 28, 1, 89–116.Google Scholar
Niemelä, I. 2008. Stable models and difference logic. Annals of Mathematics and Artificial Intelligence 53, 1–4, 313–329.CrossRefGoogle Scholar
Nieuwenhuis, R. and Oliveras, A. 2005. DPLL(T) with exhaustive theory propagation and its application to difference logic. In CAV, Etessami, K. and Rajamani, S. K., Eds. LNCS, vol. 3576. Springer, 321–334.Google Scholar
Park, D. 1969. Fixpoint induction and proofs of program properties. Machine Intelligence 5, 59–78.Google Scholar
Schlipf, J. S. 1995. The expressive powers of the logic programming semantics. Journal of Computer and System Sciences 51, 1, 64–86.Google Scholar
Syrjänen, T. and Niemelä, I. 2001. The smodels system. In LPNMR, Eiter, T., Faber, W., and Truszczyński, M., Eds. LNCS, vol. 2173. Springer, 434–438.Google Scholar
Tarjan, R. E. 1972. Depth-first search and linear graph algorithms. SIAM Journal on Computing 1, 2, 146–160.Google Scholar
Tseitin, G. S. 1968. On the complexity of derivation in propositional calculus. In Studies in Constructive Mathematics and Mathematical Logic II, Slisenko, A. O., Ed. Consultants Bureau, N.Y., 115–125.Google Scholar
Vennekens, J. and Denecker, M. 2009. FO(ID) as an extension of DL with rules. In ESWC, Aroyo, L., Traverso, P., Ciravegna, F., Cimiano, P., Heath, T., Hyvönen, E., Mizoguchi, R., Oren, E., Sabou, M., and Simperl, E. P. B., Eds. LNCS, vol. 5554. Springer, 384–398.Google Scholar
Wittocx, J., Mariën, M., and Denecker, M. 2008. Grounding with bounds. In AAAI, Fox, D. and Gomes, C. P., Eds. AAAI Press, 572–577.Google Scholar