- data Sequent = Sequent {}
- seProto :: Sequent -> Protocol
- wellTypedCases :: MonadPlus m => Sequent -> m [(String, Sequent)]
- saturate :: MonadPlus m => Sequent -> m Sequent
- frule :: MonadPlus m => Sequent -> Sequent -> m (Mapping, Maybe Sequent)
- fruleInst :: MonadPlus m => Sequent -> Mapping -> Sequent -> m (Maybe Sequent)
- chainRule :: MonadPlus m => Sequent -> Message -> m [((String, [Either TID AgentId]), Sequent)]
- splitEq :: MsgEq -> Sequent -> [Maybe Sequent]
- exploitTyping :: MonadPlus m => Sequent -> m Sequent
- uniqueTIDQuantifiers :: Sequent -> Sequent

# Datatype

A sequent with a conjunction of a set of facts as the premise and a single formula as the conclusion denoting a statement about a reachable state of a protocol.

## Logically safe construction

wellTypedCases :: MonadPlus m => Sequent -> m [(String, Sequent)]Source

The named list of sequents which need to be proven in order to prove that the given protocol is well typed or weakly-atomic

PRE: The conclusion of the sequent must be typing atom.

Uses `fail`

for error reporting.

saturate :: MonadPlus m => Sequent -> m SequentSource

Try to saturate a sequent, if possible and leading to new facts.

:: MonadPlus m | |

=> Sequent | rule |

-> Sequent | proof state |

-> m (Mapping, Maybe Sequent) | some result if resolution worked. Nothing denotes that False was derived. Just means that premises of proof state were extended. mzero if rule could not be applied |

Like `fruleInst`

but tries all mappings.

:: MonadPlus m | |

=> Sequent | rule |

-> Mapping | mapping of free variables of rule to proof state |

-> Sequent | proof state |

-> m (Maybe Sequent) | some result if resolution worked. Nothing denotes that False was derived. Just means that premises of proof state were extended. mzero if rule could not be applied |

Emulate a variant Isabelle's `frule`

tactic. It works only if the given
maping of free variables of the rule makes the premise of the rule provable
under the given proof state. Then, the conclusion of the rule with free
variables mapped accordingly is added to premises of the proof state. The
last step works currently only for conclusions being false of pure
conclusions.

NOTE that `frule`

works only for rules that contain no existential
quantifiers in the conclusion.

chainRule :: MonadPlus m => Sequent -> Message -> m [((String, [Either TID AgentId]), Sequent)]Source

Try to use the chain rule.

MonadPlus is used to report a failure to apply the rule.

splitEq :: MsgEq -> Sequent -> [Maybe Sequent]Source

Split a splittable equality. splitting can be done.

exploitTyping :: MonadPlus m => Sequent -> m SequentSource

Try to exploit the typing. Fails if no new facts could be derived.

uniqueTIDQuantifiers :: Sequent -> SequentSource

Make all thread identifiers occurring in the sequent unique by consistently relabeling the thread identifiers in the conclusion.