package logtk

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

Module Logtk_parsers.CallProverSource

Call external provers with TSTP (Old)

This module is intended to provide a uniform interface to invoke some classic first-order provers (E, SPASS, …) on a problem specified as a TPTP Ast.

The point is that this AST might be generated programmatically, or manipulated from an existing TSTP proof (for checking purpose), rather than being handled as text.

Sourcetype 'a or_error = ('a, string) CCResult.t
Sourcetype untyped = Logtk.STerm.t
Sourcemodule A = Ast_tptp

Description of provers

Sourcemodule Prover : sig ... end
Sourceval name : Prover.t -> string

Name of the prover

Run provers

Sourcetype result =
  1. | Unsat
  2. | Sat
  3. | Unknown
  4. | Error of string
Sourceval call : ?timeout:int -> ?args:string list -> prover:Prover.t -> untyped A.t list -> result or_error

Call the prover (if present) on the given problem, and return a result. Default timeout is 30.

Sourceval call_proof : ?timeout:int -> ?args:string list -> prover:Prover.t -> untyped A.t list -> (result * Trace_tstp.t) or_error

Call the prover, and also tries to parse a TSTP derivation, if the prover succeeded

Sourceval call_with_out : ?timeout:int -> ?args:string list -> prover:Prover.t -> untyped A.t list -> (result * string) or_error

Same as call, but also returns the raw output of the prover

E-prover specific functions

Sourcemodule Eprover : sig ... end
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