A Modal Logic for Temporal and Jurisdictional Classifier Models

Basic Information

• Paper ID: 2510.13691
• Title: A Modal Logic for Temporal and Jurisdictional Classifier Models
• Authors: Cecilia Di Florio (University of Bologna, University of Luxembourg), Huimin Dong (TU WIEN), Antonino Rotolo (University of Bologna)
• Category: cs.AI
• Publication Date: October 15, 2025 (arXiv preprint)
• Paper Link: https://arxiv.org/abs/2510.13691

Abstract

Logic-based models can be used to build verification tools for machine learning classifiers employed in the legal field. ML classifiers predict the outcomes of new cases based on previous ones, thereby performing a form of case-based reasoning (CBR). In this paper, we introduce a modal logic of classifiers designed to formally capture legal CBR. We incorporate principles for resolving conflicts between precedents, by introducing into the logic the temporal dimension of cases and the hierarchy of courts within the legal system.

Research Background and Motivation

Problem Context

1. Verification Requirements for Legal AI: Machine learning classifiers are increasingly applied in the legal field, but their normative correctness, accuracy, and robustness cannot be guaranteed, raising concerns among judges.
2. Precedential Constraint Problem: In common law systems, classifiers must satisfy precedential constraints and follow the principle of stare decisis (following precedent).
3. Precedent Conflicts: Real legal systems contain conflicting precedents, while existing Horty models assume case base consistency and cannot handle conflicting precedents.

Research Motivation

Legal case-based reasoning is inherently a form of case-based reasoning (CBR), where machine learning classifiers predict outcomes of new cases based on historical cases. However, existing models cannot handle precedent conflicts and require the introduction of temporal and hierarchical dimensions to address this issue.

Limitations of Existing Approaches

• Horty's reason and result models assume case base consistency
• Cannot handle conflicting precedents that exist in practice
• Lack formal modeling of temporal and hierarchical dimensions

Core Contributions

1. Extension of BCL Framework: Building upon the Binary Classifier Logic (BCL), introduces temporal and hierarchical operators to construct the Temporal and Jurisdictional Classifier Model (TJCM).
2. Formalization of Precedent Concepts: Strictly defines the concepts of precedents, potentially binding precedents, and binding precedents.
3. Exception Handling Mechanism: Models two types of precedent exceptions—overruling and per incuriam (wrongly decided).
4. Conflict Resolution Principles: Formalizes precedent conflict resolution principles based on temporal-hierarchical relationships.
5. Completeness Proof: Provides axiomatization and completeness proof for the TJCL logical system.

Methodology Details

Task Definition

Input: New legal case, including factual factors, court of jurisdiction, case name Output: Predicted judgment outcome (plaintiff prevails = 1, defendant prevails = 0, undecided = ?) Constraints: Must comply with precedential constraints and temporal-hierarchical principles

Core Concept Modeling

1. Jurisdiction Structure

Definition 1: Jurisdiction Jur = (Courts, H, B)
- Courts: Set of courts
- H ⊆ Courts × Courts: Hierarchical relation (transitive, non-reflexive)
- B ⊆ Courts × Courts: Binding relation

2. Temporal and Jurisdictional Classifier Model (TJCM)

Definition 2: TJCM = (S, f, Jur, ≤T, R)
- S ⊆ 2^Atm0: Set of states (each state contains a unique court)
- f: S → Val: Decision function, Val = {1, 0, ?}
- ≤T: Total preorder on S (temporal relation)
- R ⊆ S × S: Relevance relation

3. Modal Logic Language

Definition 3: L(Atm) Syntax
φ ::= p | t(o) | H(c,c) | B(c,c) | ¬φ | φ ∧ φ | □φ | [≤T]φ | R∀φ

Precedent Classification System

1. Supporting Precedents

Definition 6: Π(s', s, o) ⟺ f(s') = o ∧ s' ∈ R(s) ∧ s' <T s

2. Potentially Binding Precedents

Definition 8: β(s', s, o) ⟺ Π(s', s, o) ∧ c'Bc
where c' ∈ s' ∩ Courts, c ∈ s ∩ Courts

3. Exception Handling Mechanism

Overruling Power:

Definition 10: O(c', c) ⟺ H(c', c) ∨ (c' = c ∧ ¬cBc)

Per Incuriam: Computed through recursive graph structure Gs = (Vs, Es), considering:

• Violation of binding precedents without overruling power
• Temporal-hierarchical relationships with binding precedents
• Completeness of overruling chains

Final Binding Precedents:

Definition 21: s' ∈ β̄s ⟺ s' ∈ βs ∧ ¬(Incuriam(s) ∧ s ~= s') ∧ ¬Overruled(s')

Conflict Resolution Principles

Temporal-Hierarchical Principle

Definition 23: BestTH(β̄s) = {s' ∈ β̄s | ∀s'' ∈ β̄s: s' ⊀ s'' ∧ ¬(s' ~= s'' ∧ s' <T s'')}

Decision Function

Definition 25: f*(s) = {
    {f(s)} if s ≠ s*
    {f(s') | s' ∈ BestTH(β̄s*)} otherwise
}

Experimental Setup

Case Study

The paper uses trade secret cases for illustration, containing four factors:

• Supporting Plaintiff: measure (security measures), deceived (deceptive acquisition)
• Supporting Defendant: reverse (reverse engineering), disclosed (voluntary disclosure)

Court Hierarchy

Based on the English and Welsh civil court system:

• c0: UK Supreme Court (not bound by itself)
• c1: Court of Appeal (self-binding)
• c2: High Court (self-binding)
• c3, c4: County Courts (do not issue binding decisions)

Running Example

Six historical cases (s1-s6) and one new case (s*), demonstrating the complete conflict resolution process.

Experimental Results

Main Results

The framework's effectiveness is verified through the running example:

1. Initial Conflict Identification: s1, s2, s3, s4 are all relevant to s* but render different judgments.
2. Jurisdiction Filtering: Excludes s5, s6 (county court decisions, non-binding).
3. Exception Handling:
   • s1 is overruled by s3
   • s4 is identified as per incuriam
4. Final Decision: s3 (Supreme Court, more recent) prevails over s2 (Court of Appeal), forcing s* to be decided as 0.

Theoretical Results

• Completeness Theorem (Proposition 3): TJCL is complete with respect to TJCM.
• Semantic Equivalence (Proposition 9): Syntactic and semantic per incuriam definitions are equivalent.
• Correctness Verification: Semantic correctness of various modal operators is proven.

Related Work

Legal CBR Research

• Horty Model: Reason and result models, but assume consistency.
• CATO Framework: Trade secret case reasoning, providing factor structure.
• Liu et al.: Established correspondence between Horty models and classifier models.

Temporal and Hierarchical Modeling

• Broughton: Combines vertical and horizontal constraints, but with different treatment.
• Wyner & Bench-Capon: Judicial reasoning based on argumentation frameworks.
• Ashley: Pioneering work on legal argumentation modeling.

Modal Logic Applications

• BCL Framework: Foundation for binary classifier logic.
• Hybrid Logic: Theoretical basis for name operators.

Conclusions and Discussion

Main Conclusions

1. Successfully extends the BCL framework by introducing temporal and jurisdictional dimensions.
2. Formalizes complex legal precedent relationships and exception handling.
3. Provides a systematic approach to handling precedent conflicts.
4. Establishes a complete axiomatic system with completeness proof.

Limitations

1. Relevance Relation: No specific attribute constraints imposed on the relevance relation.
2. Binary Constraints: Binding relations are binary, not considering context-dependent constraints.
3. Computational Complexity: Does not analyze the complexity of per incuriam computation.
4. Practical Application: Lacks verification with large-scale real cases.

Future Directions

1. Consider context-dependent binding relations.
2. Explore connections with argumentation frameworks.
3. Develop concrete verification algorithms.
4. Extend to other legal systems.

In-Depth Evaluation

Strengths

1. Theoretical Rigor: Provides a complete formal framework including syntax, semantics, and axiomatic system.
2. Practical Relevance: Addresses practical problems in legal AI—precedent conflicts.
3. Novelty: First to introduce temporal and jurisdictional dimensions into classifier logic.
4. Completeness: Provides theoretical guarantees ensuring soundness of the logical system.

Weaknesses

1. Computational Complexity: Does not analyze the complexity of recursive per incuriam computation.
2. Empirical Verification: Lacks validation with large-scale real data.
3. Relevance Definition: The definition of relevance relation is overly broad.
4. Cross-System Applicability: Primarily targets common law systems; applicability to other legal systems insufficiently discussed.

Impact

1. Theoretical Contribution: Provides new theoretical tools for legal AI.
2. Practical Value: Can be used to build verification tools for legal classifiers.
3. Interdisciplinary Significance: Connects logic, AI, and law.
4. Future Research: Provides solid theoretical foundation for related fields.

Applicable Scenarios

1. Legal AI Verification: Verifying precedent consistency of legal classifiers.
2. Legal Reasoning Systems: Building expert systems handling precedent conflicts.
3. Legal Research: Formal analysis of legal reasoning processes.
4. Judicial Decision Support: Assisting judges in handling complex precedent relationships.

References

The paper cites 25 related references, primarily including:

• Horty (2011): Rules and reasons in precedent theory
• Liu et al. (2022, 2023): Logical frameworks for classifier systems
• Ashley (1990): Legal argumentation modeling
• Blackburn et al. (2001): Theoretical foundations of modal logic
• MacCormick & Summers (1997): Comparative study of precedent interpretation

Overall Assessment: This is an excellent theoretical paper making important contributions at the intersection of legal AI and logic. While it has some limitations in empirical verification, the rigor and novelty of its theoretical framework give it significant academic value and practical potential.