package logtk
Core types and algorithms for logic
Install
Dune Dependency
Authors
Maintainers
Sources
1.6.tar.gz
md5=97cdb2f90468e9e27c7bbe3b4fb160bb
sha512=fee73369f673a91dfa9e265fc69be08b32235e10a495f3af6477d404fcd01e3452a0d012b150f3d7f97c00af2f6045019ad039164bf698f70d771231cc4efe5d
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