SearcharxivSearch

arXiv subjects

Agata Ciabattoni

Publications and source records attributed to Agata Ciabattoni.

17 recordsLinked to original sources

Toward Robust Legal Text Formalization into Defeasible Deontic Logic using LLMs

We present a comprehensive approach to the automated formalization of legal texts using large language models (LLMs), targeting their transformation into Defeasible Deontic Logic (DDL). Our method employs a structured pipeline that segments complex normative language into atomic snippets, extracts deontic rules, and evaluates them for syntactic and semantic coherence. We introduce a refined success metric that more precisely captures the completeness of formalizations, and a novel two-stage pipeline with a dedicated refinement step to improve logical consistency and coverage. The evaluation procedure has been strengthened with stricter error assessment, and we provide comparative results across multiple LLM configurations, including newly released models and various prompting and fine-tuning strategies. Experiments on legal norms from the Australian Telecommunications Consumer Protections Code demonstrate that, when guided effectively, LLMs can produce formalizations that align closely with expert-crafted representations, underscoring their potential for scalable legal informatics.

cs.CL

Support + Belief = Decision Trust

We present SBTrust, a logical framework designed to formalize decision trust. Our logic integrates a doxastic modality with a novel non-monotonic conditional operator that establishes a positive support relation between statements, and is closely related to a known dyadic deontic modality. For SBTrust, we provide semantics, proof theory and complexity results, as well as motivating examples. Compared to existing approaches, our framework seamlessly accommodates the integration of multiple factors in the emergence of trust.

cs.LO

Dyadic obligations: proofs and countermodels via hypersequents

The basic system E of dyadic deontic logic proposed by {\AA}qvist offers a simple solution to contrary-to-duty paradoxes and allows to represent norms with exceptions. We investigate E from a proof-theoretical viewpoint. We propose a hypersequent calculus with good properties, the most important of which is cut-elimination, and the consequent subformula property. The calculus is refined to obtain a decision procedure for E and an effective countermodel computation in case of failure of proof search. Using the refined calculus, we prove that validity in E is Co-NP and countermodels have polynomial size.

cs.LO

Internal and External Calculi: Ordering the Jungle without Being Lost in Translations

This paper gives a broad account of the various sequent-based proof formalisms in the proof-theoretic literature. We consider formalisms for various modal and tense logics, intuitionistic logic, conditional logics, and bunched logics. After providing an overview of the logics and proof formalisms under consideration, we show how these sequent-based formalisms can be placed in a hierarchy in terms of the underlying data structure of the sequents. We then discuss how this hierarchy can be traversed using translations. Translating proofs up this hierarchy is found to be relatively straightforward while translating proofs down the hierarchy is substantially more difficult. Finally, we inspect the prevalent distinction in structural proof theory between 'internal calculi' and 'external calculi.' We discuss the ambiguities involved in the informal definitions of these categories, and we critically assess the properties that (calculi from) these classes are purported to possess.

cs.LO

Deontic Paradoxes in ASP with Weak Constraints

The rise of powerful AI technology for a range of applications that are sensitive to legal, social, and ethical norms demands decision-making support in presence of norms and regulations. Normative reasoning is the realm of deontic logics, that are challenged by well-known benchmark problems (deontic paradoxes), and lack efficient computational tools. In this paper, we use Answer Set Programming (ASP) for addressing these shortcomings and showcase how to encode and resolve several well-known deontic paradoxes utilizing weak constraints. By abstracting and generalizing this encoding, we present a methodology for translating normative systems in ASP with weak constraints. This methodology is applied to "ethical" versions of Pac-man, where we obtain a comparable performance with related works, but ethically preferable results.

cs.LO

Streamlining Input/Output Logics with Sequent Calculi

Input/Output (I/O) logic is a general framework for reasoning about conditional norms and/or causal relations. We streamline Bochman's causal I/O logics via proof-search-oriented sequent calculi. Our calculi establish a natural syntactic link between the derivability in these logics and in the original I/O logics. As a consequence of our results, we obtain new, simple semantics for all these logics, complexity bounds, embeddings into normal modal logics, and efficient deduction methods. Our work encompasses many scattered results and provides uniform solutions to various unresolved problems.

cs.LO

Cut-restriction: from cuts to analytic cuts

Cut-elimination is the bedrock of proof theory with a multitude of applications from computational interpretations to proof analysis. It is also the starting point for important meta-theoretical investigations including decidability, complexity, disjunction property, and interpolation. Unfortunately cut-elimination does not hold for the sequent calculi of most non-classical logics. It is well-known that the key to applications is the subformula property (a typical consequence of cut-elimination) rather than cut-elimination itself. With this in mind we introduce cut-restriction, a procedure to restrict arbitrary cuts to analytic cuts (when elimination is not possible). The algorithm applies to all sequent calculi satisfying language-independent and simple-to-check conditions, and it is obtained by adapting age-old cut-elimination. Our work encompasses existing results in a uniform way, and establishes novel analytic subformula properties.

cs.LO

A theory of cut-restriction: first steps

Cut-elimination is the bedrock of proof theory. It is the algorithm that eliminates cuts from a sequent calculus proof that leads to cut-free calculi and applications. Cut-elimination applies to many logics irrespective of their semantics. Such is its influence that whenever cut-elimination is not provable in a sequent calculus the invariable response has been a move to a richer proof system to regain it. In this paper we investigate a radically different approach to the latter: adapting age-old cut-elimination to restrict the shape of the cut-formulas when elimination is not possible. We tackle the "first level" above cut-free: analytic cuts. Our methodology is applied to the sequent calculi for bi-intuitionistic logic and S5 where analytic cuts are already known to be required. This marks the first steps in a theory of cut-restriction.

cs.LO

Display to Labeled Proofs and Back Again for Tense Logics

We introduce translations between display calculus proofs and labeled calculus proofs in the context of tense logics. First, we show that every derivation in the display calculus for the minimal tense logic Kt extended with general path axioms can be effectively transformed into a derivation in the corresponding labeled calculus. Concerning the converse translation, we show that for Kt extended with path axioms, every derivation in the corresponding labeled calculus can be put into a special form that is translatable to a derivation in the associated display calculus. A key insight in this converse translation is a canonical representation of display sequents as labeled polytrees. Labeled polytrees, which represent equivalence classes of display sequents modulo display postulates, also shed light on related correspondence results for tense logics.

cs.LO

A typed parallel λ-calculus via 1-depth intermediate proofs

We introduce a Curry-Howard correspondence for a large class of intermediate logics characterized by intuitionistic proofs with non-nested applications of rules for classical disjunctive tautologies (1-depth intermediate proofs). The resulting calculus, we call it $λ_{\parallel}$, is a strongly normalizing parallel extension of the simply typed $λ$-calculus. Although simple, the $λ_{\parallel}$ reduction rules can model arbitrary process network topologies, and encode interesting parallel programs ranging from numeric computation to algorithms on graphs.

cs.LO

Dermtrainer: A Decision Support System for Dermatological Diseases

Dermtrainer is a medical decision support system that assists general practitioners in diagnosing skin diseases and serves as a training platform for dermatologists. Its key components are a comprehensive dermatological knowledge base, a clinical algorithm for diagnosing skin diseases, a reasoning component for deducing the most likely differential diagnoses for a patient, and a library of high-quality images. This report describes the technical components of the system, in particular the ranking algorithm for retrieving appropriate diseases as diagnoses.

cs.IR

Classical Proofs as Parallel Programs

We introduce a first proofs-as-parallel-programs correspondence for classical logic. We define a parallel and more powerful extension of the simply typed lambda calculus corresponding to an analytic natural deduction based on the excluded middle law. The resulting functional language features a natural higher-order communication mechanism between processes, which also supports broadcasting. The normalization procedure makes use of reductions that implement novel techniques for handling and transmitting process closures.

cs.LO

Hypersequents and Systems of Rules: Embeddings and Applications

We define a bi-directional embedding between hypersequent calculi and a subclass of systems of rules (2-systems). In addition to showing that the two proof frameworks have the same expressive power, the embedding allows for the recovery of the benefits of locality for 2-systems, analyticity results for a large class of such systems, and a rewriting of hypersequent rules as natural deduction rules.

math.LO

Gödel Logic: from Natural Deduction to Parallel Computation

Propositional Gödel logic extends intuitionistic logic with the non-constructive principle of linearity $A\rightarrow B\ \lor\ B\rightarrow A$. We introduce a Curry-Howard correspondence for this logic and show that a particularly simple natural deduction calculus can be used as a typing system. The resulting functional language enriches the simply typed lambda calculus with a synchronous communication mechanism between parallel processes. Our normalization proof employs original termination arguments and sophisticated proof transformations with a meaningful computational reading. Our results provide a computational interpretation of Gödel logic as a logic of communicating parallel processes, thus proving Avron's 1991 conjecture.

cs.LO

Mīmā\d{m}sā deontic logic: proof theory and applications

Starting with the deontic principles in M\=ımā\d{m}sā texts we introduce a new deontic logic. We use general proof-theoretic methods to obtain a cut-free sequent calculus for this logic, resulting in decidability, complexity results and neighbourhood semantics. The latter is used to analyse a well known example of conflicting obligations from the Vedas.

cs.LO

Theorem proving for prenex Gödel logic with Delta: checking validity and unsatisfiability

Gödel logic with the projection operator Delta (G_Delta) is an important many-valued as well as intermediate logic. In contrast to classical logic, the validity and the satisfiability problems of G_Delta are not directly dual to each other. We nevertheless provide a uniform, computational treatment of both problems for prenex formulas by describing appropriate translations into sets of order clauses that can be subjected to chaining resolution. For validity a version of Herbrand's Theorem allows us to show the soundness of standard Skolemization. For satisfiability the translation involves a novel, extended Skolemization method.

cs.LO

Quantified propositional Goedel logics

It is shown that G-up, the quantified propositional Goedel-Dummett logic based on the truth-values set V-up = {1 - 1/n : n >= 1} u {1}, is decidable. This result is obtained by reduction to Buechi's theory S1S. An alternative proof based on elimination of quantifiers is also given, which yields both an axiomatization and a characterization of G-up as the intersection of all finite-valued quantified propositional Goedel logics.

math.LO