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.