package logtk

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

Module Logtk.FV_treeSource

Feature Vector indexing

Feature Vector indexing (see Schulz 2004) for efficient forward and backward subsumption on Horn Clauses.

This allows to retrieve clauses that (potentially) subsume or are subsumed by a given query clause.

This module is a modified version of FeatureVector, with full-signature features that encompass all symbols at the same time.

Sourcetype feature =
  1. | N of int
  2. | S of ID.Set.t
  3. | M of int ID.Map.t
  4. | L of labels
Sourcetype feature_vector = feature IArray.t

a vector of feature

Sourcemodule Make (C : Index_intf.CLAUSE) : sig ... end
OCaml

Innovation. Community. Security.