package logtk
Core types and algorithms for logic
Install
Dune Dependency
Authors
Maintainers
Sources
2.1.tar.gz
md5=e72de75e9f0f87da9e6e8c0a4d4c89f9
sha512=81becfc9badd686ab3692cd9312172aa4c4e3581b110e81770bb01e0ffbc1eb8495d0dd6d43b98f3d06e6b8c8a338174c13ebafb4e9849a3ddf89f9a3a72c287
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
val is_axiom : t -> bool
val is_theory : t -> bool
val is_step : t -> bool
val is_proof_of_false : t -> bool
val force : t -> unit
Force the lazy proof step, if any
Proof traversal
type proof_set = unit StepTbl.t
val is_dag : t -> bool
Is the proof a proper DAG?
Traverse the proof. Each proof node is traversed only once, using the set to recognize already traversed 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.
Debug printing, non recursive
include Logtk.Interfaces.PRINT with type t := t
val pp : t CCFormat.printer
val to_string : t -> string
val pp1 : t CCFormat.printer
Print proof step, and its parents
val pp_tstp : t CCFormat.printer
print the whole proofs
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page