package logtk

  1. Overview
  2. Docs
package logtk
Legend:
Library
Module
Module type
Parameter
Class
Class type
type rule
module Rule : sig ... end
val normalize_clause : Literals.t -> (Literals.t list * rule * Subst.t * Scoped.scope * Subst.Renaming.t * Proof.tag list) option

normalize literals of the clause w.r.t. rules, or return None if no rule applies. The input clause lives in scope 0.

val narrow_lit : ?subst:Unif_subst.t -> scope_rules:Scoped.scope -> Literal.t Scoped.t -> (rule * Unif_subst.t * Proof.tag list) Iter.t

narrow_term rules lit finds the set of rules (l --> clauses) in rules and substitutions sigma such that sigma(l) = sigma(lit)

  • parameter scope_rules

    used for rules (LEFT)