package logtk

You can search for identifiers within the package.

in-package search v0.2.0

package logtk

logtk
- CHANGELOG
- README
- Library logtk
  - Logtk
    
    AllocCache
    
    Arr
    
    Binder
    
    TPTP
    
    ZF
    
    Builtin
    
    Arith
    
    Map
    
    Set
    
    Tbl
    
    Tag
    
    TPTP
    
    ArithOp
    
    ZF
    
    Cnf
    
    Comparison
    
    PARTIAL_ORD
    
    Compute_prec
    
    Congruence
    
    S
    
    TERM
    
    Make
    
    FO
    
    Congruence_intf
    
    S
    
    DBEnv
    
    Defined_pos
    
    Fmt
    
    Arr
    
    Dtree
    
    Make
    
    E
    
    Default
    
    E
    
    FV_tree
    
    Make
    
    Feature_fun
    
    C
    
    FeatureVector
    
    Make
    
    Feature
    
    C
    
    Fingerprint
    
    Make
    
    Leaf
    
    FixpointUnif
    
    T
    
    US
    
    Flex_state
    
    HO_unif
    
    HVar
    
    Hash
    
    Hashcons
    
    HashedType
    
    S
    
    Make
    
    MakeNonWeak
    
    IArray
    
    ID
    
    Map
    
    Set
    
    Tbl
    
    Ind_ty
    
    Index
    
    LEAF
    
    MakeLeaf
    
    TERM_IDX
    
    CLAUSE
    
    SUBSUMPTION_IDX
    
    EQUATION
    
    BasicEquation
    
    UNIT_IDX
    
    Index_intf
    
    LEAF
    
    TERM_IDX
    
    Leaf
    
    CLAUSE
    
    SUBSUMPTION_IDX
    
    C
    
    EQUATION
    
    UNIT_IDX
    
    E
    
    InnerTerm
    
    I
    
    Map
    
    Set
    
    Tbl
    
    VarMap
    
    VarSet
    
    VarTbl
    
    DB
    
    Seq
    
    Pos
    
    Input_format
    
    Int_lit
    
    Seq
    
    Focus
    
    Util
    
    Interfaces
    
    EQ
    
    HASH
    
    ORD
    
    PRINT
    
    PRINT1
    
    PRINT2
    
    PRINT3
    
    PRINT_OVERLOAD
    
    PRINT_DE_BRUIJN
    
    ITER
    
    MONOID
    
    GROUP
    
    JPFull
    
    Make
    
    JP_unif
    
    T
    
    US
    
    S
    
    Lambda
    
    Inner
    
    LazyList
    
    Literal
    
    Set
    
    Comp
    
    Seq
    
    Pos
    
    View
    
    Conv
    
    Literals
    
    Seq
    
    Pos
    
    Conv
    
    View
    
    Monome
    
    Seq
    
    Focus
    
    Int
    
    Modulo
    
    Solve
    
    Rat
    
    Multiset
    
    S
    
    Make
    
    Seq
    
    Multiset_intf
    
    S
    
    Seq
    
    Multisets
    
    MT
    
    Seq
    
    MMT
    
    Seq
    
    NPDtree
    
    Make
    
    E
    
    MakeTerm
    
    Leaf
    
    Options
    
    Ordering
    
    Ordinal
    
    Output_format
    
    PUnif
    
    IntSet
    
    Make
    
    ParseLocation
    
    Infix
    
    PatternUnif
    
    T
    
    US
    
    S
    
    Position
    
    Map
    
    Build
    
    With
    
    Infix
    
    PragUnifParams
    
    Precedence
    
    Weight
    
    Infix
    
    Constr
    
    Seq
    
    Proof
    
    Loc
    
    Tag
    
    Rule
    
    Kind
    
    Src
    
    Result
    
    Step
    
    Parent
    
    S
    
    Tbl
    
    Rat_lit
    
    Seq
    
    Focus
    
    Rewrite
    
    Term
    
    Rule
    
    Set
    
    Rule_inst_set
    
    Lit
    
    Rule
    
    Rule
    
    Rule_set
    
    Defined_cst
    
    SLiteral
    
    TPTP
    
    ZF
    
    STerm
    
    Set
    
    Map
    
    Tbl
    
    StringSet
    
    Seq
    
    TPTP
    
    TPTP_THF
    
    ZF
    
    StrMap
    
    Scoped
    
    Signal
    
    Signature
    
    Seq
    
    Skolem
    
    SolidSubsumption
    
    Make
    
    SolidUnif
    
    T
    
    US
    
    Make
    
    Statement
    
    Seq
    
    ZF
    
    TPTP
    
    Subst
    
    Renaming
    
    SPECIALIZED
    
    Ty
    
    FO
    
    Projection
    
    Term
    
    Classic
    
    IntMap
    
    Set
    
    Map
    
    Tbl
    
    VarSet
    
    VarMap
    
    VarTbl
    
    Seq
    
    Pos
    
    AC_SPEC
    
    AC
    
    Form
    
    Arith
    
    DB
    
    TPTP
    
    ZF
    
    Conv
    
    Test_prop
    
    Type
    
    Set
    
    Map
    
    Tbl
    
    Seq
    
    VarSet
    
    VarMap
    
    VarTbl
    
    TPTP
    
    ZF
    
    Conv
    
    TypeInference
    
    TyBuiltin
    
    Ctx
    
    TypedSTerm
    
    Ty
    
    Form
    
    Set
    
    Map
    
    Tbl
    
    Seq
    
    Subst
    
    Var_tbl
    
    UStack
    
    TPTP
    
    TPTP_THF
    
    ZF
    
    Unif
    
    S
    
    Inner
    
    Ty
    
    FO
    
    UnifFramework
    
    S
    
    LL
    
    T
    
    PARAMETERS
    
    Make
    
    Unif_constr
    
    FO
    
    Unif_intf
    
    S
    
    Unif_subst
    
    FO
    
    UnionFind
    
    PAIR
    
    Make
    
    UntypedAST
    
    Loc
    
    T
    
    A
    
    Util
    
    Section
    
    Exn
    
    Flag
    
    Int_map
    
    Int_set
    
    Var
    
    Set
    
    Subst
- Library logtk.parsers
  - Logtk_parsers
    
    Ast_dk
    
    A
    
    T
    
    Set
    
    Map
    
    Tbl
    
    StringSet
    
    Seq
    
    TPTP
    
    TPTP_THF
    
    ZF
    
    StrMap
    
    Ast_tptp
    
    CallProver
    
    A
    
    Prover
    
    Eprover
    
    Lex_dk
    
    Lex_tptp
    
    Lex_zf
    
    Parse_dk
    
    Parse_tptp
    
    Parse_zf
    
    Parsing_utils
    
    Tip_ast
    
    Loc
    
    Tip_lexer
    
    A
    
    Loc
    
    Tip_parser
    
    Trace_tstp
    
    StepTbl
    
    Util_dk
    
    A
    
    Util_tip
    
    A
    
    Util_tptp
    
    A
    
    Util_zf
- Library logtk.proofs
  - Logtk_proofs
    
    LLProof
    
    Tbl
    
    Dot
    
    LLProof_check
    
    LLProof_conv
    
    LLProver
    
    LLTerm
    
    Int_op
    
    Rat_op
    
    LINEXP
    
    Linexp_int
    
    Linexp_rat
    
    Form
    
    Set
    
    Conv
- Library logtk.solving
  - Logtk_solving
    
    Lpo
    
    Constraint
    
    Seq
    
    Solution
    
    FO
    
    TypedSTerm
- Sources
  - logtk
    
    AllocCache.ml
    
    Binder.ml
    
    Builtin.ml
    
    Cnf.ml
    
    Comparison.ml
    
    Compute_prec.ml
    
    Congruence.ml
    
    Congruence_intf.ml
    
    DBEnv.ml
    
    Defined_pos.ml
    
    Dtree.ml
    
    FV_tree.ml
    
    FeatureVector.ml
    
    Fingerprint.ml
    
    FixpointUnif.ml
    
    Flex_state.ml
    
    HO_unif.ml
    
    HVar.ml
    
    Hash.ml
    
    Hashcons.ml
    
    IArray.ml
    
    ID.ml
    
    Ind_ty.ml
    
    Index.ml
    
    Index_intf.ml
    
    InnerTerm.ml
    
    Input_format.ml
    
    Int_lit.ml
    
    Interfaces.ml
    
    JPFull.ml
    
    JP_unif.ml
    
    Lambda.ml
    
    LazyList.ml
    
    Literal.ml
    
    Literals.ml
    
    Monome.ml
    
    Multiset.ml
    
    Multiset_intf.ml
    
    Multisets.ml
    
    NPDtree.ml
    
    Options.ml
    
    Ordering.ml
    
    Ordinal.ml
    
    Output_format.ml
    
    PUnif.ml
    
    ParseLocation.ml
    
    PatternUnif.ml
    
    Position.ml
    
    PragUnifParams.ml
    
    Precedence.ml
    
    Proof.ml
    
    Rat_lit.ml
    
    Rewrite.ml
    
    SLiteral.ml
    
    STerm.ml
    
    Scoped.ml
    
    Signature.ml
    
    Skolem.ml
    
    SolidSubsumption.ml
    
    SolidUnif.ml
    
    Statement.ml
    
    Subst.ml
    
    Term.ml
    
    Test_prop.ml
    
    Type.ml
    
    TypeInference.ml
    
    TypedSTerm.ml
    
    Unif.ml
    
    UnifFramework.ml
    
    Unif_constr.ml
    
    Unif_intf.ml
    
    Unif_subst.ml
    
    UnionFind.ml
    
    UntypedAST.ml
    
    Util.ml
    
    Var.ml
    
    logtk.ml
    
    signal.ml
  - logtk.parsers
    
    Ast_dk.ml
    
    Lex_dk.ml
    
    Lex_tptp.ml
    
    Lex_zf.ml
    
    Parse_dk.ml
    
    Parse_tptp.ml
    
    Parse_zf.ml
    
    Tip_ast.ml
    
    Tip_lexer.ml
    
    Tip_parser.ml
    
    Util_dk.ml
    
    ast_tptp.ml
    
    callProver.ml
    
    logtk_parsers.ml
    
    parsing_utils.ml
    
    trace_tstp.ml
    
    util_tip.ml
    
    util_tptp.ml
    
    util_zf.ml
  - logtk.proofs
    
    LLProof.ml
    
    LLProof_check.ml
    
    LLProof_conv.ml
    
    LLProver.ml
    
    LLTerm.ml
    
    logtk_proofs.ml
  - logtk.solving
    
    logtk_solving.ml
    
    lpo.ml

Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module `Unif_constr.FO`Source

Sourceval make : tags:Proof.tag list -> Term.t Scoped.t -> Term.t Scoped.t -> t

package logtk

Module Unif_constr.FOSource

Module `Unif_constr.FO`Source