Copyright  (c) Evgenii Kotelnikov 20192021 

License  GPL3 
Maintainer  evgeny.kotelnikov@gmail.com 
Stability  experimental 
Safe Haskell  None 
Language  Haskell2010 
Interface to automated theorem provers.
Synopsis
 data ProvingOptions = ProvingOptions {
 prover :: Prover
 timeLimit :: TimeLimit
 memoryLimit :: MemoryLimit
 debug :: Bool
 defaultOptions :: ProvingOptions
 refute :: Clauses > IO (Partial Solution)
 refuteUsing :: Prover > Clauses > IO (Partial Solution)
 refuteWith :: ProvingOptions > Clauses > IO (Partial Solution)
 prove :: Theorem > IO (Partial Solution)
 proveUsing :: Prover > Theorem > IO (Partial Solution)
 proveWith :: ProvingOptions > Theorem > IO (Partial Solution)
Documentation
data ProvingOptions Source #
The options that describe what theorem prover to use for a problem and how to run it.
ProvingOptions  

Instances
Eq ProvingOptions Source #  
Defined in ATP.Prove (==) :: ProvingOptions > ProvingOptions > Bool # (/=) :: ProvingOptions > ProvingOptions > Bool #  
Ord ProvingOptions Source #  
Defined in ATP.Prove 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 #  
Defined in ATP.Prove showsPrec :: Int > ProvingOptions > ShowS # show :: ProvingOptions > String # showList :: [ProvingOptions] > ShowS # 
refute :: Clauses > IO (Partial Solution) Source #
Attempt to refute a set of clauses using defaultProver
.
refute = refuteWith defaultOptions
refuteUsing :: Prover > Clauses > IO (Partial Solution) Source #
Attempt to refute a set of clauses using a given prover.
refuteWith :: ProvingOptions > Clauses > IO (Partial Solution) Source #
Attempt to refute a set of clauses with a given set of options.
prove :: Theorem > IO (Partial Solution) Source #
Attempt to prove a theorem using defaultProver
.
prove = proveWith defaultOptions