Proof State
Implements the proof state.
- exception ProofBuildError
Bases:
Exception
- class ProofState(*, problem, rule_matcher, deductors, rng=None)
Bases:
objectObject representing the proof state.
- match_theorem(rule)
Match a rule to the proof state.
- Return type:
set[Assumption|NumericalCheck|RuleApplication|ARDeduction|CircleMerge|LineMerge|DirectConsequence|Reflexivity]- Returns:
A set of dependencies that would be added to the proof state if the rule was applied.
- apply(justification)
Add the justification to the proof dependency graph.
- Return type:
bool- Returns:
True if the predicate is a new one, false otherwise.
- check(predicate)
Symbolically check if the predicate is currently considered True.
- Return type:
bool
- check_numerical(predicate)
Check if the predicate is numerically sound.
- Return type:
bool
- justify(predicate)
- Return type:
Assumption|NumericalCheck|RuleApplication|ARDeduction|CircleMerge|LineMerge|DirectConsequence|Reflexivity
- check_goals()
Check if the goals are all symbolically checked.
- Return type:
bool