ATP.Prove

Interface to automated theorem provers.

Documentation

data ProvingOptions

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

Eq ProvingOptions

Defined in ATP.Prove

Methods

(==) :: ProvingOptions -> ProvingOptions -> Bool

(/=) :: ProvingOptions -> ProvingOptions -> Bool

Ord ProvingOptions

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

Defined in ATP.Prove

Methods

showsPrec :: Int -> ProvingOptions -> ShowS

show :: ProvingOptions -> String

showList :: [ProvingOptions] -> ShowS

defaultOptions :: ProvingOptions

The default options used by refute and prove.

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

refute :: Clauses -> IO (Partial Solution)

Attempt to refute a set of clauses using defaultProver.

refute = refuteWith defaultOptions

refuteUsing :: Prover -> Clauses -> IO (Partial Solution)

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

refuteWith :: ProvingOptions -> Clauses -> IO (Partial Solution)

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

prove :: Theorem -> IO (Partial Solution)

Attempt to prove a theorem using defaultProver.

prove = proveWith defaultOptions

proveUsing :: Prover -> Theorem -> IO (Partial Solution)

Attempt to prove a theorem using a given prover.

proveWith :: ProvingOptions -> Theorem -> IO (Partial Solution)

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