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.
type 'a or_error = ('a, string) CCResult.ttype untyped = Logtk.STerm.tmodule A = Ast_tptpmodule Prover : sig ... endval name : Prover.t -> stringName of the prover
val call :
?timeout:int ->
?args:string list ->
prover:Prover.t ->
untyped A.t list ->
result or_errorCall the prover (if present) on the given problem, and return a result. Default timeout is 30.
val call_proof :
?timeout:int ->
?args:string list ->
prover:Prover.t ->
untyped A.t list ->
(result * Trace_tstp.t) or_errorCall the prover, and also tries to parse a TSTP derivation, if the prover succeeded
val call_with_out :
?timeout:int ->
?args:string list ->
prover:Prover.t ->
untyped A.t list ->
(result * string) or_errorSame as call, but also returns the raw output of the prover
module Eprover : sig ... end