Skip to main content
SpringerLink
Log in

Reducing Inductive Definitions to Propositional Satisfiability

  • Conference paper
Logic Programming (ICLP 2005)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 3668))

Included in the following conference series:

Abstract

The FO(ID) logic is an extension of classical first-order logic with a uniform representation of various forms of inductive definitions. The definitions are represented as sets of rules and they are interpreted by two-valued well-founded models. For a large class of combinatorial and search problems, knowledge representation in FO(ID) offers a viable alternative to the paradigm of Answer Set Programming. The main reasons are that (i) the logic is an extension of classical logic and (ii) the semantics of the language is based on well-understood principles of mathematical induction.

In this paper, we define a reduction from the propositional fragment of FO(ID) to SAT. The reduction is based on a novel characterization of two-valued well-founded models using a set of inequality constraints on level mappings associated with the atoms. We also show how the reduction to SAT can be adapted for logic programs under the stable model semantics. Our experiments show that when using a state of the art SAT solver both reductions are competitive with other answer set programming systems — both direct implementations and SAT based.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Baral, C.: Knowledge Representation, Reasoning and Declarative Problem Solving. Cambridge University Press, Cambridge (2003)

    Book  MATH  Google Scholar 

  2. Ben-Eliyahu, R., Dechter, R.: Propositional semantics for disjunctive logic programs. Annals of Mathematics and Artificial Intelligence 12(1–2), 53–87 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  3. Brachman, R.J., Levesque, H.: Competence in knowledge representation. Proc. of the National Conference on Artificial Intelligence, 189–192 (1982)

    Google Scholar 

  4. Denecker, M.: Extending classical logic with inductive definitions. In: Palamidessi, C., Moniz Pereira, L., Lloyd, J.W., Dahl, V., Furbach, U., Kerber, M., Lau, K.-K., Sagiv, Y., Stuckey, P.J. (eds.) CL 2000. LNCS (LNAI), vol. 1861, pp. 703–717. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  5. Denecker, M., Ternovska, E.: Inductive situation calculus. In: Principles of Knowledge Representation and Reasoning: Proc. of the 9th International Conference, pp. 545–553. AAAI Press, Menlo Park (2004)

    Google Scholar 

  6. Denecker, M., Ternovska, E.: A logic of non-monotone inductive definitions and its modularity properties. In: Lifschitz, V., Niemelä, I. (eds.) LPNMR 2004. LNCS (LNAI), vol. 2923, pp. 47–60. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  7. Denecker, M., Theseider Dupré, D., Van Belleghem, K.: An inductive definition approach to ramifications. Linköping Electronic Articles in Computer and Information Science 3(7), 1–43 (1998), http://www.ep.liu.se/ea/cis/1998/007/

    Google Scholar 

  8. Erdem, E., Lifschitz, V.: Tight logic programs. Theory and Practice of Logic Programming 3(4–5), 499–518 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  9. Fages, F.: Consistency of Clark’s completion and existence of stable models. Journal of Methods of Logic in Computer Science 1, 51–60 (1994)

    Google Scholar 

  10. Gelfond, M., Lifschitz, V.: The stable model semantics for logic programming. In: Logic Programming, 5th International Conference and Symposium, pp. 1070–1080 (1988)

    Google Scholar 

  11. Janhunen, T.: Representing normal programs with clauses. In: Proc. of the 16th European Conference on Artificial Intelligence, pp. 358–362 (2004)

    Google Scholar 

  12. Lierler, Y., Maratea, M.: Cmodels-2: SAT-based answer set solver enhanced to non-tight programs. In: Lifschitz, V., Niemelä, I. (eds.) LPNMR 2004. LNCS (LNAI), vol. 2923, pp. 346–350. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  13. Lin, F., Zhao, J.: On tight logic programs and yet another translation from normal logic programs to propositional logic. In: International Joint Conference on Artificial Intelligence, pp. 853–858. Morgan Kaufmann, San Francisco (2003)

    Google Scholar 

  14. Lin, F., Zhao, Y.: ASSAT: Computing answer sets of a logic program by SAT solvers. Artificial Intelligence 157(1–2), 115–137 (2004)

    Article  MATH  MathSciNet  Google Scholar 

  15. Linke, T., Tompits, H., Woltran, S.: On acyclic and head-cycle free nested logic programs. In: Demoen, B., Lifschitz, V. (eds.) ICLP 2004. LNCS, vol. 3132, pp. 225–239. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  16. Mariën, M., Gilis, D., Denecker, M.: On the relation between ID-Logic and Answer Set Programming. In: Alferes, J.J., Leite, J. (eds.) JELIA 2004. LNCS (LNAI), vol. 3229, pp. 108–120. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  17. Mitchell, D., Ternovska, E.: A framework for representing and solving NP-search problems. In: Proc. of the National Conference on Artificial Intelligence, pp. 430–435 (2005)

    Google Scholar 

  18. Niemelä, I.: Logic programs with stable model semantics as a constraint programming paradigm. Annals of Mathematics and Artificial Intelligence 25(3,4), 241–273 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  19. Ryan, L.: Efficient algorithms for clause-learning SAT solvers. Master’s thesis, Simon Fraser University, Burnaby, Canada (2004)

    Google Scholar 

  20. Simons, P., Niemelä, I., Soininen, T.: Extending and implementing the stable model semantics. Artificial Intelligence 138(1–2), 181–234 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  21. Ternovskaia, E.: Causality via inductive definitions. In: Working Notes of ”Prospects for a Commonsense Theory of Causation”. AAAI Spring Symposium Series, pp. 94–100 (1998)

    Google Scholar 

  22. Ternovskaia, E.: ID-logic and the ramification problem for the situation calculus. In: Proc. of the 14th European Conference on Artificial Intelligence, pp. 563–567 (2000)

    Google Scholar 

  23. Van Gelder, A., Ross, K.A., Schlipf, J.S.: The well-founded semantics for general logic programs. Journal of the ACM 38(3), 620–650 (1991)

    MATH  Google Scholar 

  24. Van Nuffelen, B., Cortés-Calabuig, A., Denecker, M., Arieli, O., Bruynooghe, M.: Data integration ising ID-logic. In: Persson, A., Stirna, J. (eds.) CAiSE 2004. LNCS, vol. 3084, pp. 67–81. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Computing Science, Simon Fraser University, Vancouver, Canada

    Nikolay Pelov & Eugenia Ternovska

Authors
  1. Nikolay Pelov
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Eugenia Ternovska
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Dipartimento di Scienze dell’Informazione, Università di Bologna, Italy

    Maurizio Gabbrielli

  2. Department of Computer Science, University of Texas at Dallas, 75080, Richardson, TX

    Gopal Gupta

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Pelov, N., Ternovska, E. (2005). Reducing Inductive Definitions to Propositional Satisfiability. In: Gabbrielli, M., Gupta, G. (eds) Logic Programming. ICLP 2005. Lecture Notes in Computer Science, vol 3668. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11562931_18

Download citation

  • DOI: https://doi.org/10.1007/11562931_18

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-29208-1

  • Online ISBN: 978-3-540-31947-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation