Approximation Fixpoint Theory in Coq: With an Application to Logic Programming

Bart Bogaerts; Luís Cruz-Filipe

doi:10.1007/978-3-031-61716-4_5

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 › Research › peer-review

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.

Original language	English
Book series	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	14560
Pages (from-to)	84-99
Number of pages	16
DOIs	https://doi.org/10.1007/978-3-031-61716-4_5
Publication status	Published - 22 May 2024
Externally published	Yes

Access to Document

10.1007/978-3-031-61716-4_5

Cite this

@article{e01fc8ca4f2f478e8e587473f104946e,

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",

month = may,

day = "22",

doi = "10.1007/978-3-031-61716-4\_5",

language = "English",

volume = "14560",

pages = "84--99",

journal = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

}

Approximation Fixpoint Theory in Coq: With an Application to Logic Programming. / Bogaerts, Bart; Cruz-Filipe, Luís.
In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 14560, 22.05.2024, p. 84-99.

Research output: Journal Article or Conference Article in Journal › Journal article › Research › peer-review

TY - JOUR

T1 - Approximation Fixpoint Theory in Coq: With an Application to Logic Programming

AU - Bogaerts, Bart

AU - Cruz-Filipe, Luís

PY - 2024/5/22

Y1 - 2024/5/22

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-031-61716-4_5

DO - 10.1007/978-3-031-61716-4_5

M3 - Journal article

VL - 14560

SP - 84

EP - 99

JO - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

JF - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

ER -

Approximation Fixpoint Theory in Coq: With an Application to Logic Programming

Abstract

Access to Document

Fingerprint

Cite this