Passeto, LucaLucaPassetoBenzmüller, ChristophChristophBenzmüller0000-0002-3392-30932025-12-082025-12-0820251613-0073https://fis.uni-bamberg.de/handle/uniba/112064LogiKEy 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).engProof assistantsModel findersIsabelle/HOLAutomated theorem provingSemantical embeddingHigher-order logicconferenceobjecthttps://ceur-ws.org/Vol-4117/LPLR2025_short_1.pdf