package logtk

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

Trace of a TSTP prover

type id = Ast_tptp.name
type term = Logtk.STerm.t
type form = Logtk.STerm.t
type clause = term Logtk.SLiteral.t list
type t =
  1. | Axiom of string * string
  2. | Theory of string
  3. | InferForm of form * step lazy_t
  4. | InferClause of clause * step lazy_t
and step = {
  1. id : id;
  2. rule : string;
  3. parents : t array;
  4. esa : bool;
    (*

    Equisatisfiable step?

    *)
}
val equal : t -> t -> bool
val compare : t -> t -> int
val mk_f_axiom : id:id -> form -> file:string -> name:string -> t
val mk_c_axiom : id:id -> clause -> file:string -> name:string -> t
val mk_f_step : ?esa:bool -> id:id -> form -> rule:string -> t list -> t
val mk_c_step : ?esa:bool -> id:id -> clause -> rule:string -> t list -> t
val is_axiom : t -> bool
val is_theory : t -> bool
val is_step : t -> bool
val is_proof_of_false : t -> bool
val get_id : t -> id

Obtain the ID of the proof step.

  • raises Invalid_argument

    if the step is Axiom or Theory

val force : t -> unit

Force the lazy proof step, if any

Proof traversal

module StepTbl : Stdlib.Hashtbl.S with type key = t
type proof_set = unit StepTbl.t
val is_dag : t -> bool

Is the proof a proper DAG?

val traverse : ?traversed:proof_set -> t -> (t -> unit) -> unit

Traverse the proof. Each proof node is traversed only once, using the set to recognize already traversed proofs.

val to_seq : t -> t Iter.t

Traversal of parent proofs

val depth : t -> int

Max depth of the proof

val size : t -> int

Number of nodes in the proof

IO

type 'a or_error = ('a, string) CCResult.t
val of_decls : form Ast_tptp.t Iter.t -> t or_error

Try to extract a proof from a list of TSTP statements.

val parse : ?recursive:bool -> string -> t or_error

Try to parse a proof from a file.

Debug printing, non recursive

include Logtk.Interfaces.PRINT with type t := t
val to_string : t -> string

Print proof step, and its parents

val pp_tstp : t CCFormat.printer

print the whole proofs

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