No CrossRef data available.
Article contents
FO(FD): Extending classical logic with rule-based fixpoint definitions
Published online by Cambridge University Press: 09 July 2010
Abstract
Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.
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).
Information
- 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
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
You have
Access
- 13
- Cited by