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

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




Proof methods and heuristics: the external small-step interface to the constraint solver.


Proof methods

type CaseName = StringSource

Every case in a proof is uniquely named.

data ProofMethod Source

Sound transformations of sequents.


Sorry (Maybe String)

Proof was not completed


An attack was fond


A simplification step.

SolveGoal Goal

A goal that was solved.

Contradiction (Maybe Contradiction)

A contradiction could be derived, possibly with a reason.


Use inductive strengthening on the single formula constraint in the system.


data GoalRanking Source

The different available functions to rank goals with respect to their order of solving in a constraint system.

goalRankingName :: GoalRanking -> StringSource

The name/explanation of a GoalRanking.

rankProofMethods :: GoalRanking -> ProofContext -> System -> [(ProofMethod, (Map CaseName System, String))]Source

Use a GoalRanking to generate the ranked, list of possible ProofMethods and their corresponding results in this ProofContext and for this System. If the resulting list is empty, then the constraint system is solved.

roundRobinHeuristic :: [GoalRanking] -> HeuristicSource

Smart constructor for heuristics. Schedules the goal rankings in a round-robin fashion dependent on the proof depth.

useHeuristic :: Heuristic -> Int -> GoalRankingSource

Use a heuristic to schedule a GoalRanking according to the given proof-depth.

Pretty Printing

prettyProofMethod :: HighlightDocument d => ProofMethod -> dSource

Pretty-print a proof method.