package logtk

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

Module Logtk_parsers.Trace_tstpSource

Trace of a TSTP prover

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

    Equisatisfiable step?

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

Obtain the ID of the proof step.

Sourceval force : t -> unit

Force the lazy proof step, if any

Proof traversal

Sourcemodule StepTbl : Hashtbl.S with type key = t
Sourcetype proof_set = unit StepTbl.t
Sourceval is_dag : t -> bool

Is the proof a proper DAG?

Sourceval 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.

Sourceval to_seq : t -> t Iter.t

Traversal of parent proofs

Sourceval depth : t -> int

Max depth of the proof

Sourceval size : t -> int

Number of nodes in the proof

IO

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

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

Sourceval 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
Sourceval to_string : t -> string

Print proof step, and its parents

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