package logtk

  1. Overview
  2. Docs
package logtk
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Logtk.NPDtreeSource

Non-Perfect Discrimination Tree

This module provides a simplification index and a term index, based on a non-perfect discrimination tree (see "the handbook of automated reasoning", chapter "term indexing", for instance). It should be more compact in memory than Dtree, and maybe more optimized too.

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