ATP.Prove

Description

Interface to automated theorem provers.

Synopsis

Documentation

The options that describe what theorem prover to use for a problem and how to run it.

Constructors

ProvingOptions
Fields prover :: Prover timeLimit :: TimeLimit memoryLimit :: MemoryLimit debug :: Bool If `True`, print the input, the cli command, the exit code and the output of the prover

Instances details

Eq ProvingOptions Source #
Instance details Defined in ATP.Prove Methods (==) :: ProvingOptions -> ProvingOptions -> Bool # (/=) :: ProvingOptions -> ProvingOptions -> Bool #
Ord ProvingOptions Source #
Instance details Defined in ATP.Prove Methods compare :: ProvingOptions -> ProvingOptions -> Ordering # (<) :: ProvingOptions -> ProvingOptions -> Bool # (<=) :: ProvingOptions -> ProvingOptions -> Bool # (>) :: ProvingOptions -> ProvingOptions -> Bool # (>=) :: ProvingOptions -> ProvingOptions -> Bool # max :: ProvingOptions -> ProvingOptions -> ProvingOptions # min :: ProvingOptions -> ProvingOptions -> ProvingOptions #
Show ProvingOptions Source #
Instance details Defined in ATP.Prove Methods showsPrec :: Int -> ProvingOptions -> ShowS # show :: ProvingOptions -> String # showList :: [ProvingOptions] -> ShowS #

The default options used by refute and prove.

>>> defaultOptions
ProvingOptions {prover = Prover {vendor = E, executable = "eprover"}, timeLimit = 300, memoryLimit = 2000, debug = False}

Attempt to refute a set of clauses using defaultProver.

refute = refuteWith defaultOptions

Attempt to refute a set of clauses using a given prover.

Attempt to refute a set of clauses with a given set of options.

Attempt to prove a theorem using defaultProver.

prove = proveWith defaultOptions

Attempt to prove a theorem using a given prover.

Attempt to prove a theorem with a given set of options.