Options
Visualizing Kripke Models in LogiKEy : the Case of SDL
Passeto, Luca; Benzmüller, Christoph (2025): Visualizing Kripke Models in LogiKEy : the Case of SDL, in: Damiano Azzolini, Sotirios Batsakis, Manuel Alejandro Borroto Santana, u. a. (Hrsg.), Joint Proceedings of the Workshops and Doctoral Consortium of the 41st International Conference on Logic Programming (ICLP-WS-DC 2025), Aachen, Germany: RWTH Aachen.
Faculty/Chair:
Author:
Title of the compilation:
Joint Proceedings of the Workshops and Doctoral Consortium of the 41st International Conference on Logic Programming (ICLP-WS-DC 2025)
Editors:
Azzolini, Damiano
Batsakis, Sotirios
Borroto Santana, Manuel Alejandro
Bruno, Pierangela
Cecchi, Laura A.
Fandinno, Jorge
Hecher, Markus
Maratea, Marco
Morales, José F.
Muñiz, Brais
Papadakis, Emmanuel
Robaldo, Livio
Serafini, Luciano
Lo Scudo, Fabrizio
Tachmazidis, Ilias
Tarzariol, Alice
Vallati, Mauro
Wyner, Adam
ISSN:
1613-0073
Conference:
Workshops and Doctoral Consortium of the 41st International Conference on Logic Programming ; Rende, Italy
Publisher Information:
Year of publication:
2025
Pages:
Series ; Volume:
CEUR workshop proceedings ; 4117
Language:
English
Abstract:
LogiKEy is a framework and methodology for the design and engineering of ethico-legal reasoners. It is based on semantical embeddings of logics and logic combinations in expressive classical higher-order logic (HOL). This meta-logical approach allows the use of off-the-shelf theorem provers and (counter-)model finders for HOL such as Nitpick. While these model finders produce precise model descriptions, their raw textual output can be hard to read and interpret for users. In this paper, we present a tool that converts a Kripke model description from Nitpick into a TikZ graph. We showcase the tool using an example in Standard Deontic Logic (SDL).
Keywords: ; ; ; ; ;
Proof assistants
Model finders
Isabelle/HOL
Automated theorem proving
Semantical embedding
Higher-order logic
Peer Reviewed:
Yes:
International Distribution:
Yes:
Open Access Journal:
Yes:
Type:
Conferenceobject
Activation date:
December 8, 2025
Versioning
Question on publication
Permalink
https://fis.uni-bamberg.de/handle/uniba/112064