@inbook{6655ba65a2084d1981db1ce83418d86a,
title = "Approximation Fixpoint Theory in Coq: With an Application to Logic Programming",
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.",
author = "Bart Bogaerts and Lu{\'i}s Cruz-Filipe",
year = "2024",
doi = "10.1007/978-3-031-61716-4_5",
language = "English",
isbn = "978-3-031-61715-7",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Science+Business Media",
pages = "84--99",
editor = "Venanzio Capretta and Krebbers, {Robbert } and Wiedijk, { Freek }",
booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
address = "United States",
}