Tomer Libal

Aleksander Smywiński-Pohl, Tomer Libal, Adam Kaczmarczyk et al.

One of the elements of legal research is looking for cases where judges have extended the meaning of a legal concept by providing interpretations of what a concept means or does not mean. This allow legal professionals to use such interpretations as precedents as well as laymen to better understand the legal concept. The state-of-the-art approach for retrieving the most relevant interpretations for these concepts currently depends on the ranking of sentences and the training of language models over annotated examples. That manual annotation process can be quite expensive and need to be repeated for each such concept, which prompted recent research in trying to automate this process. In this paper, we highlight the results of various experiments conducted to determine the volume, scope and even the need for manual annotation. First of all, we check what is the optimal number of annotations per a legal concept. Second, we check if we can draw the sentences for annotation randomly or there is a gain in the performance of the model, when only the best candidates are annotated. As the last question we check what is the outcome of automating the annotation process with the help of an LLM.

Tomer Libal, Alexander Steen

A prototype for automated reasoning over legal texts, called NAI, is presented. As an input, NAI accepts formalized logical representations of such legal texts that can be created and curated using an integrated annotation interface. The prototype supports automated reasoning over the given text representation and multiple quality assurance procedures. The pragmatics of the NAI suite as well its feasibility in practical applications is studied on a fragment of the Smoking Prohibition (Children in Motor Vehicles) (Scotland) Act 2016 of the Scottish Parliament.

Tomer Libal, Matteo Pascucci

Systems of deontic logic suffer either from being too expressive and therefore hard to mechanize, or from being too simple to capture relevant aspects of normative reasoning. In this article we look for a suitable way in between: the automation of a simple logic of normative ideality and sub-ideality that is not affected by many deontic paradoxes and that is expressive enough to capture contrary-to-duty reason- ing. We show that this logic is very useful to reason on normative scenarios from which one can extract a certain kind of argumentative structure, called a Normative Detachment Structure with Ideal Conditions. The theoretical analysis of the logic is accompanied by examples of automated reasoning on a concrete legal text.

Tomer Libal, Xaviera Steele

The search for increased trustworthiness of SAT solvers is very active and uses various methods. Some of these methods obtain a proof from the provers then check it, normally by replicating the search based on the proof's information. Because the certification process involves another nontrivial proof search, the trust we can place in it is decreased. Some attempts to amend this use certifiers which have been verified by proofs assistants such as Isabelle/HOL and Coq. Our approach is different because it is based on an extremely simplified certifier. This certifier enjoys a very high level of trust but is very inefficient. In this paper, we experiment with this approach and conclude that by placing some restrictions on the formats, one can mostly eliminate the need for search and in principle, can certify proofs of arbitrary size.

Tomer Libal, Martin Riener, Mikheil Rukhaia

Sequent calculus is widely used for formalizing proofs. However, due to the proliferation of data, understanding the proofs of even simple mathematical arguments soon becomes impossible. Graphical user interfaces help in this matter, but since they normally utilize Gentzen's original notation, some of the problems persist. In this paper, we introduce a number of criteria for proof visualization which we have found out to be crucial for analyzing proofs. We then evaluate recent developments in tree visualization with regard to these criteria and propose the Sunburst Tree layout as a complement to the traditional tree structure. This layout constructs inferences as concentric circle arcs around the root inference, allowing the user to focus on the proof's structural content. Finally, we describe its integration into ProofTool and explain how it interacts with the Gentzen layout.

Cvetan Dunchev, Alexander Leitsch, Tomer Libal et al.

This paper introduces PROOFTOOL, the graphical user interface for the General Architecture for Proof Theory (GAPT) framework. Its features are described with a focus not only on the visualization but also on the analysis and transformation of proofs and related tree-like structures, and its implementation is explained. Finally, PROOFTOOL is compared with three other graphical interfaces for proofs.