Arbitrage betting: Difference between revisions

Revision as of 17:05, 16 January 2014

In computer science, term indexing is the task of creating an index of terms and clauses in a collection.

Many operations in automatic theorem provers require search in huge collections of terms and clauses. Such operations typically fall into the following scheme. Given a collection $S$ of terms (clauses) and a query term (clause) $q$ , find in $S$ some/all terms $t$ related to $q$ according to a certain retrieval condition. Most interesting retrieval conditions are formulated as existence of a substitution that relates in a special way the query and the retrieved objects $t$ . Here is a list of retrieval conditions frequently used in provers:

term $q$ is unifiable with term $t$ , i.e., there exists a substitution $θ$ , such that $q θ$ = $t θ$
term $t$ is an instance of $q$ , i.e., there exists a substitution $θ$ , such that $q θ$ = $t$
term $t$ is a generalisation of $q$ , i.e., there exists a substitution $θ$ , such that $q$ = $t θ$
clause $q$ subsumes clause $t$ , i.e., there exists a substitution $θ$ , such that $q θ$ is a subset/submultiset of $t$
clause $q$ is subsumed by $t$ , i.e., there exists a substitution $θ$ , such that $t θ$ is a subset/submultiset of $q$

More often than not, we are actually interested in finding the appropriate substitutions explicitly, together with the retrieved terms $t$ , rather than just in establishing existence of such substitutions.

Very often the sizes of term sets to be searched are large, the retrieval calls are frequent and the retrieval condition test is rather complex. In such situations linear search in $S$ , when the retrieval condition is tested on every term from $S$ , becomes prohibitively costly. To overcome this problem, special data structures, called indexes, are designed in order to support fast retrieval. Such data structures, together with the accompanying algorithms for index maintenance and retrieval, are called term indexing techniques.

Classic indexing techniques

Modern indexing techniques

P. Graf, Term Indexing, Lecture Notes in Computer Science 1053, 1996 (slightly outdated overview)
R. Sekar and I.V. Ramakrishnan and A. Voronkov, Term Indexing, in A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, volume 2, 2001 (recent overview)
W. W. 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, Artificial Intelligence Center, SRI International, 1989
S. Schulz, Simple and Efficient Clause Subsumption with Feature Vector Indexing, Proc. of IJCAR-2004 workshop ESFOR, 2004
A. Riazanov and A. Voronkov, Partially Adaptive Code Trees, Proc. JELIA, Lecture Notes in Artificial Intelligence 1919, 2000
H. Ganzinger and R. Nieuwenhuis and P. Nivela, Fast Term Indexing with Coded Context Trees, Journal of Automated Reasoning, 32(2), 2004
A. Riazanov and A. Voronkov, Efficient Instance Retrieval with Standard and Relational Path Indexing, Information and Computation, 199(1–2), 2005

fr:Index terminologique pl:Indeksowanie termów

@@ Line 1: / Line 1: @@
-I would like to introduce myself to you, I am Andrew and my wife doesn't like it at all. To perform lacross is one of the things she loves most. My day job is a journey agent. For years he's been residing in Alaska and he doesn't strategy on altering it.<br><br>My weblog: psychic phone ([http://Conniecolin.com/xe/community/24580 visit the up coming site])
+In [[computer science]], '''term indexing''' is the task of creating an [[index (search engine)|index]] of terms and clauses in a collection.
+Many operations in automatic [[Automated theorem prover|theorem prover]]s require search in huge
+collections of terms and clauses. Such operations typically fall into
+the following scheme. Given a collection <math>S</math> of terms (clauses) and a query
+term (clause) <math>q</math>, find in <math>S</math> some/all terms <math>t</math> related to <math>q</math> according to a
+certain retrieval condition. Most interesting retrieval conditions
+are formulated as existence of a substitution that relates in a special
+way the query and the retrieved objects <math>t</math>. Here is a list of retrieval
+conditions frequently used in provers:
+* term <math>q</math> is unifiable with term <math>t</math>, i.e., there exists a substitution <math> \theta </math>, such that <math>q\theta</math> = <math>t\theta</math>
+* term <math>t</math> is an instance of <math>q</math>, i.e., there exists a substitution <math>\theta</math>, such that <math>q\theta</math> = <math>t</math>
+* term <math>t</math> is a generalisation of <math>q</math>, i.e., there exists a substitution <math>\theta</math>, such that <math>q</math> = <math>t\theta</math>
+* clause <math>q</math> subsumes clause <math>t</math>, i.e., there exists a substitution <math>\theta</math>, such that <math>q\theta</math> is a subset/submultiset of <math>t</math>
+* clause <math>q</math> is subsumed by <math>t</math>, i.e., there exists a substitution <math>\theta</math>, such that <math>t\theta</math> is a subset/submultiset of <math>q</math>
+More often than not, we are actually interested in finding the appropriate
+substitutions explicitly, together with the retrieved terms <math>t</math>,
+rather than just in establishing existence of such substitutions.
+Very often the sizes of term sets to be searched are large,
+the retrieval calls are frequent and the retrieval condition test
+is rather complex. In such situations linear search in <math>S</math>, when the retrieval
+condition is tested on every term from <math>S</math>, becomes prohibitively costly.
+To overcome this problem, special data structures, called ''indexes'', are
+designed in order to support fast retrieval. Such data structures,
+together with the accompanying algorithms for index maintenance
+and retrieval, are called ''term indexing techniques''.
+==Classic indexing techniques==
+* [[discrimination tree]]s
+* [[substitution tree]]s
+* [[path indexing]]
+==Modern indexing techniques==
+* [[feature vector indexing]]
+* [[code tree]]s
+* [[context tree]]s
+* [[relational path indexing]]
+==Further reading==
+* P. Graf, Term Indexing, Lecture Notes in Computer Science 1053, 1996 (slightly outdated overview)
+* R. Sekar and I.V. Ramakrishnan and A. Voronkov, Term Indexing, in A. Robinson and A. Voronkov, editors, [[Handbook of Automated Reasoning]], volume 2, 2001 (recent overview)
+* W. W. 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, [[Artificial Intelligence Center]], [[SRI International]], 1989
+* S. Schulz, Simple and Efficient Clause Subsumption with Feature Vector Indexing, Proc. of IJCAR-2004 workshop ESFOR, 2004
+* A. Riazanov and A. Voronkov, Partially Adaptive Code Trees, Proc. JELIA, Lecture Notes in Artificial Intelligence 1919, 2000
+* H. Ganzinger and R. Nieuwenhuis and P. Nivela, Fast Term Indexing with Coded Context Trees, Journal of Automated Reasoning, 32(2), 2004
+* A. Riazanov and A. Voronkov, Efficient Instance Retrieval with Standard and Relational Path Indexing, Information and Computation, 199(1–2), 2005
+{{DEFAULTSORT:Term Indexing}}
+[[Category:Searching]]
+[[fr:Index terminologique]]
+[[pl:Indeksowanie termów]]

Arbitrage betting: Difference between revisions

Revision as of 17:05, 16 January 2014

Classic indexing techniques

Modern indexing techniques

Further reading

Navigation menu

Search