package logtk

You can search for identifiers within the package.

in-package search v0.2.0

logtk
- Logtk
- LogtkCache
  - Dummy
    
    X
  - Dummy2
    
    X
    
    Y
  - EQ
  - HASH
  - LRU
    
    X
  - Linear
    
    X
  - Linear2
    
    X
    
    Y
  - Replacing
    
    X
  - Replacing2
    
    X
    
    Y
  - S
  - S2
- LogtkCnf
- LogtkComparison
  - PARTIAL_ORD
- LogtkCongruence
  - FO
  - HO
  - Make
    
    T
  - S
  - TERM
- LogtkDBEnv
- LogtkDtree
  - Default
  - Make
    
    E
- LogtkFOTerm
  - AC
    
    A
  - AC_SPEC
  - Classic
  - Pos
  - Seq
  - T2LogtkCache
  - TLogtkCache
  - TPTP
    
    Arith
  - Tbl
- LogtkFastFingerprint
  - Make
    
    Leaf
- LogtkFeatureVector
  - Make
    
    C
    
    Feature
- LogtkFingerprint
  - Make
    
    Leaf
- LogtkFormula
  - FO
    
    Base
    
    Seq
    
    TPTP
  - Make
    
    Base
    
    MyT
    
    Seq
    
    TPTP
    
    Seq
    
    TPTP
  - Map
    
    From
    
    Base
    
    Seq
    
    TPTP
    
    To
    
    Base
    
    Seq
    
    TPTP
  - S
    
    Base
    
    Seq
    
    TPTP
  - TERM
    
    Seq
    
    TPTP
- LogtkFormulaShape
- LogtkHORewriting
  - Seq
- LogtkHOTerm
  - LogtkCache
  - Pos
  - Seq
  - TPTP
  - Tbl
  - any_visitor
  - id_visitor
- LogtkHashcons
  - HashedLogtkType
  - Make
    
    X
  - S
- LogtkIArray
  - Seq
- LogtkIndex
  - BasicEquation
  - CLAUSE
  - EQUATION
  - LEAF
  - MakeLeaf
  - SUBSUMPTION_IDX
    
    C
  - TERM_IDX
    
    Leaf
  - UNIT_IDX
    
    E
- LogtkInterfaces
  - EQ
  - GROUP
  - HASH
  - ITER
  - MONOID
  - ORD
  - PRINT
  - PRINT1
  - PRINT_DE_BRUIJN
  - PRINT_OVERLOAD
- LogtkLambda
- LogtkLazyGraph
  - Dot
  - Full
  - Heap
  - Infix
  - Mutable
- LogtkLazyList
- LogtkMultiset
  - Make
    
    Seq
  - S
    
    Seq
- LogtkNPDtree
  - Make
    
    E
  - MakeTerm
    
    Leaf
- LogtkOptions
- LogtkOrdering
  - Default
  - Make
    
    P
    
    Constr
    
    Seq
- LogtkOrdering_intf
  - S
    
    Prec
    
    Constr
    
    Seq
- LogtkParseLocation
- LogtkPartialOrder
  - ELEMENT
  - Make
    
    E
- LogtkPartialOrder_intf
  - S
- LogtkPosition
  - Build
- LogtkPrecedence
  - Constr
  - Default
    
    Constr
    
    Seq
  - Make
    
    Constr
    
    Seq
    
    Sym
  - SYMBOL
  - Seq
- LogtkPrecedence_intf
  - S
    
    Constr
    
    Seq
- LogtkPrologTerm
  - Seq
  - TPTP
  - id_visitor
  - visitor
- LogtkRewriting
  - FormRW
  - MakeOrdered
    
    E
  - MakeTRS
    
    I
    
    E
  - ORDERED
    
    E
  - SIG_TRS
  - TRS
- LogtkScopedTerm
  - DB
  - Kind
  - Pos
  - Seq
  - Tbl
- LogtkSignature
  - Seq
  - TPTP
    
    Arith
- LogtkSkolem
- LogtkSourced
- LogtkSubsts
  - FO
  - Form
  - HO
  - Renaming
  - SPECIALIZED
  - Ty
- LogtkSymbol
  - ArithOp
  - Base
  - Seq
  - TPTP
    
    Arith
- LogtkTransform
  - DAG
    
    Form
  - FORM
  - FormDag
    
    Form
  - MakeDAG
    
    Form
- LogtkType
  - Conv
  - Seq
  - TPTP
- LogtkTypeInference
  - Closure
  - Ctx
  - FO
  - HO
  - S
- LogtkTypedPrologTerm
  - Seq
  - Subst
  - Visitor
- LogtkUnif
  - FO
  - Form
  - HO
  - NARY
  - Nary
  - Ty
  - UNARY
  - Unary
- LogtkUtil
  - Exn
  - Flag
  - Section

Legend:
Library
Module
Module type
Parameter
Class
Class type

type term = LogtkFOTerm.t

val unification : 
  ?env1:env ->
  ?env2:env ->
  ?subst:subst ->
  term ->
  scope ->
  term ->
  scope ->
  subst

LogtkUnify terms, returns a subst or

raises Fail
if the terms are not unifiable

parameter env1
environment for the first term

parameter env2
environment for the second term

val matching : 
  ?allow_open:bool ->
  ?env1:env ->
  ?env2:env ->
  ?subst:subst ->
  pattern:term ->
  scope ->
  term ->
  scope ->
  subst

matching ~pattern scope_p b scope_b returns sigma such that sigma pattern = b, or fails. Only variables from the scope of pattern can be bound in the subst.

parameter subst
initial substitution (default empty)

parameter allow_open
if true, variables can bind to non-closed DB terms (default false)

raises Fail
if the terms do not match.

raises Invalid_argument
if the two scopes are equal

val matching_same_scope : 
  ?env1:env ->
  ?env2:env ->
  ?protect:term Sequence.t ->
  ?subst:subst ->
  scope:scope ->
  pattern:term ->
  term ->
  subst

matches pattern (more general) with the other term. The two terms live in the same scope, which is passed as the scope argument. It needs to gather the variables of the other term to make sure they are not bound.

parameter scope
the common scope of both terms

parameter protect
a sequence of variables to protect (they cannot be bound during matching!). Variables of the second term are automatically protected.

val matching_adapt_scope : 
  ?env1:env ->
  ?env2:env ->
  ?protect:term Sequence.t ->
  ?subst:subst ->
  pattern:term ->
  scope ->
  term ->
  scope ->
  subst

Call either matching or matching_same_scope depending on whether the given scopes are the same or not.

parameter protect
used if scopes are the same, see matching_same_scope

val variant : 
  ?env1:env ->
  ?env2:env ->
  ?subst:subst ->
  term ->
  scope ->
  term ->
  scope ->
  subst

Succeeds iff the first term is a variant of the second, ie if they are alpha-equivalent

val eq : 
  ?env1:env ->
  ?env2:env ->
  subst:subst ->
  term ->
  scope ->
  term ->
  scope ->
  bool

eq subst t1 s1 t2 s2 returns true iff the two terms are equal under the given substitution, i.e. if applying the substitution will return the same term.

val are_unifiable : term -> term -> bool

val matches : pattern:term -> term -> bool

val are_variant : term -> term -> bool