package logtk

  1. Overview
  2. Docs

Module Logtk.Dtree

Perfect Discrimination Tree

This module provides a simplification index, based on a perfect discrimination tree (see "the handbook of automated reasoning", chapter "term indexing", for instance).

The simplification index can only retrieve generalizations of a given query term, but it does it efficiently.

It is used for demodulation (rewriting) in Superposition.

module Make (E : Index.EQUATION) : Index.UNIT_IDX with module E = E