Options
Visualizing Kripke Models in LogiKEy : the Case of SDL
Passeto, Luca; Benzmüller, Christoph (2026): Visualizing Kripke Models in LogiKEy : the Case of SDL, in: Bamberg: Otto-Friedrich-Universität.
Faculty/Chair:
Author:
Publisher Information:
Year of publication:
2026
Pages:
Series ; Volume:
CEUR workshop proceedings
Source/Other editions:
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, 2025, ISSN: 1613-0073
Year of first publication:
2025
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:
February 9, 2026
Permalink
https://fis.uni-bamberg.de/handle/uniba/113026