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

Bart Bogaerts; Luis Cruz-Filipe

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

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

Bart Bogaerts, Luis Cruz-Filipe

Research output: Chapter in Book/Report/Conference proceeding › Chapter › Research › peer-review

1 Citation (Scopus)

78 Downloads (Pure)

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
Title of host publication	Logics and Type Systems in Theory and Practice
Subtitle of host publication	Essays Dedicated to Herman Geuvers on The Occasion of His 60th Birthday
Publisher	Springer
Pages	84-99
Number of pages	16
ISBN (Electronic)	9783031617164
ISBN (Print)	9783031617157
DOIs	https://doi.org/10.1007/978-3-031-61716-4_5
Publication status	Published - 2024
Event	Workshop 60th Birthday Herman Geuvers - Nijmegen, Nijmegen, Netherlands Duration: 29 May 2024 → 29 May 2024 https://robbertkrebbers.nl/geuversfest/

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	14560 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	Workshop 60th Birthday Herman Geuvers
Country/Territory	Netherlands
City	Nijmegen
Period	29/05/24 → 29/05/24
Internet address	https://robbertkrebbers.nl/geuversfest/

Bibliographical note

Funding Information:
This work was partially supported by Fonds Wetenschappelijk Onderzoek \u2013 Vlaanderen (project G0B2221N).

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

Access to Document

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

FormalisingAFTinCOQAccepted author manuscript, 420 KB

Handle.net

Persistent link

Cite this

Bogaerts, B., & Cruz-Filipe, L. (2024). Approximation Fixpoint Theory in Coq: with an Application to Logic Programming. In Logics and Type Systems in Theory and Practice: Essays Dedicated to Herman Geuvers on The Occasion of His 60th Birthday (pp. 84-99). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 14560 LNCS). Springer. https://doi.org/10.1007/978-3-031-61716-4_5

Bogaerts, Bart ; Cruz-Filipe, Luis. / Approximation Fixpoint Theory in Coq : with an Application to Logic Programming. Logics and Type Systems in Theory and Practice: Essays Dedicated to Herman Geuvers on The Occasion of His 60th Birthday. Springer, 2024. pp. 84-99 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inbook{fa6fdd8a7b29419cbc6748349a5ea48c,

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 Luis Cruz-Filipe",

note = "Funding Information: This work was partially supported by Fonds Wetenschappelijk Onderzoek \u2013 Vlaanderen (project G0B2221N). Publisher Copyright: {\textcopyright} The Author(s), under exclusive license to Springer Nature Switzerland AG 2024.; Workshop 60th Birthday Herman Geuvers ; Conference date: 29-05-2024 Through 29-05-2024",

year = "2024",

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

language = "English",

isbn = "9783031617157 ",

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

publisher = "Springer",

pages = "84--99",

booktitle = "Logics and Type Systems in Theory and Practice",

url = "https://robbertkrebbers.nl/geuversfest/",

}

Bogaerts, B & Cruz-Filipe, L 2024, Approximation Fixpoint Theory in Coq: with an Application to Logic Programming. in Logics and Type Systems in Theory and Practice: Essays Dedicated to Herman Geuvers on The Occasion of His 60th Birthday. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 14560 LNCS, Springer, pp. 84-99, Workshop 60th Birthday Herman Geuvers, Nijmegen, Netherlands, 29/05/24. https://doi.org/10.1007/978-3-031-61716-4_5

Approximation Fixpoint Theory in Coq: with an Application to Logic Programming. / Bogaerts, Bart; Cruz-Filipe, Luis.
Logics and Type Systems in Theory and Practice: Essays Dedicated to Herman Geuvers on The Occasion of His 60th Birthday. Springer, 2024. p. 84-99 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 14560 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Chapter › Research › peer-review

TY - CHAP

T1 - Approximation Fixpoint Theory in Coq

T2 - Workshop 60th Birthday Herman Geuvers

AU - Bogaerts, Bart

AU - Cruz-Filipe, Luis

N1 - Funding Information: This work was partially supported by Fonds Wetenschappelijk Onderzoek \u2013 Vlaanderen (project G0B2221N). Publisher Copyright: © The Author(s), under exclusive license to Springer Nature Switzerland AG 2024.

PY - 2024

Y1 - 2024

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.

UR - http://www.scopus.com/inward/record.url?scp=85195935389&partnerID=8YFLogxK

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

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

M3 - Chapter

SN - 9783031617157

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

SP - 84

EP - 99

BT - Logics and Type Systems in Theory and Practice

PB - Springer

Y2 - 29 May 2024 through 29 May 2024

ER -

Bogaerts B, Cruz-Filipe L. Approximation Fixpoint Theory in Coq: with an Application to Logic Programming. In Logics and Type Systems in Theory and Practice: Essays Dedicated to Herman Geuvers on The Occasion of His 60th Birthday. Springer. 2024. p. 84-99. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-031-61716-4_5

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

Abstract

Publication series

Conference

Bibliographical note

Access to Document

Handle.net

Other files and links

Fingerprint

FWOAL990: Approximation Fixpoint Theory as a General Algebraic Theory of Constructive Knowledge

Cite this

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

Abstract

Publication series

Conference

Bibliographical note

Access to Document

Handle.net

Other files and links

Fingerprint

Projects

FWOAL990: Approximation Fixpoint Theory as a General Algebraic Theory of Constructive Knowledge

Cite this