Term-Indexierung

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.