Zum Hauptinhalt springen

Begründung: Umsetzung

Module, Schemadatei, Beweiser, Argumentdatei, Ansicht

Veröffentlichungsdatum

1. Oktober 2026

TippIn einem Satz

Nach der SQL-Abfrage einer Form baut fql/argument für jeden Zeugen der Antwort die Fakten, leitet die Instanz mit dem gemeinsamen Beweiser famulus_proof ab, stellt die kritischen Fragen der Schemadatei, bildet Konklusion und Antwort und schreibt das ganze Argument neben das Notebook, wo die Ansicht Gründe es liest.

Der Weg einer Anfrage

flowchart TD
  frage["Frage im Block"] --> vor["Vorverarbeitung: Form, Parameter, Lesart"]
  vor --> bind["Bindung an das Register"]
  bind --> sql["SQL der Form auf dem Sidecar"]
  sql --> zeugen["Zeilen mit Zeugen: _belege, _acts, Satzschlüssel"]
  zeugen --> fakten["facts.py: Fakten mit Adresse, Herkunft, Grad"]
  fakten --> ground["datalog.py: Regeln über den Fakten jedes Zeugen"]
  ground --> beweis["famulus_proof: Instanzziel folgt, Blätter"]
  zeugen --> kq["Kritische Fragen: Sonden auf dem Sidecar"]
  kq --> agg["reason.py: Annahme, Verschmelzen, Quantor, Urteil"]
  beweis --> agg
  agg --> worte["verbalise.py: Sätze mit Platzhaltern"]
  agg --> datei["store.py: _famulus/evidence"]
  datei --> ansicht["Ansicht Gründe"]

Modul Aufgabe
fql/request.py Der Harness: Kontext, Vorverarbeitung, Bindung, SQL, Begründung, Formulierung, Gedächtnis
fql/argument/facts.py Zeilen des Sidecars als Fakten: Briefe, Handlungen, Sätze, Themen, Perioden, Namensformen; Grade aus den gemessenen Präzisionen
fql/argument/datalog.py Grundatome, Regeln mit Variablen und Parametern, eingebaute Vergleiche, Grundierung je Zeuge
famulus_proof Grundresolution mit Beweisgraph; dasselbe Paket prüft im Lektor die sachliche Validität
fql/argument/reason.py Zeugen, Instanzen, kritische Fragen, Aggregation, Urteil, Prämissen, Belege, Antwort
fql/argument/refs.py Verweise in drei Formen: Seite (mit Faksimile), Dokument, Zitat
fql/argument/verbalise.py Detailsätze des Modells mit Platzhaltern, Verwerfen eigener Zahlen
fql/argument/store.py Argumentdateien und ihr Index; Ketten und verlorene Geltung
fql/argument/schemes.yaml Vokabular, Regeln, kritische Fragen, Schemata, Formspezifikationen, Grade (lernbar)

Zeugen in den Zeilen

Jede Form gibt ihre Zeugen mit aus. Zählende Formen haben die Spalte _belege (die Briefe einer Zeile) und, wo die Zeile eine Person oder ein Thema ist, _keys (deren Registereinträge); Formen über Handlungen haben _acts oder _act; Formen über Sätze nennen doc_id, pidx, sent_idx. Die Ansicht zeigt diese Spalten nicht, das Argument liest sie.

Die Schemadatei

schemes.yaml ist eine Datei mit fünf Teilen. Sie ist ein lernbares Artefakt: Die Lernschleife versioniert und ändert sie, nur durch Operationen auf diesen Teilen.

grading:   {stark: 0.9, mittel: 0.7, accept: mittel, min_coverage: 0.5}
reliability:
  karman-nachlass:
    act.sentence: {audit: acts_karman}          # Stichprobe in site/data/fql_audit.json
rules:
  R-von: {spec: "VonPerson(L,X) :- Absender(L,P), Gebunden(P,X)", text: "…"}
critical:
  CQ-dubletten:
    question: "Sind unter den Belegbriefen Dubletten?"
    applies: [partner, briefzaehlung, paar, chronik, thema, periode]
    sql: "SELECT l1.letter_id AS x, l2.letter_id AS y FROM … WHERE list_contains($witnesses, …)"
    when: "rows > 0"
    outcome: offen
    effect: {merge: witnesses}
forms:
  C1-briefpartner:
    scheme: partner
    grain: letter
    witnesses: _belege
    keys: _keys
    goal: ["GegenparteiAls(W,a,{name|lit})", "ImFenster(W) if @years"]
    aggregate: rows
    conclusion: "{a} korrespondierte{zeitraum} mit {quantor} {n} Personen ({n_witness} Briefe)."

Gelesen: Für die Form C1 ist jeder Brief W einer Zeile ein Zeuge; sein Ziel ist, dass W die gebundene Person a mit der Gegenpartei verbindet, die die Zeile nennt, und, wenn ein Zeitraum gefragt ist, dass W in ihm liegt. Großgeschriebene Argumente sind Variablen, a und b sind die gebundenen Personen, {name|lit} ist der Wert der Zeile als Konstante, … if @years gilt nur, wenn ein Zeitraum gebunden ist.

Eine kritische Frage ist eine lesende SQL-Sonde mit den Parametern der Anfrage und den Zeugen ($witnesses, $acts, $keys). Ihre Wirkung ist eine von sechs: quantor (Untergrenze), merge (Einträge oder Belege verschmelzen), downgrade und upgrade (Grad einer Instanz um eine Stufe), regrade (eine Lesart herabstufen), note.

Der Beweiser

famulus_proof ist die aus dem Lektor herausgelöste Grundresolution. Eine Klausel ist eine Menge von Literalen; ein Beleg ist eine Einheitsklausel mit Adresse, eine Regelinstanz eine Horn-Klausel mit der Regel-Id. entails(W, ziel) fügt die Negation des Ziels hinzu und sucht einen Widerspruch: Einheitspropagation mit zwei beobachteten Literalen entscheidet Horn-Mengen in linearer Zeit, ein Rest geht an DPLL, der Beweistext entsteht durch Resolution mit Stützmenge. Es gibt keine Negation durch Scheitern: Was nicht abgeleitet wird, bleibt offen.

from famulus_proof import Clause, entails
d = entails(clauses, (True, "GegenparteiAls(L:…/015,a,\"Herzfeld H.\")"))
d.holds, d.leaves(), d.graph()

Für jeden Zeugen werden nur die Regeln grundiert, deren Köpfe die Ziele der Form rückwärts erreichen, und nur die Fakten, die in einer Regelinstanz vorkommen oder selbst Ziel sind. Grundierung und Beweis sind je Zeuge zwischengespeichert. Eine Form mit 13.000 Instanzen braucht so rund 10 s, die meisten Formen unter 1 s.

Die Argumentdatei

<projekt>/_famulus/evidence/<notebook>/<block>/v0005.json
<projekt>/_famulus/evidence/<notebook>/index.json

Die Version ist die des Ergebnisses im Store; Ergebnis und Begründung werden zusammen gelesen. Das Schema famulus-argument/2:

Feld Inhalt
frage, form, schema_name, schemata_version Frage, Form, Schema und Fassung der Schemadatei
interpretation Lesart, angezeigte Parameter, Bindungsschritte
abfrage, bindung_parameter SQL, Parameter, Laufzeit; alles, was zur Wiederholung nötig ist
ziel Die gefragte Aussageform
schluss Konklusion, Urteil, Quantor und seine Gründe, Kennzahlen, Abdeckung, Schlussart, schwächste Prämissen
praemissen Zeugnis, Identität, Zuverlässigkeit, Regeln, Kette, je mit Grad
kritische_fragen Jede gestellte Frage mit Ergebnis, Befund, Erläuterung und SQL
instanzen Jeder Zeuge: Ziel, gilt, Grad, angenommen, Blätter (Indizes in fakten), Regeln, Anpassungen; für die ersten zwölf der Resolutionsbeweis
fakten Die Fakten, auf die eine angenommene Instanz zeigt, mit Quelle, Adresse, Grad, Zuverlässigkeit, Fundstellen
zeilen Je Zeile der Abfrage: begründet, Zeugen, angenommen, Grad
belege Die Belege für die Ansicht, mit aufgelösten Verweisen
antwort Sätze mit Knoten und Teil (antwort oder begruendung)
expansion Das Expansionsprotokoll je Zeuge und Abteilung: Ziele, Alternativen, geschlossene Zweige, „kein Vorrat“
kern Der minimale Kern: Fakten und Regelinstanzen, kern_geprueft, ungeprueft, entfernte Klauseln
baum Der Validitätsbaum famulus-baum/1: Knoten (Art, Status, Grad, Anzahl, Grund), Kanten, Statistik
stuetzt_sich_auf, luecken, hash Kette, Lücken, Prüfsumme

GET /api/notebooks/<nb>/evidence/<block>?teil=kurz liefert das Argument ohne Instanzen und Fakten; teil=voll&von=0&bis=50 eine Seite der Instanzen mit den Fakten, die sie nennen.

Die Ansicht

Ein Block mit gespeichertem Argument zeigt die Antwortkarte: die Konklusion als ersten Satz, das Siegel validiert, nicht validiert oder Lücke. In der ausführlichen Lesart (Menü ⋯ → „Begründungen ausführlich zeigen“, oder „Alle Abschnitte aufklappen“) folgt die Begründung: Kennzahlen, nummerierte Prämissen mit Grad und Verweisen auf die Belege, der Satz Daraus folgt, die kritischen Fragen nach Widerlegt, Offen und Geprüft, die Lücken und die Belege. Der Schalter Seite · Dokument · Zitat wählt die Verweisform für das ganze Notebook; Faksimile öffnet die Seite. Vollständiger Baum zeigt Aussageform, Lesart, Regeln, kritische Fragen mit SQL und alle Instanzen seitenweise, jede mit Zielen, Blättern und, für die ersten, dem Resolutionsbeweis. Nicht überzeugend an jeder Prämisse, an der Konklusion und an jeder Instanz öffnet eine Lernepisode.

Der Link notebook?nb=<projekt>/<notebook>&block=<id> öffnet das Notebook an einem Block.

Prüfungen

Prüfung Datei
Grundierung behält die Fakten; Zählung als Untergrenze mit adressierten Blättern tests/test_argument.py
Erfundene und verschobene Zeugen werden nicht angenommen (Mutationstest) tests/test_argument.py
Detailsätze verwerfen eigene Zahlen tests/test_argument.py
Argumentdatei je Version, verlorene Geltung bei geänderter Prämisse tests/test_argument.py
Lernpatch wird geprüft, Widerruf stellt die vorige Fassung her tests/test_argument.py
Antwort einer Anfrage beginnt mit der Konklusion; abgelehnte Sätze stehen im Argument tests/test_fql.py
Alle 74 Katalogfragen mit Urteil und Begründung scripts/fql_bench.py