package logtk
Core types and algorithms for logic
Install
Dune Dependency
Authors
Maintainers
Sources
1.5.1.tar.gz
md5=cc320f66f10555c54822da624419e003
sha512=f8d5f7a5ae790bf0388d74261673803cf375f91f92f7b413b70db1ce5841ef55343a208f98727c8551d66f1840ab892f1c0c943a34861d14d79ce469b235a2f2
doc/logtk.parsers/Logtk_parsers/CallProver/index.html
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.
Description of provers
Run provers
Source
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.
Source
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
Source
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