Eine Familie von Datenstrukturen und Algorithmustechniken zur Organisation von Termen, Untertermen oder Klauseln, sodass syntaktische Übereinstimmungen, Unifikationspartner oder Musterereignisse im automatisierten Schließen schnell abgerufen werden können.

Prinzip

Nutzung kompakter diskriminierender Merkmale von Termen (Symbole, Pfade, Fingerprints, Positionen), um brute-force-Vergleiche zu vermeiden; Indexstrukturen tauschen Speicher- und Aktualisierungskosten gegen schnelle Kandidatenabrufe zur Laufzeit bei Wahrung der Korrektheit für syntaktisches Matching und Unifikation.

Demonstration

In einem saturationbasierten Prädikatenbeweiser speichert ein Diskriminationsbaum Terme nach ihrer Symbolfolge, sodass beim Auswählen eines Literals f(a, X) nur Klauseln mit unifizierbaren Termen mit Kopf f abgerufen werden, anstatt die gesamte Klauseldatenbank zu durchsuchen. Ein weiteres Beispiel ist ein Substitutionsbaum, der alle Terme auflistet, die mit einer Anfrage unifizierbar sind, und so Kandidatenkennung in sublinearer Zeit zur Datenbankgröße liefert.

Fehlanwendung

Ein Index, der nur nach Wurzelzeichen sortiert ist, bei Bedarf an strukturellem Untertermabgleich einzusetzen, führt zu vielen falschen Kandidaten und keinem Zeitgewinn; ebenso machen extrem spezialisierte Indizes ohne Berücksichtigung der Aktualisierungskosten die inkrementelle Hinzufügung von Lemmata in interaktiven Beweisern unbrauchbar teuer.

Konsequenz

Richtig gestaltete Term-Indizes reduzieren die Zahl teurer syntaktischer Unifikationsversuche und senken so drastisch Laufzeiten und Speicherbelastung großer Beweisdatenbanken, wodurch skalierbare Dienste wie Prämissenauswahl und matchingbasierte Vereinfachung möglich werden.

Umkehrung

Ohne Term-Indexierung muss das System exhaustive paarweise Termvergleiche oder vollständige Durchsuchungen durchführen; der invertierte Gegensatz ist ein Index, der für modellorientierte semantische Abfragen (z. B. Indexierung von Valuationen) ausgelegt ist und andere Abruffunktionen bedient, jedoch nicht zwangsläufig der syntaktischen Unifikation dient.

Abgrenzung

Gilt für syntaktische Retrieval-Probleme (exakte Matches, Muster-Matches, syntaktische Unifikation). Liefert an sich keine semantische Folgerung, Modellprüfung oder probabilistische Ähnlichkeitssuche; schließt rein statistische Einbettungstechniken aus, sofern sie nicht ausdrücklich als approximative Indexschichten verwendet werden.

Semantische Spannung

Es besteht eine Spannung zwischen kompakten, schnell zu aktualisierenden Indizes, die viele grobe Kandidaten zurückgeben (hohe Recall, geringe Präzision), und reich strukturierten Indizes, die präzise, aber wartungsintensiv sind; eine weitere Spannung entsteht zwischen Indizes für Batch-Konstruktion und solchen für interaktive Inkrementarbeit.

Synthese

Term-Indexierung ist die Praxis, diskriminierende strukturelle Merkmale von Termen in Datenstrukturen (Diskriminationsbäume, Substitutionsbäume, Signatur-Hashes, Pfad-Indizes) zu organisieren, damit automatisierte Beweiser schnell Kandidatenmengen für Matching und Unifikation eingrenzen und dabei die Retrieval-Geschwindigkeit gegen Speicher- und Aktualisierungskosten abwägen.