package logtk
Core types and algorithms for logic
Install
Dune Dependency
Authors
Maintainers
Sources
2.1.tar.gz
md5=e72de75e9f0f87da9e6e8c0a4d4c89f9
sha512=81becfc9badd686ab3692cd9312172aa4c4e3581b110e81770bb01e0ffbc1eb8495d0dd6d43b98f3d06e6b8c8a338174c13ebafb4e9849a3ddf89f9a3a72c287
doc/logtk.parsers/Logtk_parsers/CallProver/index.html
Module Logtk_parsers.CallProver
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.
type 'a or_error = ('a, string) CCResult.t
type untyped = Logtk.STerm.t
module A = Ast_tptp
Description of provers
module Prover : sig ... end
val name : Prover.t -> string
Name of the prover
Run provers
val 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.
val 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
val 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
module Eprover : sig ... end
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page