Copilot.Theorem.Prove

Connection to theorem provers.

Documentation

data Output

Output produced by a prover, containing the Status of the proof and additional information.

Constructors

Output Status [String]

data Status

Status returned by a prover when given a specification and a property to prove.

Constructors

Sat

Valid

Invalid

Unknown

Error

data Prover

A connection to a prover able to check the satisfiability of specifications.

The most important is askProver, which takes 3 arguments :

• The prover descriptor
• A list of properties names which are assumptions
• A properties that have to be deduced from these assumptions

Constructors

forall r. Prover

Fields

• proverName :: String
• startProver :: Spec -> IO r
• askProver :: r -> [PropId] -> [PropId] -> IO Output
• closeProver :: r -> IO ()

type PropId = String

A unique property identifier

data PropRef a where

Reference to a property.

Constructors

PropRef :: PropId -> PropRef a

type Proof a = ProofScheme a ()

A proof scheme with unit result.

type UProof = Writer [Action] ()

A sequence of computations that generate a trace of required prover Actions.

data ProofScheme a b where

A proof scheme is a sequence of computations that compute a result and generate a trace of required prover Actions.

Constructors

Proof :: Writer [Action] b -> ProofScheme a b

Instances

Applicative (ProofScheme a)

Defined in Copilot.Theorem.Prove

Methods

pure :: a0 -> ProofScheme a a0

(<*>) :: ProofScheme a (a0 -> b) -> ProofScheme a a0 -> ProofScheme a b

liftA2 :: (a0 -> b -> c) -> ProofScheme a a0 -> ProofScheme a b -> ProofScheme a c

(*>) :: ProofScheme a a0 -> ProofScheme a b -> ProofScheme a b

(<*) :: ProofScheme a a0 -> ProofScheme a b -> ProofScheme a a0

Functor (ProofScheme a)

Defined in Copilot.Theorem.Prove

Methods

fmap :: (a0 -> b) -> ProofScheme a a0 -> ProofScheme a b

(<$) :: a0 -> ProofScheme a b -> ProofScheme a a0

Monad (ProofScheme a)

Defined in Copilot.Theorem.Prove

Methods

(>>=) :: ProofScheme a a0 -> (a0 -> ProofScheme a b) -> ProofScheme a b

(>>) :: ProofScheme a a0 -> ProofScheme a b -> ProofScheme a b

return :: a0 -> ProofScheme a a0

data Action where

Prover actions.

Constructors

Check :: Prover -> Action

Assume :: PropId -> Action

Admit :: Action

data Universal

Empty datatype to mark proofs of universally quantified predicates.

data Existential

Empty datatype to mark proofs of existentially quantified predicates.

check :: Prover -> Proof a

Record a requirement for satisfiability checking.

prove :: Spec -> PropId -> UProof -> IO Bool

Try to prove a property in a specification with a given proof scheme.

Return True if a proof of satisfiability or validity is found, false otherwise.

combine :: Prover -> Prover -> Prover

Combine two provers producing a new prover that will run both provers in parallel and combine their outputs.

The results produced by the provers must be consistent. For example, if one of the provers indicates that a property is Valid while another indicates that it is Invalid, the combination of both provers will return an Error.