Approximation Fixpoint Theory in Coq: With an Application to Logic Programming
- Bart Bogaerts,
- Luís Cruz-Filipe
- University Libre du Bruxelles,
- University of Southern Denmark
Research Output:
Journal Article or Conference Article in Journal
Journal article
Peer-reviewPublication Information
Output type
Research Output:
Journal Article or Conference Article in Journal
Journal article
Peer-reviewOriginal language
EnglishPages from-to (Number of pages)
Pages 84-99 (16 pages)Journal (Volume, Issue Number)
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Volume 14560)Publication milestones
- Published - 22/05/2024
Publication status
Published - 22/05/2024
Publication IDs
- Scopus: 85195935389
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.
Publication metrics
PlumX, opens in new tab
Citations
1