package logtk

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Simple and Lightweight Congruence and order
1. Functor
2. Common implementations

logtk
- Logtk
  - Binder
    
    TPTP
    
    ZF
  - Builtin
    
    Arith
    
    ArithOp
    
    Map
    
    Set
    
    TPTP
    
    Tag
    
    Tbl
    
    ZF
  - Cnf
  - Comparison
    
    PARTIAL_ORD
  - Compute_prec
  - Congruence
    
    FO
    
    Make
    
    T
    
    TERM
  - Congruence_intf
    
    S
  - DBEnv
  - Defined_pos
    
    Arr
  - Dtree
    
    Default
    
    Make
    
    E
  - FV_tree
    
    Make
    
    C
    
    Feature_fun
  - FeatureVector
    
    Make
    
    C
    
    CSet
    
    Feature
    
    IntMap
  - Fingerprint
    
    Make
    
    Leaf
    
    X
  - FixpointUnif
  - Flex_state
  - HO_unif
  - HVar
  - Hash
  - Hashcons
    
    HashedType
    
    Make
    
    X
    
    MakeNonWeak
    
    X
    
    S
  - IArray
  - ID
    
    Map
    
    Set
    
    Tbl
  - Ind_ty
  - Index
    
    BasicEquation
    
    MakeLeaf
    
    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
    
    S
  - JP_unif
    
    S
  - Lambda
    
    Inner
  - LazyList
  - Literal
    
    Comp
    
    Conv
    
    Pos
    
    Seq
    
    Set
    
    View
  - Literals
    
    Conv
    
    Pos
    
    Seq
    
    View
  - Multiset
    
    Make
    
    Seq
    
    X
  - Multiset_intf
    
    S
    
    Seq
  - Multisets
    
    MMT
    
    Seq
    
    MT
    
    Seq
  - NPDtree
    
    Make
    
    E
    
    MakeTerm
    
    Leaf
    
    X
  - Options
  - Ordering
  - Output_format
  - PUnif
    
    IntSet
    
    Make
    
    S
  - ParseLocation
    
    Infix
  - PatternUnif
    
    S
  - Polynomial
    
    IntegerModule
    
    Make
    
    Coeff
    
    Indet
    
    OrderedType
    
    S
  - Position
    
    Build
    
    Map
    
    With
    
    Infix
  - PragUnifParams
  - Precedence
    
    Constr
    
    Seq
    
    Weight
    
    Infix
  - PrefWeight
    
    Make
    
    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
    
    S
  - SolidUnif
    
    Make
    
    S
  - Statement
    
    Seq
    
    TPTP
    
    ZF
  - Subst
    
    FO
    
    Projection
    
    Renaming
    
    SPECIALIZED
    
    Ty
  - Term
    
    AC
    
    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
    
    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
logtk.arith
- Logtk_arith
  - Q
  - Z
logtk.parsers
- Logtk_parsers
  - Ast_dk
  - Ast_tptp
  - CallProver
    
    Eprover
    
    Prover
  - Lex_dk
  - Lex_tptp
  - Lex_zf
  - Parse_dk
  - Parse_tptp
  - Parse_zf
  - Parsing_utils
  - Tip_ast
  - Tip_lexer
  - Tip_parser
  - Trace_tstp
    
    StepTbl
  - Util_dk
  - Util_tip
  - Util_tptp
  - Util_zf
logtk.proofs
- Logtk_proofs
  - LLProof
    
    Dot
    
    Tbl
  - LLProof_check
  - LLProof_conv
  - LLProver
  - LLTerm
    
    Conv
    
    Form
    
    Int_op
    
    LINEXP
    
    Linexp_int
    
    Linexp_rat
    
    Rat_op
    
    Set
logtk.solving
- Logtk_solving
  - Lpo
    
    Constraint
    
    Seq
    
    FO
    
    Solution
    
    TypedSTerm

Legend:
Library
Module
Module type
Parameter
Class
Class type

Simple and Lightweight Congruence and order

Congruence Closure provides an efficient, lightweight procedure for deciding equality on ground terms (i.e. ignoring variables). Here we have a simple implementation that is mostly used to check if clauses are tautologies w.r.t. equality

module type S = Congruence_intf.S

Functor

module type TERM = sig ... end

module Make (T : TERM) : S with type term = T.t

Common implementations

module FO : S with type term = Term.t