package logtk

  1. Overview
  2. Docs
package logtk
Legend:
Library
Module
Module type
Parameter
Class
Class type

Statement

The input problem is made of statements. Each statement can declare a type, assert a formula, or a conjecture, define a term, add a rewrite rule, etc.

Those statements do not necessarily reflect exactly statements in the input language(s) (e.g., TPTP).

type 'ty data = {
  1. data_id : ID.t;
    (*

    Name of the type

    *)
  2. data_args : 'ty Var.t list;
    (*

    type parameters

    *)
  3. data_ty : 'ty;
    (*

    type of Id, that is, type -> type -> ... -> type

    *)
  4. data_cstors : (ID.t * 'ty * ('ty * (ID.t * 'ty)) list) list;
    (*

    Each constructor is id, ty, args. ty must be of the form ty1 -> ty2 -> ... -> id args. args has the form (ty1, p1), (ty2,p2), … where each p is a projector.

    *)
}

A datatype declaration

type attr =
  1. | A_AC
  2. | A_infix of string
  3. | A_prefix of string
  4. | A_sos
    (*

    set of support

    *)
type attrs = attr list
type 'ty skolem = ID.t * 'ty
type polarity = [
  1. | `Equiv
  2. | `Imply
]

polarity for rewrite rules

type ('f, 't, 'ty) def_rule =
  1. | Def_term of {
    1. vars : 'ty Var.t list;
    2. id : ID.t;
    3. ty : 'ty;
    4. args : 't list;
    5. rhs : 't;
    6. as_form : 'f;
    }
    (*

    forall vars, id args = rhs

    *)
  2. | Def_form of {
    1. vars : 'ty Var.t list;
    2. lhs : 't SLiteral.t;
    3. rhs : 'f list;
    4. polarity : polarity;
    5. as_form : 'f list;
    }
    (*

    forall vars, lhs op bigand rhs where op depends on polarity (in {=>, <=>, <=})

    *)
type ('f, 't, 'ty) def = {
  1. def_id : ID.t;
  2. def_ty : 'ty;
  3. def_rules : ('f, 't, 'ty) def_rule list;
  4. def_rewrite : bool;
}
type ('f, 't, 'ty) view =
  1. | TyDecl of ID.t * 'ty
    (*

    id: ty

    *)
  2. | Data of 'ty data list
  3. | Def of ('f, 't, 'ty) def list
  4. | Rewrite of ('f, 't, 'ty) def_rule
  5. | Assert of 'f
    (*

    assert form

    *)
  6. | Lemma of 'f list
    (*

    lemma to prove and use, using Avatar cut

    *)
  7. | Goal of 'f
    (*

    goal to prove

    *)
  8. | NegatedGoal of 'ty skolem list * 'f list
    (*

    goal after negation, with skolems

    *)
type lit = Term.t SLiteral.t
type formula = TypedSTerm.t
type clause = lit list
type ('f, 't, 'ty) t = private {
  1. id : int;
  2. view : ('f, 't, 'ty) view;
  3. attrs : attrs;
  4. proof : proof;
  5. mutable name : string option;
}
and proof = Proof.Step.t
and clause_t = (clause, Term.t, Type.t) t
val compare : (_, _, _) t -> (_, _, _) t -> int
val view : ('f, 't, 'ty) t -> ('f, 't, 'ty) view
val attrs : (_, _, _) t -> attrs
val proof_step : (_, _, _) t -> proof
val name : (_, _, _) t -> string

Retrieve a name from the proof, or generate+save a new one

val as_proof_i : input_t -> Proof.t
val res_tc_i : input_t Proof.result_tc
val as_proof_c : clause_t -> Proof.t
val res_tc_c : clause_t Proof.result_tc
val mk_data : ID.t -> args:'ty Var.t list -> 'ty -> (ID.t * 'ty * ('ty * (ID.t * 'ty)) list) list -> 'ty data
val mk_def : ?rewrite:bool -> ID.t -> 'ty -> ('f, 't, 'ty) def_rule list -> ('f, 't, 'ty) def
val attrs_ua : (_, _, _) t -> UntypedAST.attrs

All attributes, included these in the proof

val ty_decl : ?attrs:attrs -> proof:proof -> ID.t -> 'ty -> (_, _, 'ty) t
val def : ?attrs:attrs -> proof:proof -> ('f, 't, 'ty) def list -> ('f, 't, 'ty) t
val rewrite : ?attrs:attrs -> proof:proof -> ('f, 't, 'ty) def_rule -> ('f, 't, 'ty) t
val data : ?attrs:attrs -> proof:proof -> 'ty data list -> (_, _, 'ty) t
val assert_ : ?attrs:attrs -> proof:proof -> 'f -> ('f, _, _) t
val lemma : ?attrs:attrs -> proof:proof -> 'f list -> ('f, _, _) t
val goal : ?attrs:attrs -> proof:proof -> 'f -> ('f, _, _) t
val neg_goal : ?attrs:attrs -> proof:proof -> skolems:'ty skolem list -> 'f list -> ('f, _, 'ty) t
val signature : ?init:Signature.t -> ?conj_syms:ID.t Iter.t -> (_, _, Type.t) t Iter.t -> Signature.t

Compute signature when the types are using Type

val conv_attrs : UntypedAST.attrs -> attrs
val attr_to_ua : attr -> UntypedAST.attr
val map_data : ty:('ty1 -> 'ty2) -> 'ty1 data -> 'ty2 data
val map_def : form:('f1 -> 'f2) -> term:('t1 -> 't2) -> ty:('ty1 -> 'ty2) -> ('f1, 't1, 'ty1) def -> ('f2, 't2, 'ty2) def
val map_def_rule : form:('a -> 'b) -> term:('c -> 'd) -> ty:('e -> 'f) -> ('a, 'c, 'e) def_rule -> ('b, 'd, 'f) def_rule
val map : form:('f1 -> 'f2) -> term:('t1 -> 't2) -> ty:('ty1 -> 'ty2) -> ('f1, 't1, 'ty1) t -> ('f2, 't2, 'ty2) t

Defined Constants

type definition = Rewrite.rule_set
val as_defined_cst : ID.t -> (int * definition) option

as_defined_cst id returns Some level if id is a constant defined at stratification level level, None otherwise

val as_defined_cst_level : ID.t -> int option
val is_defined_cst : ID.t -> bool
val declare_defined_cst : ID.t -> level:int -> definition -> unit

declare_defined_cst id ~level states that id is a defined constant of given level. It means that it is defined based only on constants of strictly lower levels

val scan_stmt_for_defined_cst : clause_t -> unit

Try and declare defined constants in the given statement

val scan_tst_rewrite : input_t -> unit

Inductive Types

val scan_stmt_for_ind_ty : clause_t -> unit

scan_stmt_for_ind_ty stmt examines stmt, and, if the statement is a declaration of inductive types or constants, it declares them using declare_ty or declare_inductive_constant.

val scan_simple_stmt_for_ind_ty : input_t -> unit

Same as scan_stmt but on earlier statements

val get_rw_rule : ?weight_incr:int -> clause_t -> (ID.Set.elt * Rewrite.rule) option
val get_formulas_from_defs : ('a, _, _) t -> 'a CCList.t
val eliminate_long_implications : ?is_goal:bool -> TypedSTerm.Form.t -> TypedSTerm.Form.t
val sine_axiom_selector : ?ignore_k_most_common_symbols:int option -> ?take_conj_defs:bool -> ?take_only_defs:bool -> ?trim_implications:bool -> ?depth_start:int -> ?depth_end:int -> ?tolerance:float -> input_t Iter.t -> input_t Iter.t

Implementation of SinE algorithm with the usual parameters described in Hoder and Voronkov Sine Qua Non paper

Iterators

module Seq : sig ... end

IO

val pp_def_rule : 'a CCFormat.printer -> 'b CCFormat.printer -> 'c CCFormat.printer -> ('a, 'b, 'c) def_rule CCFormat.printer
val pp_def : 'a CCFormat.printer -> 'b CCFormat.printer -> 'c CCFormat.printer -> ('a, 'b, 'c) def CCFormat.printer
val pp : 'a CCFormat.printer -> 'b CCFormat.printer -> 'c CCFormat.printer -> ('a, 'b, 'c) t CCFormat.printer
val to_string : 'a CCFormat.printer -> 'b CCFormat.printer -> 'c CCFormat.printer -> ('a, 'b, 'c) t -> string
val pp_clause : clause_t CCFormat.printer
val pp_input : input_t CCFormat.printer
module ZF : sig ... end
module TPTP : sig ... end
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct