Constructor and Description |
---|
Validator(Trace trace,
_Prover prover,
_TraceManager traceManager) |
Modifier and Type | Method and Description |
---|---|
ProverName |
getProverName()
Returns an object describing the detailed name of the prover.
|
_Strategy |
getStrategy()
Returns the strategy used by this prover.
|
ProvabilityStatus |
statusFor(ProofSearchResult result)
Returns the provability status corresponding to the specified proof-search
result.
|
public Validator(Trace trace, _Prover prover, _TraceManager traceManager)
public ProverName getProverName()
_Prover
getProverName
in interface _Prover
public _Strategy getStrategy()
_Prover
getStrategy
in interface _Prover
public ProvabilityStatus statusFor(ProofSearchResult result)
_Prover
ProofSearchResult.SUCCESS
) corresponds to a provable problem
(status ProvabilityStatus.PROVABLE
), while a failed proof-search
(result ProofSearchResult.FAILURE
) corresponds to an unprovable
problem (status ProvabilityStatus.UNPROVABLE
). On the other hand,
in a calculus for unprovability a successful proof-search corresponds to an
unprovable formula, while a failed proof-search corresponds to a provable
formula (status ProvabilityStatus.PROVABLE
).