logtk

Core types and algorithms for logic
IN THIS PACKAGE
Module Logtk . FeatureVector

Feature Vector indexing

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

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

type lits = Index_intf.lits
module Make (C : Index.CLAUSE) : sig ... end