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 of-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).
LogiKEy [
As part of the framework and methodology, in this paper we introduce a lightweight, self‐contained
tool that takes a Kripke model found by the HOL model-finder Nitpick [
The rest of the paper is structured as follows: Section2 describes the problem that we are tackling by means of an example of input of the tool and an example of intended output, Section3 describes the
CEUR Workshop
ISSN1613-0073
L o g i K E y M e t h o d o l o g y visualizer tool, Section4 demonstrates the tool by applying it to Standard Deontic Logic (SDL), and Section 5 discusses the relevant results and the remaining challenges.
In this section we outline the specific task our tool addresses. Given a textual model or countermodel produced by the Nitpick model finder, we wish to generate a fully self‐contained TikZ diagram that visualizes the possible worlds, their propositional valuations, and the accessibility relation between them.
Example Input Below is a representative snippet of the kind of Nitpick output our tool consumes: Intended Output The tool should produce TikZ code that, when compiled, yields a graphical rendering of the frame as a directed graph (rendered in Figure2, where start indicates the current world1): }; % self loops \path[->,loop right,looseness=8] (w5) edge (w5); % initial state \node[draw=none,left=of w0,xshift=-5mm] (init) {\small start}; \draw[->,thick] (init) -- (w0); \end{tikzpicture} 4 ∶ ,
Note that we use the Spring-Electrical Layout (see Section 32.3 of 8[] and [9]) from the graph drawing features of TikZ [10]: each edge behaves like a spring, pulling its two endpoint nodes toward each other; simultaneously, every pair of distinct nodes experiences a smallelectrical repulsion [9]. The combined efect is that connected nodes cluster at a natural distance (set by node distance), while unrelated nodes space themselves apart, avoiding overlaps. Iterating these forces until equilibrium yields an aesthetically pleasing, roughly evenly spaced graph [9]. The advantage for us is generality: this approach yields clear, automatically arranged visualizations of Nitpick models (e.g., with varying numbers of worlds), suitable for inclusion in papers or presentations with minimal manual adjustment8[]. 1While worlds in the Nitpick output are numbered starting from 1, in the TikZ graph we start from 0 (i.e.i, 1 corresponds to 0).
The conversion tool automates the process of turning a Nitpick countermodel (text output from Isabelle/HOL) into a clean, self‐contained TikZ diagram. In Algorithm1 we show the pseudo-code of the tool2. Conceptually, it performs two main tasks: (1) Model Extraction, reading and extracting information from the Nitpick dump; and (2) Graph Rendering, producing TikZ code to draw a graph corresponding to the extracted information.
Data: Lines of a Nitpick (counter)-model dump Result: TikZ graph rendering of the model begin
Read nonempty lines intolines; Parse the number of worlds, the index of the current world, and list atoms of proposition names; Build an × | atoms| truth‐table values; Extract all True edges into edges;
Split edges into self_loops and inter_edges; end begin
Print TikZ header and graph settings; Define Label( ):
Return the formatted label for world using atoms and values[i]; Group inter_edges by source into by_src; Initialize empty set defined; foreach source in ascending order do
Let successors ← by_src[ ]; if ∉ defined then
Define node with Label( );
Add to defined; end else end else
end if multiple successors then
Emit an edge from to the set of successors;
end
Mark any newly introduced successors in defined; end Print closing of thegraph block; foreach pair (, ) in self_loops do
Print a separate self‐loop edge for ; end Print arrow to the current worldm;
Print end of TikZ picture; end
Algorithm 1: Pseudocode for Nitpick‐to‐TikZ conversion 2The python code is available online atlogikey.org/Nitpick2TikZ.
We now go into more detail on what happens at the two distinct phases of the algorithm: 1. Model Extraction (Parsing the Nitpick Output)
We read each non‐empty line of the (counter)-model dump and extract: • The number of worlds. • The index of the current world. • The list atoms of all proposition names in the order they appear. • A truth‐table values of size × | atoms|, recording which atoms hold in which worlds. • The list edges of all directed pairs (, ) for which the relation isTrue.
We then separate out any self‐loops (, ) so they can be handled after the automatic layout. 2. Graph Rendering (Generating the TikZ Code)
We begin a tikzpicture using a force‐directedgraph layout. A helper function Label formats each world as
∶ atom1, ¬atom2, … .
We group the non‐loop edges by their source world, then iterate in ascending order. For each source : • If has not yet been printed, we introduce node with its label. • We emit arrows from to each of its successors, bundling multiple targets where appropriate.
After closing the graph block, we draw each self‐loop explicitly using TikZ’s \path[->,loop above], ensuring those loops remain visible, and we draw a special arrow indicating the current world. Finally we close the TikZ picture.
We demonstrate the application of the tool to Standard Deontic Logic (SDL). In particular, we present
the well-known example of the Chisholm’s contrary-to-duty paradox [11], which has been encoded in
LogiKEy in [12]. For details on the Chisholm paradox in SDL, here we refer to Chapter 1 1[
Standard Deontic Logic is a formal system used to represent and reason about normative concepts such as obligation, permission, and prohibition. It is based on modal logic and typically corresponds to the modal system D (also known as KD), which includes the modal axioms of system K along with the seriality axiom D, ensuring that what is obligatory is at least permitted. In the languageO, is the deontic modality for obligation. Semantically, the accessibility relatio n⊆ × is a serial binary relation over . It is understood as a relation of deontic alternatives: (or, alternatively, (, ) ∈ ) expresses that is an ideal alternative to , or that is a “good” successor of . The first one is “good” in the sense that it complies with all the obligations true in the second one. Furthermore, the constraint of seriality means that the model does not have a dead end, a state with no good successor.
Chisholm’s paradox is a classic contrary-to-duty scenario that exposes a key limitation of SDL. The scenario can be stated as follows with four sentences (see [13]):
F1 It ought to be that Jones goes to the assistance of his neighbors.
F2 It ought to be that if Jones goes to the assistance of his neighbors, then he tells them he is coming. F3 If Jones doesn’t go to the assistance of his neighbors, then he ought not tell them he is coming. F4 Jones does not go to the assistance of his neighbors.
The problem is then how to formalize this: it is widely thought that all four could be true simultaneously, and none is a deductive consequence of the others. In Figure3 we list four ways of representing Chisholm’s paradox in SDL as in [13]. These are the four combinations depending on the obligation modalityO having a wide or narrow scope with respect to implication, and each of them violates one or both of the requirements.
F1 F2 F3 F4
WN
O O( → ) ¬ →
O¬ ¬
WW
O
O( → ) O(¬ → ¬) ¬
→ ¬ → ¬
NN O
O O ¬
NW
O →
O O(¬ → ¬) ¬
Here, we do not address the technicalities of the paradox but only focus on interesting applications for the tool discussed in this paper. One example is checking whether a formula is not a deductive consequence of the others. Indeed, the fourth formula 4 is not a consequence of the other three in all of the formalizations, and this is something that we can find a countermodel for using Nitpick. More specifically, we use the SSE of SDL and Chisholm’s paradox encodings from [12], and for each formalization , , and we check that formula ( 1 ∧ 2 ∧ 3) → 4 is not valid and find a countermodel using Nitpick from the Isabelle2025/HOL (March 2025) distribution. We then apply our tool to visualize such textual countermodels. Figures4, 5, 6 and 7 show the countermodels found for formalizations WW, NN, NW and WN, respectively. Figure2 above displays a larger countermodel found for the formalizations WN and NN. In all the frames,start is used to indicate the current world (for which the formula does not hold).
start
This paper contributes a self-contained tool for visualizing the Kripke models that are returned by
Nitpick in a textual format. The tool complements theLogiKEy framework and methodology by
start
start
start
facilitating the inspection of examples and counterexamples, which can be crucial in scenarios where
such examples are not intuitive. Numerous systems support model or countermodel generation, e.g.
Mace4 for first‐order logic [ 15], or Nitpick and Quickcheck in Isabelle/HOL [
Legal reasoning often involves detecting conflicts, conditional obligations, and exceptions within
complex normative systems. By visualizing these structures, our tool has the potential to helpLogiKEy
users see where obligations clash or where contrary‐to‐duty scenarios arise. This graphical “cognitive
scafold” not only speeds up case analysis and lets users explore what‐if scenarios, but also enhances
transparency and trust. Indeed, research in legal informatics suggests that systematically visualizing
interactions of legal provisions can serve as a powerful decision-support tool2[
In conclusion, our visualization tool extends the LogiKEy methodology by making countermodels
accessible, can contribute to more intuitive legal‐logic workflows and supports the broader goals of
explainable AI in law. Future work will test how the tool scales to larger models and extend support
to richer logics encoded in Isabelle/HOL in theLogiKEy framework (such as logics from the modal
logic cube [
This work was supported by the Luxembourg National Research Fund (FNR) through the project Logical methods for Deontic Explanations (INTER/DFG/23/17415164/LODEX) and the project Deontic Logic for Epistemic Rights (OPEN O20/14776480).
The authors have not employed any Generative AI tools. [9] Y. Hu, Eficient, high-quality force-directed graph drawing, The Mathematica Journal 10 (2006) 37–71. [10] J. Pohlmann, Configurable Graph Drawing Algorithms for the TikZ Graphics Description Language,
Master’s thesis, 2011. [11] R. M. Chisholm, Contrary-to-duty imperatives and deontic logic, Analysis 24 (1963) 33–36.
doi:10.1093/analys/24.2.33. [12] C. Benzmüller, A. Farjami, D. Fuenmayor, P. Meder, X. Parent, A. Steen, L. van der Torre, V. Zahoransky, LogiKEy workbench: Deontic logics, logic combinations and expressive ethical and legal reasoning (Isabelle/HOL dataset), Data in Brief 33 (2020) 1–10. doi1:0.1016/j.dib.2020.106409. [13] R. Hilpinen, P. McNamara, Deontic logic: A historical survey and introduction, in: D. M. Gabbay, J. Horty, X. Parent, R. van der Meyden, L. van der Torre (Eds.), Handbook of Deontic Logic and Normative Systems, College Publications, London, UK, 2013, pp. 3–136. [14] D. M. Gabbay, J. Horty, X. Parent, R. van der Meyden, L. van der Torre (Eds.), Handbook of Deontic
Logic and Normative Systems, College Publications, London, UK, 2013. [15] W. McCune, Mace4 Reference Manual and Guide, Technical Report ANL/MCS-TM-264, Argonne National Laboratory, 2003. URL:https://www.mcs.anl.gov/research/projects/AR/mace4/July-2005/ doc/mace4.pdf, technical Memorandum, Mathematics and Computer Science Division. [16] S. Berghofer, T. Nipkow, Random testing in isabelle/hol, in: Proceedings of the Second International Conference on Software Engineering and Formal Methods, 2004. SEFM 2004., 2004, pp. 230–239. doi:10.1109/SEFM.2004.1347524. [17] L. Bulwahn, The new quickcheck for isabelle, in: C. Hawblitzel, D. Miller (Eds.), Certified Programs and Proofs, Springer Berlin Heidelberg, Berlin, Heidelberg, 2012, pp. 92–108. [18] D. Jackson, Alloy: a lightweight object modelling notation, ACM Trans. Softw. Eng. Methodol. 11 (2002) 256–290. doi:10.1145/505145.505149. [19] M. Gattinger, Kripkevis — a haskell module to visualize kripke frames, 2014. URL:https://w4eg.de/ malvin/illc/kripkevis/. [20] M. Gattinger, Gomoche: Gossip model checking, 2022. URL: https://malv.in/2022/
LAMASSR-GoMoChe.pdf. [21] S. McLachlan, E. Kyrimi, K. Dube, N. Fenton, L. C. Webley, Lawmaps: enabling legal ai development through visualisation of the implicit structure of legislation and lawyerly process, Artificial Intelligence and Law 31 (2023) 169–194. doi:10.1007/s10506-021-09298-0. [22] C. Benzmüller, M. Claus, N. Sultana, Systematic verification of the modal logic cube in Isabelle/HOL, in: C. Kaliszyk, A. Paskevich (Eds.), PxTP 2015, volume 186, EPTCS, Berlin, Germany, 2015, pp. 27–41. doi:10.4204/EPTCS.186.5. [23] C. Benzmüller, L. C. Paulson, Quantified multimodal logics in simple type theory, Logica Universalis 7 (2013) 7–20. doi:10.1007/s11787-012-0052-y. [24] C. Benzmüller, S. Reiche, Automating public announcement logic with relativized common knowledge as a fragment of HOL in LogiKEy, Journal of Logic and Computation 33 (2023) 1243–1269. doi:10.1093/logcom/exac029. [25] L. Pasetto, C. Benzmüller, Implementing the fatio protocol for multi-agent argumentation in logikey, in: C. Benzmüller, J. Otten, R. Ramanayake (Eds.), ARQNL 2024, CEUR Workshop Proceedings, 2024. [26] L. Lawniczak, L. Pasetto, C. Benzmüller, X. Li, R. Markovich, Reasoning with epistemic rights and duties: Automating a dynamic logic of the right to know in LogiKEy, in: I. Lynce, N. Murano, M. Vallati, S. Villata, F. Chesani, M. Milano, A. Omicini, M. Dastani (Eds.), Proceedings of the 28th European Conference on Artificial Intelligence (ECAI 2025), volume 413 of Frontiers in Artificial Intelligence and Applications, IOS Press, 2025, pp. 1623 – 1630. doi:10.3233/FAIA250988. [27] C. Benzmüller, D. Fuenmayor, Mathematical proof assistants for teaching logic: The LogiKEy methodology, in: Book of Abstracts — V Congress Tools for Teaching Logic, Madrid, Spain, 2023. URL: https://www.researchgate.net/publication/371044093. doi:10.13140/RG.2.2.24708.74888.