Termindexering

Inom datavetenskap är ett termindex en datastruktur för att underlätta snabb uppslagning av termer och klausuler i ett logikprogram , deduktiv databas eller automatiserad teoremprovare .

Översikt

Många operationer i automatiska teoremprovare kräver sökning i enorma samlingar av termer och satser. Sådana operationer faller vanligtvis inom följande schema. Med tanke på en samling $S$ av termer (satser) och en frågeterm (klausul) $q$ , hitta i $S$ några/alla termer $t$ relaterade till ${ \displaystyle q}$ enligt ett visst hämtningsvillkor. De mest intressanta hämtningsvillkoren är formulerade som förekomsten av en substitution som på ett speciellt sätt relaterar frågan och de hämtade objekten t {\ $t}$ . Här är en lista över hämtningstillstånd som ofta används i prover:

• term $q$ kan förenas med term $t$ , dvs det finns en substitution ${\displaystyle \theta } ,$ så att $q\theta$ = $t \theta$
• term $t$ är en instans av $q$ , dvs det finns en substitution ${\displaystyle \theta } ,$ så att $q\theta$ = $t$
• term $t$ är en generalisering av $q$ , dvs det finns en substitution ${\displaystyle \theta } ,$ så att $q$ = $t\theta$
• sats $q$ subsumerar sats $t$ , dvs det finns en substitution ${\displaystyle \theta } ,$ så att $q\theta$ är en delmängd/submultis av ${\ displaystil t}$
• klausul $q$ subsumeras av $t$ , dvs det finns en substitution ${\displaystyle \theta } ,$ så att $t\theta$ är en delmängd/submultis av ${ \displaystyle q}$

Oftare än inte är vi faktiskt intresserade av att hitta lämpliga substitutioner explicit, tillsammans med de hämtade termerna $\displaystyle t}$ , snarare än att bara fastställa existensen av sådana substitutioner.

Mycket ofta är storleken på termuppsättningar som ska sökas stora, hämtningsanropen är frekventa och hämtningsvillkorstestet är ganska komplicerat. I sådana situationer blir linjär sökning i $S$ , när hämtningsvillkoret testas på varje term från $S$ , oöverkomligt kostsam. För att övervinna detta problem är speciella datastrukturer, kallade index , utformade för att stödja snabb hämtning. Sådana datastrukturer, tillsammans med de tillhörande algoritmerna för indexunderhåll och hämtning, kallas termindexeringstekniker .

Klassiska indexeringstekniker

• diskrimineringsträd
• substitutionsträd
• banindexering

Substitutionsträd överträffar banindexering, diskrimineringsträdindexering och abstraktionsträd.

Ett termindex för diskrimineringsträd lagrar sin information i en försöksdatastruktur .

Moderna indexeringstekniker

• funktionsvektorindexering
• kodträd
• sammanhang träd
• relationell vägindexering

Vidare läsning

• P. Graf, Term Indexing, Lecture Notes in Computer Science 1053, 1996 (något föråldrad översikt)
• R. Sekar och IV Ramakrishnan och A. Voronkov, Term Indexing, i A. Robinson och A. Voronkov, redaktörer, Handbook of Automated Reasoning , volym 2, 2001 (nyare översikt)
• WW McCune, Experiments with Discrimination-Tree Indexing and Path Indexing for Term Retrieval, Journal of Automated Reasoning, 9(2), 1992
• P. Graf, Substitution Tree Indexing, Proc. of RTA, Lecture Notes in Computer Science 914, 1995
• M. Stickel, The Path Indexing Method for Indexing Terms, Tech. Rep. 473, Artificiell intelligens Center , SRI International , 1989
• S. Schulz, Enkel och effektiv klausulsubsumtion med funktionsvektorindexering, Proc. av IJCAR-2004 workshop ESFOR, 2004
• A. Riazanov och A. Voronkov, Partially Adaptive Code Trees, Proc. JELIA, föreläsningsanteckningar i artificiell intelligens 1919, 2000
• H. Ganzinger och R. Nieuwenhuis och P. Nivela, Fast Term Indexing with Coded Context Trees, Journal of Automated Reasoning, 32(2), 2004
• A. Riazanov och A. Voronkov, Efficient Instance Retrieval with Standard and Relational Path Indexing, Information and Computation, 199(1–2), 2005