Eine Modallogik für zeitliche und jurisdiktionelle Klassifikatormodelle

Grundinformationen

• Papier-ID: 2510.13691
• Titel: A Modal Logic for Temporal and Jurisdictional Classifier Models
• Autoren: Cecilia Di Florio (Universität Bologna, Universität Luxemburg), Huimin Dong (TU WIEN), Antonino Rotolo (Universität Bologna)
• Klassifizierung: cs.AI
• Veröffentlichungsdatum: 15. Oktober 2025 (arXiv-Preprint)
• Papierlink: https://arxiv.org/abs/2510.13691

Zusammenfassung

Logikbasierte Modelle können zur Entwicklung von Verifikationswerkzeugen für Maschinenlern-Klassifikatoren im Rechtsbereich eingesetzt werden. ML-Klassifikatoren prognostizieren die Ergebnisse neuer Fälle basierend auf vorherigen Fällen und führen somit eine Form des fallbasierten Schließens (Case-Based Reasoning, CBR) durch. In diesem Papier führen wir eine Modallogik von Klassifikatoren ein, die dazu konzipiert ist, das juristische CBR formal zu erfassen. Wir integrieren Prinzipien zur Konfliktlösung zwischen Präzedenzfällen, indem wir die zeitliche Dimension von Fällen und die Hierarchie der Gerichte innerhalb des Rechtssystems in die Logik einführen.

Forschungshintergrund und Motivation

Problemhintergrund

1. Verifikationsbedarf in der Rechts-KI: Die Anwendung von Maschinenlern-Klassifikatoren im Rechtsbereich nimmt zu, doch die normative Korrektheit, Genauigkeit und Robustheit ihrer Vorhersageergebnisse können nicht garantiert werden, was Richter beunruhigt
2. Präzedenzfall-Bindungsproblem: In Common-Law-Systemen müssen Klassifikatoren die Präzedenzfall-Bindung (precedential constraint) erfüllen und das Prinzip des „stare decisis" (Bindung an Präzedenzfälle) befolgen
3. Präzedenzfall-Konflikte: In realen Rechtssystemen existieren Präzedenzfall-Konflikte, während bestehende Horty-Modelle Fallkonsistenz voraussetzen und Konflikte zwischen Präzedenzfällen nicht bewältigen können

Forschungsmotivation

Juristische Fallanalyse ist im Wesentlichen eine Form des fallbasierten Schließens (CBR), wobei Maschinenlern-Klassifikatoren historische Fälle zur Vorhersage neuer Fallergebnisse nutzen. Bestehende Modelle können jedoch Präzedenzfall-Konflikte nicht bewältigen und erfordern die Einführung zeitlicher und hierarchischer Dimensionen zur Lösung dieses Problems.

Einschränkungen bestehender Ansätze

• Hortys Reason- und Result-Modelle setzen Fallkonsistenz voraus
• Können reale Präzedenzfall-Konflikte nicht bewältigen
• Ermangeln einer formalen Modellierung zeitlicher und hierarchischer Dimensionen

Kernbeiträge

1. Erweiterung des BCL-Rahmens: Einführung zeitlicher und hierarchischer Operatoren auf Grundlage der binären Eingabe-Klassifikatorlogik (BCL) zur Konstruktion des zeitlich-jurisdiktionellen Klassifikatormodells (TJCM)
2. Formalisierung des Präzedenzfall-Konzepts: Strenge Definition der Konzepte Präzedenzfall, potenziell bindender Präzedenzfall und bindender Präzedenzfall
3. Ausnahmeverarbeitungsmechanismus: Modellierung zweier Präzedenzfall-Ausnahmefälle – Aufhebung (overruled) und fehlerhafte Entscheidung (per incuriam)
4. Konfliktlösungsprinzipien: Formalisierung zeitlich-hierarchischer Präzedenzfall-Konfliktlösungsprinzipien
5. Vollständigkeitsbeweis: Bereitstellung der Axiomatisierung und des Vollständigkeitsbeweises des TJCL-Logik-Systems

Methodische Details

Aufgabendefinition

Eingabe: Neuer Rechtsfall mit Sachverhaltsmerkmalen, zuständigem Gericht und Fallname Ausgabe: Vorhersage des Urteils (Klägerin unterstützen = 1, Beklagter unterstützen = 0, unentschieden = ?) Einschränkungen: Muss Präzedenzfall-Bindung und zeitlich-hierarchische Prinzipien befolgen

Modellierung von Kernkonzepten

1. Jurisdiktionsstruktur (Jurisdiction)

Definition 1: Jurisdiktion Jur = (Courts, H, B)
- Courts: Menge von Gerichten
- H ⊆ Courts × Courts: Hierarchiebeziehung (transitiv, nicht reflexiv)
- B ⊆ Courts × Courts: Bindungsbeziehung

2. Zeitlich-Jurisdiktionelles Klassifikatormodell (TJCM)

Definition 2: TJCM = (S, f, Jur, ≤T, R)
- S ⊆ 2^Atm0: Zustandsmenge (jeder Zustand enthält ein eindeutiges Gericht)
- f: S → Val: Entscheidungsfunktion, Val = {1, 0, ?}
- ≤T: Totale Präordnung auf S (zeitliche Beziehung)
- R ⊆ S × S: Relevanzbeziehung

3. Modallogische Sprache

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

Klassifikationssystem für Präzedenzfälle

1. Unterstützende Präzedenzfälle (Supporting Precedents)

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

2. Potenziell Bindende Präzedenzfälle (Potentially Binding Precedents)

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

3. Ausnahmeverarbeitungsmechanismus

Aufhebungsbefugnis (Overruling Power):

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

Fehlerhafte Entscheidung (Per Incuriam): Berechnung durch rekursive Graphstruktur Gs = (Vs, Es), berücksichtigung:

• Verstoß gegen bindende Präzedenzfälle ohne Aufhebungsbefugnis
• Zeitlich-hierarchische Beziehung zu bindenden Präzedenzfällen
• Vollständigkeit der Aufhebungskette

Endgültig Bindende Präzedenzfälle:

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

Konfliktlösungsprinzipien

Zeitlich-Hierarchisches Prinzip

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

Entscheidungsfunktion

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

Experimentelle Einrichtung

Fallstudie

Das Papier verwendet eine Fallstudie zu Geschäftsgeheimnissen mit vier Faktoren:

• Unterstützen Kläger: measure (Sicherheitsmaßnahmen), deceived (täuschend erworben)
• Unterstützen Beklagter: reverse (rückwärts konstruierbar), disclosed (freiwillig offengelegt)

Gerichtshierarchie

Basierend auf dem englischen und walisischen Zivilgerichtssystem:

• c0: Oberster Gerichtshof des Vereinigten Königreichs (nicht an sich selbst gebunden)
• c1: Berufungsgericht (an sich selbst gebunden)
• c2: High Court (an sich selbst gebunden)
• c3, c4: County Courts (veröffentlichen keine bindenden Entscheidungen)

Ausführungsbeispiel

6 historische Fälle (s1-s6) und 1 neuer Fall (s*), demonstriert den vollständigen Konfliktlösungsprozess.

Experimentelle Ergebnisse

Hauptergebnisse

Validierung der Rahmeneffektivität durch Ausführungsbeispiel:

1. Anfängliche Konflikterkennung: s1, s2, s3, s4 sind alle mit s* relevant, aber mit unterschiedlichen Urteilen
2. Jurisdiktionsfilterung: Ausschluss von s5, s6 (County-Court-Urteile, nicht bindend)
3. Ausnahmeverarbeitung:
   • s1 wird durch s3 aufgehoben
   • s4 wird als per incuriam erkannt
4. Endgültige Entscheidung: s3 (Oberster Gerichtshof, neuerer) übertrumpft s2 (Berufungsgericht), s* wird zwingend als 0 entschieden

Theoretische Ergebnisse

• Vollständigkeitssatz (Proposition 3): TJCL ist relativ zu TJCM vollständig
• Semantische Äquivalenz (Proposition 9): Syntaktische und semantische per-incuriam-Definitionen sind äquivalent
• Korrektheitsprüfung: Semantische Korrektheit aller Modaloperatoren nachgewiesen

Verwandte Arbeiten

Juristische CBR-Forschung

• Horty-Modell: Reason- und Result-Modelle, aber mit Konsistenzannahme
• CATO-Rahmen: Fallanalyse zu Geschäftsgeheimnissen mit Faktorstruktur
• Liu et al.: Etablierung der Entsprechung zwischen Horty-Modell und Klassifikatormodell

Zeitliche und Hierarchische Modellierung

• Broughton: Integration vertikaler und horizontaler Bindungen, aber unterschiedliche Behandlung
• Wyner & Bench-Capon: Argumentationsrahmen-basierte juristische Argumentation
• Ashley: Bahnbrechende Arbeiten zur Modellierung juristischer Argumentation

Modallogik-Anwendungen

• BCL-Rahmen: Grundlage der binären Klassifikatorlogik
• Hybridlogik: Theoretische Grundlage für Namensoperatoren

Schlussfolgerungen und Diskussion

Hauptschlussfolgerungen

1. Erfolgreiche Erweiterung des BCL-Rahmens mit zeitlicher und jurisdiktioneller Dimension
2. Formalisierung komplexer Präzedenzfall-Beziehungen und Ausnahmeverarbeitung
3. Bereitstellung eines systematischen Ansatzes zur Bewältigung von Präzedenzfall-Konflikten
4. Etablierung eines vollständigen Axiom-Systems mit Vollständigkeitsbeweis

Einschränkungen

1. Relevanzbeziehung: Keine spezifischen Eigenschaftsbeschränkungen für Relevanzbeziehungen
2. Binäre Bindung: Bindungsbeziehung ist binär, kontextabhängige Bindung nicht berücksichtigt
3. Rechenkomplexität: Komplexität der per-incuriam-Berechnung nicht analysiert
4. Praktische Anwendung: Mangel an Validierung mit großflächigen realen Fällen

Zukünftige Richtungen

1. Berücksichtigung kontextabhängiger Bindungsbeziehungen
2. Erkundung von Verbindungen zu Argumentationsrahmen
3. Entwicklung konkreter Verifikationsalgorithmen
4. Erweiterung auf andere Rechtssysteme

Tiefgreifende Bewertung

Stärken

1. Theoretische Strenge: Bereitstellung eines vollständigen Formalisierungsrahmens mit Syntax, Semantik und Axiom-System
2. Praktische Relevanz: Lösung praktischer Probleme in der Rechts-KI – Präzedenzfall-Konflikte
3. Innovativität: Erstmalige Einführung zeitlicher und jurisdiktioneller Dimensionen in die Klassifikatorlogik
4. Vollständigkeit: Bereitstellung theoretischer Garantien für die Solidität des Logik-Systems

Mängel

1. Rechenkomplexität: Komplexität der rekursiven per-incuriam-Berechnung nicht analysiert
2. Empirische Validierung: Mangel an Validierung mit großflächigen realen Daten
3. Relevanz-Definition: Relevanzbeziehungs-Definition zu weit gefasst
4. Rechtsordnungsübergreifende Anwendbarkeit: Hauptsächlich auf Common-Law-Systeme ausgerichtet, Anwendbarkeit auf andere Rechtsordnungen nicht ausreichend diskutiert

Auswirkungen

1. Theoretischer Beitrag: Bereitstellung neuer theoretischer Werkzeuge für Rechts-KI
2. Praktischer Wert: Einsetzbar zur Konstruktion von Verifikationswerkzeugen für juristische Klassifikatoren
3. Interdisziplinäre Bedeutung: Verbindung von Logik, KI und Rechtswissenschaft
4. Nachfolgeforschung: Bereitstellung solider theoretischer Grundlagen für verwandte Bereiche

Anwendungsszenarien

1. Rechts-KI-Verifikation: Verifikation der Präzedenzfall-Konsistenz juristischer Klassifikatoren
2. Juristische Schließsysteme: Konstruktion von Expertensystemen zur Bewältigung von Präzedenzfall-Konflikten
3. Rechtswissenschaftliche Forschung: Formale Analyse juristischer Schließprozesse
4. Justizielle Entscheidungsunterstützung: Unterstützung von Richtern bei komplexen Präzedenzfall-Beziehungen

Literaturverzeichnis

Das Papier zitiert 25 verwandte Literaturquellen, hauptsächlich:

• Horty (2011): Regeln und Gründe in der Präzedenzfall-Theorie
• Liu et al. (2022, 2023): Logische Rahmen für Klassifikatorsysteme
• Ashley (1990): Modellierung juristischer Argumentation
• Blackburn et al. (2001): Theoretische Grundlagen der Modallogik
• MacCormick & Summers (1997): Vergleichende Forschung zur Präzedenzfall-Interpretation

Gesamtbewertung: Dies ist ein theoretisch sehr starkes Papier mit wichtigen Beiträgen im Schnittstellenbereich von Rechts-KI und Logik. Obwohl es in der empirischen Validierung gewisse Mängel aufweist, verleihen die Strenge und Innovativität des theoretischen Rahmens ihm bedeutende akademische und praktische Potenziale.