org.qedeq.kernel.se.base.module
Interface ConditionalProof

All Superinterfaces:

FormalProofLine, Reason

All Known Implementing Classes:

ConditionalProofVo

public interface ConditionalProof
extends Reason, FormalProofLine

Usage of conditional proof method. If you can derive the proposition A out of the assumed formulas then the following formula is true: conjunction of the assumed formulas implies A

      H    hypothesis
     -------------------
      A
  ---------------
   H -> A
 

Author:

Michael Meyling

Method Summary

Conclusion	getConclusion() Get conclusion.
ConditionalProof	getConditionalProof() Get this reason.
FormalProofLineList	getFormalProofLineList() Get proof that can use the hypothesis.
Hypothesis	getHypothesis() Get hypothesis.

Methods inherited from interface org.qedeq.kernel.se.base.module.Reason

getName, getReferences

Methods inherited from interface org.qedeq.kernel.se.base.module.FormalProofLine

getFormula, getLabel, getReason

Method Detail

getConditionalProof

ConditionalProof getConditionalProof()

Get this reason.

Returns:

This reason.

getHypothesis

Hypothesis getHypothesis()

Get hypothesis.

Returns:

Hypothesis.

getFormalProofLineList

FormalProofLineList getFormalProofLineList()

Get proof that can use the hypothesis.

Returns:

Conditional proof.

getConclusion

Conclusion getConclusion()

Get conclusion. This is a newly proven formula.

Returns:

Reference to proved formula.