ATP.Prover

Description

Models of automated theorem provers.

Synopsis

Documentation

The implementation of a theorem prover, supported by atp.

Constructors

E
Vampire

Instances details

Bounded Vendor Source #
Instance details Defined in ATP.Prover Methods minBound :: Vendor # maxBound :: Vendor #
Enum Vendor Source #
Instance details Defined in ATP.Prover Methods succ :: Vendor -> Vendor # pred :: Vendor -> Vendor # toEnum :: Int -> Vendor # fromEnum :: Vendor -> Int # enumFrom :: Vendor -> [Vendor] # enumFromThen :: Vendor -> Vendor -> [Vendor] # enumFromTo :: Vendor -> Vendor -> [Vendor] # enumFromThenTo :: Vendor -> Vendor -> Vendor -> [Vendor] #
Eq Vendor Source #
Instance details Defined in ATP.Prover Methods (==) :: Vendor -> Vendor -> Bool # (/=) :: Vendor -> Vendor -> Bool #
Ord Vendor Source #
Instance details Defined in ATP.Prover Methods compare :: Vendor -> Vendor -> Ordering # (<) :: Vendor -> Vendor -> Bool # (<=) :: Vendor -> Vendor -> Bool # (>) :: Vendor -> Vendor -> Bool # (>=) :: Vendor -> Vendor -> Bool # max :: Vendor -> Vendor -> Vendor # min :: Vendor -> Vendor -> Vendor #
Show Vendor Source #
Instance details Defined in ATP.Prover Methods showsPrec :: Int -> Vendor -> ShowS # show :: Vendor -> String # showList :: [Vendor] -> ShowS #

The automated theorem prover.

Constructors

Prover
Fields vendor :: Vendor executable :: FilePath

Instances details

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

The time limit allocated to the prover, in seconds.

The memory limit allocated to the prover, in Mb.

Build the list of command line arguments for the given prover.

Arguments

Interpret the output of the theorem prover from its exit code and the contents of the returned stdout and stderr.

The Vampire theorem prover.

The E theorem prover.

The default prover used by refute and prove.

>>> defaultProver
Prover {vendor = E, executable = "eprover"}