tamarin-prover-theory-0.8.6.0: Term manipulation library for the tamarin prover.

PortabilityGHC only
MaintainerSimon Meier <iridcode@gmail.com>
Safe HaskellNone

Theory.Constraint.Solver.Contradictions

Contents

Description

This is the public interface for constructing and deconstructing constraint systems. The interface for performing constraint solving provided by Theory.Constraint.Solver.

Synopsis

Contradictory constraint systems

data Contradiction Source

Reasons why a constraint System can be contradictory.

Constructors

Cyclic

The paths are cyclic.

NonNormalTerms

Has terms that are not in normal form. | NonLastNode -- ^ Has a non-silent node after the last node.

ForbiddenExp

Forbidden Exp-down rule instance

ForbiddenBP

Forbidden bilinear pairing rule instance

ForbiddenKD

has forbidden KD-fact

ImpossibleChain

has impossible chain

NonInjectiveFactInstance (NodeId, NodeId, NodeId)

Contradicts that certain facts have unique instances.

IncompatibleEqs

Incompatible equalities.

FormulasFalse

False in formulas

SuperfluousLearn LNTerm NodeId

A term is derived both before and after a learn

NodeAfterLast (NodeId, NodeId)

There is a node after the last node.

contradictions :: ProofContext -> System -> [Contradiction]Source

All CR-rules reducing a constraint system to *⟂* represented as a list of trivial contradictions. Note that some constraint systems are also removed because they have no unifier. This is part of unification. Note also that *S_{¬@}* is handled as part of *S_∀*.

contradictorySystem :: ProofContext -> System -> BoolSource

True if the constraint system is contradictory.

Pretty-printing