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

Publikation: Artikel i tidsskrift og konference artikel i tidsskrift › Tidsskriftartikel › Forskning › 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.

Originalsprog	Engelsk
Tidsskrift	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Vol/bind	14560
Sider (fra-til)	84-99
Antal sider	16
DOI	https://doi.org/10.1007/978-3-031-61716-4_5
Status	Udgivet - 22 maj 2024
Udgivet eksternt	Ja

Adgang til dokumentet

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

Citationsformater

@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.
I: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Bind 14560, 22.05.2024, s. 84-99.

Publikation: Artikel i tidsskrift og konference artikel i tidsskrift › Tidsskriftartikel › Forskning › 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

Adgang til dokumentet

Fingeraftryk

Citationsformater