package logtk

  1. Overview
  2. Docs
package logtk
Legend:
Library
Module
Module type
Parameter
Class
Class type
type result = {
  1. answer : szs_answer;
  2. output : string;
  3. decls : untyped A.t Iter.t option;
  4. proof : Trace_tstp.t option;
}
and szs_answer =
  1. | Theorem
  2. | CounterSatisfiable
  3. | Unknown
val string_of_answer : szs_answer -> string
val run_eproof : steps:int -> input:string -> result or_error

Run Eproof_ram, and tries to read a proof back.

val run_eprover : ?opts:string list -> ?level:int -> steps:int -> input:string -> unit -> result or_error

Runs E with the given input (optional verbosity level). The returned result will not contain a proof. opts is an additional list of command line options that will be given to E.

val discover : ?opts:string list -> steps:int -> untyped A.t Iter.t -> untyped A.t Iter.t or_error

explore the surrounding of this list of declarations, returning the TPTP output of E

val cnf : ?opts:string list -> untyped A.t Iter.t -> untyped A.t Iter.t or_error

Use E to convert a set of statements into CNF

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