package logtk

  1. Overview
  2. Docs
Core types and algorithms for logic

Install 

dune-project
 Dependency

github.com Readme Changelog Edit opam file Versions (4)

Authors

  1. S
    Simon Cruanes
  2. P
    Petar Vukmirovic
  3. A
    Alexander Bentkamp
  4. S
    Sophie Tourret
  5. V
    Visa Nummelin

Maintainers

  1. S
    simon.cruanes.2007@m4x.org

Sources

2.0.tar.gz
md5=7a8e57388083ed763d12d18324c8a086
sha512=5c5ac312ada6b42907d1e91e349454a8375f7bf8165d3459721a40b707a840a3d6b3dc968a66f1040cb4de7aedf5c1c13f3e90b51337eae5ea6de41651d7bd63

doc/logtk.parsers/Logtk_parsers/Trace_tstp/index.html

Module Logtk_parsers.Trace_tstp

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.

val force : t -> unit

Force the lazy proof step, if any

Proof traversal

module StepTbl : 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_iter : 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