Portability | GHC only |
---|---|

Maintainer | Simon Meier <iridcode@gmail.com> |

Safe Haskell | None |

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

- type CaseName = String
- data ProofMethod
- execProofMethod :: ProofContext -> ProofMethod -> System -> Maybe (Map CaseName System)
- data GoalRanking
- goalRankingName :: GoalRanking -> String
- rankProofMethods :: GoalRanking -> ProofContext -> System -> [(ProofMethod, (Map CaseName System, String))]
- data Heuristic
- roundRobinHeuristic :: [GoalRanking] -> Heuristic
- useHeuristic :: Heuristic -> Int -> GoalRanking
- prettyProofMethod :: HighlightDocument d => ProofMethod -> d

# Proof methods

data ProofMethod Source

Sound transformations of sequents.

Sorry (Maybe String) | Proof was not completed |

Solved | An attack was fond |

Simplify | A simplification step. |

SolveGoal Goal | A goal that was solved. |

Contradiction (Maybe Contradiction) | A contradiction could be derived, possibly with a reason. |

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

execProofMethod :: ProofContext -> ProofMethod -> System -> Maybe (Map CaseName System)Source

## Heuristics

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
`ProofMethod`

s 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.