SpringerLink
Log in

Approximation Fixpoint Theory in Coq

With an Application to Logic Programming

  • Chapter
  • First Online:
Logics and Type Systems in Theory and Practice

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 14560))

  • 97 Accesses

Abstract

Approximation Fixpoint Theory (AFT) is an abstract framework based on lattice theory that unifies semantics of different non-monotonic logic. AFT has revealed itself to be applicable in a variety of new domains within knowledge representation. In this work, we present a formalisation of the key constructions and results of AFT in the Coq theorem prover, together with a case study illustrating its application to propositional logic programming.

This work was partially supported by Fonds Wetenschappelijk Onderzoek – Vlaanderen (project G0B2221N).

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
EUR 32.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or Ebook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 99.00
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 129.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free ship** worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    While a bilattice is usually defined as an arbitrary set with two compatible orders, AFT is only concerned with bilattices that are in fact square lattices; i.e., the underlying set is of the form \(L^2\).

  2. 2.

    Throughout this presentation we write ... for additional arguments that are left out for conciseness; we leave some arguments implicit when they can be inferred from the context by a human (even if not by Coq); we omit universally quantified variables at the top of lemmas; and we ignore namespace clashes that force us to include module names in the Coq source.

  3. 3.

    Disjointness of this lists is called consistency in the original reference.

References

  1. Antic, C., Eiter, T., Fink, M.: Hex semantics via approximation fixpoint theory. In: Cabalar, P., Son, T.C. (eds.) Logic Programming and Nonmonotonic Reasoning. Lecture Notes in Computer Science(), vol. 8148, pp. 102–115. Springer, Berlin (2013). https://doi.org/10.1007/978-3-642-40564-8_11

    Chapter  Google Scholar 

  2. Barras, B.: Sets in Coq, Coq in sets. J. Formaliz. Reason 3(1), 29–48 (2010)

    MathSciNet  Google Scholar 

  3. Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development - Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series, Springer, Cham (2004)

    Google Scholar 

  4. Blanqui, F., Koprowski, A.: CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates. Math. Struct. Comput. Sci. 21(4), 827–859 (2011)

    Article  MathSciNet  Google Scholar 

  5. Bogaerts, B., Cruz-Filipe, L.: Fixpoint semantics for active integrity constraints. Artif. Intell. 255, 43–70 (2018). https://doi.org/10.1016/j.artint.2017.11.003

    Article  MathSciNet  Google Scholar 

  6. Bogaerts, B., Cruz-Filipe, L.: Stratification in approximation fixpoint theory and its application to active integrity constraints. ACM Trans. Comput. Log. 22(1), 1–19 (2021). https://doi.org/10.1145/3430750

    Article  MathSciNet  Google Scholar 

  7. Bogaerts, B., Cruz-Filipe, L.: A formalisation of approximation fixpoint theory in Coq (2024). https://doi.org/10.5281/zenodo.10709613

  8. Bogaerts, B., Jakubowski, M.: Fixpoint semantics for recursive SHACL. In: Formisano, A., et al. (eds.) Proceedings 37th International Conference on Logic Programming (Technical Communications), ICLP Technical Communications 2021, Porto (virtual event), 20-27th September 2021. EPTCS, vol. 345, pp. 41–47 (2021). https://doi.org/10.4204/EPTCS.345.14

  9. Bogaerts, B., Vennekens, J., Denecker, M.: Grounded fixpoints and their applications in knowledge representation. Artif. Intell. 224, 51–71 (2015). https://doi.org/10.1016/j.artint.2015.03.006

    Article  MathSciNet  Google Scholar 

  10. Bogaerts, B., Vennekens, J., Denecker, M.: Safe inductions and their applications in knowledge representation. Artif. Intell. 259, 167–185 (2018). http://www.sciencedirect.com/science/article/pii/S000437021830122X

  11. Charalambidis, A., Rondogiannis, P., Symeonidou, I.: Approximation fixpoint theory and the well-founded semantics of higher-order logic programs. Theory Pract. Log. Program. 18(3–4), 421–437 (2018). https://doi.org/10.1017/S1471068418000108

    Article  MathSciNet  Google Scholar 

  12. Denecker, M., Marek, V., Truszczyński, M.: Approximations, stable operators, well-founded fixpoints and applications in nonmonotonic reasoning. In: Minker, J. (ed.) Logic-Based Artificial Intelligence. The Springer International Series in Engineering and Computer Science, vol. 597, pp. 127–144. Springer, Boston (2000). https://doi.org/10.1007/978-1-4615-1567-8_6

    Chapter  Google Scholar 

  13. Denecker, M., Marek, V., Truszczyński, M.: Uniform semantic treatment of default and autoepistemic logics. Artif. Intell. 143(1), 79–122 (2003). https://doi.org/10.1016/S0004-3702(02)00293-X

    Article  MathSciNet  Google Scholar 

  14. Denecker, M., Marek, V., Truszczyński, M.: Reiter’s default logic is a logic of autoepistemic reasoning and a good one, too. In: Brewka, G., Marek, V., Truszczyński, M. (eds.) Nonmonotonic Reasoning – Essays Celebrating Its 30th Anniversary, pp. 111–144. College Publications (2011). http://arxiv.org/abs/1108.3278

  15. Denecker, M., Vennekens, J.: Well-founded semantics and the algebraic theory of non-monotone inductive definitions. In: Baral, C., Brewka, G., Schlipf, J.S. (eds.) LPNMR. Lecture Notes in Computer Science, vol. 4483, pp. 84–96. Springer, Cham (2007). https://doi.org/10.1007/978-3-540-72200-7_9

    Chapter  Google Scholar 

  16. Fitting, M.: Fixpoint semantics for logic programming – a survey. Theor. Comput. Sci. 278(1–2), 25–51 (2002). https://doi.org/10.1016/S0304-3975(00)00330-3

    Article  MathSciNet  Google Scholar 

  17. Gelfond, M., Lifschitz, V.: The stable model semantics for logic programming. In: Kowalski, R.A., Bowen, K.A. (eds.) ICLP/SLP, pp. 1070–1080. MIT Press, Cambridge (1988). http://citeseer.ist.psu.edu/viewdoc/summary?nodoi=10.1.1.24.6050

  18. Grall, H.: Proving fixed points. Technical Report. HAL-00507775, HAL archives ouvertes (2010)

    Google Scholar 

  19. Grimm, J.: Implementation of three types of ordinals in Coq. Technical Report. RR-8407, INRIA (2013)

    Google Scholar 

  20. Heyninck, J., Bogaerts, B.: Non-deterministic approximation operators: ultimate operators, semi-equilibrium semantics and aggregates (full version). CoRR abs/2305.10846 (2023). https://doi.org/10.48550/ar**v.2305.10846

  21. de Jong, T., Kraus, N., Forsberg, F.N., Xu, C.: Set-theoretic and type-theoretic ordinals coincide. In: LICS, pp. 1–13 (2023).https://doi.org/10.1109/LICS56636.2023.10175762

  22. Konolige, K.: On the relation between default and autoepistemic logic. Artif. Intell. 35(3), 343–382 (1988). https://doi.org/10.1016/0004-3702(88)90021-5

    Article  MathSciNet  Google Scholar 

  23. Kuratowski, C.: Une méthode d’élimination des nombres transfinis des raisonnements mathématiques. Fundamenta Mathematicae 3(1), 76–108 (1922). http://eudml.org/doc/213282

  24. Liu, F., Bi, Y., Chowdhury, M.S., You, J., Feng, Z.: Flexible approximators for approximating fixpoint theory. In: Khoury, R., Drummond, C. (eds.) Advances in Artificial Intelligence. Lecture Notes in Computer Science(), vol. 9673, pp. 224–236. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-34111-8_28

    Chapter  Google Scholar 

  25. Blanqui, F.: https://github.com/fblanqui/color/blob/master/Util/Relation/Tarski.v. Accessed 02 June 2021

  26. Castéran, P.: https://github.com/coq-community/hydra-battles/tree/master/theories/ordinals. Accessed 02 June 2021

  27. Moore, R.C.: Semantical considerations on nonmonotonic logic. Artif. Intell. 25(1), 75–94 (1985). https://doi.org/10.1016/0004-3702(85)90042-6

    Article  MathSciNet  Google Scholar 

  28. Pelov, N., Denecker, M., Bruynooghe, M.: Well-founded and stable semantics of logic programs with aggregates. TPLP 7(3), 301–353 (2007). https://doi.org/10.1017/S1471068406002973

    Article  MathSciNet  Google Scholar 

  29. Reiter, R.: A logic for default reasoning. Artif. Intell. 13(1–2), 81–132 (1980). https://doi.org/10.1016/0004-3702(80)90014-4

    Article  MathSciNet  Google Scholar 

  30. Simpson, C.: Set-theoretical mathematics in Coq. CoRR abs/math/0402336 (2004)

    Google Scholar 

  31. Strass, H.: Approximating operators and semantics for abstract dialectical frameworks. Artif. Intell. 205, 39–70 (2013). https://doi.org/10.1016/j.artint.2013.09.004

    Article  MathSciNet  Google Scholar 

  32. Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pac. J. Math. (1955)

    Google Scholar 

  33. Truszczyński, M.: Strong and uniform equivalence of nonmonotonic theories - an algebraic approach. Ann. Math. Artif. Intell. 48(3–4), 245–265 (2006). https://doi.org/10.1007/s10472-007-9049-2

    Article  MathSciNet  Google Scholar 

  34. van Emden, M.H., Kowalski, R.A.: The semantics of predicate logic as a programming language. J. ACM 23(4), 733–742 (1976). https://doi.org/10.1145/321978.321991

    Article  MathSciNet  Google Scholar 

  35. Van Gelder, A., Ross, K.A., Schlipf, J.S.: The well-founded semantics for general logic programs. J. ACM 38(3), 620–650 (1991). https://doi.org/10.1145/116825.116838

    Article  MathSciNet  Google Scholar 

  36. Van Hertum, P., Cramer, M., Bogaerts, B., Denecker, M.: Distributed autoepistemic logic and its application to access control. In: Kambhampati, S. (ed.) Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, IJCAI 2016, New York, NY, USA, 9-15 July 2016, pp. 1286–1292. IJCAI/AAAI Press (2016). http://www.ijcai.org/Abstract/16/186

  37. Vennekens, J., Gilis, D., Denecker, M.: Splitting an operator: algebraic modularity results for logics with fixpoint semantics. ACM Trans. Comput. Log. 7(4), 765–797 (2006). https://doi.org/10.1145/1182613.1189735

    Article  MathSciNet  Google Scholar 

  38. Vennekens, J., Mariën, M., Wittocx, J., Denecker, M.: Predicate introduction for logics with a fixpoint semantics. Parts I and II. Fund. Inform. 79(1–2), 187–227 (2007)

    MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department Computer Science, Vrije Universiteit Brussel (VUB), Pleinlaan 2, 1050, Brussels, Belgium

    Bart Bogaerts

  2. Department Mathematics and Computer Science, University of Southern Denmark, Campusvej 55, 5230, Odense, Denmark

    Luís Cruz-Filipe

Authors
  1. Bart Bogaerts
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Luís Cruz-Filipe
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Luís Cruz-Filipe .

Editor information

Editors and Affiliations

  1. University of Nottingham, Nottingham, UK

    Venanzio Capretta

  2. Radboud University Nijmegen, Nijmegen, The Netherlands

    Robbert Krebbers

  3. Radboud University Nijmegen, Nijmegen, The Netherlands

    Freek Wiedijk

Rights and permissions

Reprints and permissions

Copyright information

© 2024 The Author(s), under exclusive license to Springer Nature Switzerland AG

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Bogaerts, B., Cruz-Filipe, L. (2024). Approximation Fixpoint Theory in Coq. In: Capretta, V., Krebbers, R., Wiedijk, F. (eds) Logics and Type Systems in Theory and Practice. Lecture Notes in Computer Science, vol 14560. Springer, Cham. https://doi.org/10.1007/978-3-031-61716-4_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-61716-4_5

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-61715-7

  • Online ISBN: 978-3-031-61716-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation