Term Indexing Task

See: Logical Term Index Creation Task, Document Index Creation Task.

---

---

References

2009

• http://en.wikipedia.org/wiki/Term_indexing
  • 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 [math]\displaystyle{ S }[/math] of terms (clauses) and a query term (clause) [math]\displaystyle{ q }[/math], find in [math]\displaystyle{ S }[/math] some/all terms [math]\displaystyle{ t }[/math] related to [math]\displaystyle{ 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]\displaystyle{ t }[/math]. Here is a list of retrieval conditions frequently used in provers:
    • term [math]\displaystyle{ q }[/math] is unifiable with term [math]\displaystyle{ t }[/math], i.e., there exists a substitution [math]\displaystyle{ \theta }[/math], such that [math]\displaystyle{ q\theta }[/math] = [math]\displaystyle{ t\theta }[/math]
    • term [math]\displaystyle{ t }[/math] is an instance of [math]\displaystyle{ q }[/math], i.e., there exists a substitution [math]\displaystyle{ \theta }[/math], such that [math]\displaystyle{ q\theta }[/math] = [math]\displaystyle{ t }[/math]
    • term [math]\displaystyle{ t }[/math] is a generalisation of [math]\displaystyle{ q }[/math], i.e., there exists a substitution [math]\displaystyle{ \theta }[/math], such that [math]\displaystyle{ q }[/math] = [math]\displaystyle{ t\theta }[/math]
    • clause [math]\displaystyle{ q }[/math] subsumes clause [math]\displaystyle{ t }[/math], i.e., there exists a substitution [math]\displaystyle{ \theta }[/math], such that [math]\displaystyle{ q\theta }[/math] is a subset/submultiset of [math]\displaystyle{ t }[/math]
    • clause [math]\displaystyle{ q }[/math] is subsumed by [math]\displaystyle{ t }[/math], i.e., there exists a substitution [math]\displaystyle{ \theta }[/math], such that [math]\displaystyle{ t\theta }[/math] is a subset/submultiset of [math]\displaystyle{ q }[/math]

2003

• (Jacquemin & Bourigault, 2003) ⇒ Christian Jacquemin, and Didier Bourigault. (2003). “Term Extraction and Automatic Indexing.” In: (Mitkov, 2003) ⇒ Ruslan Mitkov, editor. (2003). “The Oxford Handbook of Computational Linguistics." Oxford University Press.

1995

• (Graf, 1995) ⇒ Peter Graf. (1995). “Term Indexing." Springer. ISBN:3540610405

---