|Maintainer||Simon Meier <email@example.com>|
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
Sound transformations of sequents.
|Sorry (Maybe String)|
Proof was not completed
An attack was fond
A simplification step.
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.
The different available functions to rank goals with respect to their order of solving in a constraint system.
Smart constructor for heuristics. Schedules the goal rankings in a round-robin fashion dependent on the proof depth.
Use a heuristic to schedule a
GoalRanking according to the given