Logtk.Unif_intf · logtk 2.1

logtk

Core types and algorithms for logic

package logtk

logtk
- Logtk
  - Binder
    
    TPTP
    
    ZF
  - Builtin
    
    Arith
    
    ArithOp
    
    Map
    
    Set
    
    TPTP
    
    Tag
    
    Tbl
    
    ZF
  - Cnf
  - Comparison
    
    PARTIAL_ORD
  - Compute_prec
  - Congruence
    
    FO
    
    Make
    
    1-T
    
    TERM
  - Congruence_intf
    
    S
  - DBEnv
  - Defined_pos
    
    Arr
  - Dtree
    
    Default
    
    Make
    
    1-E
  - FV_tree
    
    Make
    
    1-C
    
    Feature_fun
  - FeatureVector
    
    Make
    
    1-C
    
    CSet
    
    Feature
    
    IntMap
  - Fingerprint
    
    Make
    
    1-X
    
    Leaf
  - FixpointUnif
  - Flex_state
  - HO_unif
  - HVar
  - Hash
  - Hashcons
    
    HashedType
    
    Make
    
    1-X
    
    MakeNonWeak
    
    1-X
    
    S
  - IArray
  - ID
    
    Map
    
    Set
    
    Tbl
  - Ind_ty
  - Index
    
    BasicEquation
    
    MakeLeaf
    
    1-X
  - Index_intf
    
    CLAUSE
    
    EQUATION
    
    LEAF
    
    SUBSUMPTION_IDX
    
    C
    
    TERM_IDX
    
    Leaf
    
    UNIT_IDX
    
    E
  - InnerTerm
    
    DB
    
    Map
    
    Pos
    
    Seq
    
    Set
    
    Tbl
    
    VarMap
    
    VarSet
    
    VarTbl
  - Input_format
  - Interfaces
    
    EQ
    
    GROUP
    
    HASH
    
    ITER
    
    MONOID
    
    ORD
    
    PRINT
    
    PRINT1
    
    PRINT2
    
    PRINT3
    
    PRINT_DE_BRUIJN
    
    PRINT_OVERLOAD
  - JPFull
    
    Make
    
    1-S
  - JP_unif
    
    S
  - Lambda
    
    Inner
  - LazyList
  - Literal
    
    Comp
    
    Conv
    
    Pos
    
    Seq
    
    Set
    
    View
  - Literals
    
    Conv
    
    Pos
    
    Seq
    
    View
  - Multiset
    
    Make
    
    1-X
    
    Seq
  - Multiset_intf
    
    S
    
    Seq
  - Multisets
    
    MMT
    
    Seq
    
    MT
    
    Seq
  - NPDtree
    
    Make
    
    1-E
    
    MakeTerm
    
    1-X
    
    Leaf
  - Options
  - Ordering
  - Output_format
  - PUnif
    
    IntSet
    
    Make
    
    1-S
  - ParseLocation
    
    Infix
  - PatternUnif
    
    S
  - Polynomial
    
    IntegerModule
    
    Make
    
    1-Coeff
    
    2-Indet
    
    OrderedType
    
    S
  - Position
    
    Build
    
    Map
    
    With
    
    Infix
  - PragUnifParams
  - Precedence
    
    Constr
    
    Seq
    
    Weight
    
    Infix
  - PrefWeight
    
    Make
    
    1-PARAMETERS
    
    S
  - Proof
    
    Kind
    
    Parent
    
    Result
    
    Rule
    
    S
    
    Tbl
    
    Src
    
    Step
  - Rewrite
    
    Defined_cst
    
    Lit
    
    Rule
    
    Rule
    
    Rule_set
    
    Term
    
    Rule
    
    Rule_inst_set
    
    Set
  - SLiteral
    
    TPTP
    
    ZF
  - STerm
    
    Map
    
    Seq
    
    Set
    
    StrMap
    
    StringSet
    
    TPTP
    
    TPTP_THF
    
    Tbl
    
    ZF
  - Scoped
  - Signal
  - Signature
    
    Seq
  - Skolem
  - SolidSubsumption
    
    Make
    
    1-S
  - SolidUnif
    
    Make
    
    1-S
  - Statement
    
    Seq
    
    TPTP
    
    ZF
  - Subst
    
    FO
    
    Projection
    
    Renaming
    
    SPECIALIZED
    
    Ty
  - Term
    
    AC
    
    1-A
    
    AC_SPEC
    
    Arith
    
    Classic
    
    Conv
    
    DB
    
    Form
    
    IntMap
    
    Map
    
    Pos
    
    Seq
    
    Set
    
    TPTP
    
    Tbl
    
    VarMap
    
    VarSet
    
    VarTbl
    
    ZF
  - Type
    
    Conv
    
    Map
    
    Seq
    
    Set
    
    TPTP
    
    Tbl
    
    VarMap
    
    VarSet
    
    VarTbl
    
    ZF
  - TypeInference
    
    Ctx
    
    TyBuiltin
  - TypedSTerm
    
    Form
    
    Map
    
    Seq
    
    Set
    
    Subst
    
    TPTP
    
    TPTP_THF
    
    Tbl
    
    Ty
    
    UStack
    
    Var_tbl
    
    ZF
  - Unif
    
    FO
    
    Inner
    
    Ty
  - UnifFramework
    
    Make
    
    1-X
    
    PARAMETERS
    
    S
    
    US
  - Unif_constr
    
    FO
  - Unif_intf
    
    S
  - Unif_subst
    
    FO
  - UntypedAST
    
    A
  - Util
    
    Exn
    
    Flag
    
    Int_map
    
    Int_set
    
    Section
  - Var
    
    Set
    
    Subst
  - ZProf

Legend:
Library
Module
Module type
Parameter
Class
Class type

Library logtk

Module Logtk . Unif_intf

Interface for unification

type unif_subst = Unif_subst.t

type subst = Subst.t

module type S = sig ... end

logtk 2.1 2.0 1.6 1.5.1 0.8.1

Interface for unification

logtk