org.qedeq.kernel.se.dto.module
Class ConditionalProofVo

java.lang.Object
  org.qedeq.kernel.se.dto.module.ConditionalProofVo

All Implemented Interfaces:

ConditionalProof, FormalProofLine, Reason

public class ConditionalProofVo
extends java.lang.Object
implements ConditionalProof

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.

Author:

Michael Meyling

Constructor Summary

ConditionalProofVo()
Default constructor.

ConditionalProofVo(Hypothesis hypothesis, FormalProofLineList proofLines, Conclusion conclusion)
Constructs an reason.

Method Summary

boolean	equals(java.lang.Object obj)
Conclusion	getConclusion() Get conclusion.
ConditionalProof	getConditionalProof() Get this reason.
FormalProofLineList	getFormalProofLineList() Get proof that can use the hypothesis.
Formula	getFormula() Get formula for this line.
Hypothesis	getHypothesis() Get hypothesis.
java.lang.String	getLabel() Get label for this proof line.
java.lang.String	getName() Get name for this reason.
Reason	getReason() Get reason for deriving this line.
java.lang.String[]	getReferences() Get references to previous formulas.
int	hashCode()
void	setConclusion(Conclusion conclusion) Set conclusion.
void	setFormalProofLineList(FormalProofLineList list) Set formal proof lines.
void	setHypothesis(Hypothesis hypothesis) Set hypothesis.
java.lang.String	toString()

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Constructor Detail

ConditionalProofVo

public ConditionalProofVo(Hypothesis hypothesis,
                          FormalProofLineList proofLines,
                          Conclusion conclusion)

Constructs an reason.

Parameters:

hypothesis - Free subject variable that will be replaced.

proofLines - Bound subject variable that will be substituted.

conclusion - Conclusion.

ConditionalProofVo

public ConditionalProofVo()

Default constructor.

Method Detail

getConditionalProof

public ConditionalProof getConditionalProof()

Description copied from interface: ConditionalProof

Get this reason.

Specified by:

getConditionalProof in interface ConditionalProof

Returns:

This reason.

getHypothesis

public Hypothesis getHypothesis()

Description copied from interface: ConditionalProof

Get hypothesis.

Specified by:

getHypothesis in interface ConditionalProof

Returns:

Hypothesis.

setHypothesis

public void setHypothesis(Hypothesis hypothesis)

Set hypothesis.

Parameters:

hypothesis - Reference to formula.

getReferences

public java.lang.String[] getReferences()

Description copied from interface: Reason

Get references to previous formulas.

Specified by:

getReferences in interface Reason

Returns:

List of references. Contains no entries with value null.

setFormalProofLineList

public void setFormalProofLineList(FormalProofLineList list)

Set formal proof lines.

Parameters:

list - Proof lines that might use hypothesis.

getFormalProofLineList

public FormalProofLineList getFormalProofLineList()

Description copied from interface: ConditionalProof

Get proof that can use the hypothesis.

Specified by:

getFormalProofLineList in interface ConditionalProof

Returns:

Conditional proof.

getConclusion

public Conclusion getConclusion()

Description copied from interface: ConditionalProof

Get conclusion. This is a newly proven formula.

Specified by:

getConclusion in interface ConditionalProof

Returns:

Reference to proved formula.

setConclusion

public void setConclusion(Conclusion conclusion)

Set conclusion.

Parameters:

conclusion - New derived formula.

getFormula

public Formula getFormula()

Description copied from interface: FormalProofLine

Get formula for this line.

Specified by:

getFormula in interface FormalProofLine

Returns:

Formula.

getLabel

public java.lang.String getLabel()

Description copied from interface: FormalProofLine

Get label for this proof line. Used for back references.

Specified by:

getLabel in interface FormalProofLine

Returns:

Label.

getName

public java.lang.String getName()

Description copied from interface: Reason

Get name for this reason.

Specified by:

getName in interface Reason

Returns:

Name.

getReason

public Reason getReason()

Description copied from interface: FormalProofLine

Get reason for deriving this line.

Specified by:

getReason in interface FormalProofLine

Returns:

Reason.

equals

public boolean equals(java.lang.Object obj)

Overrides:

equals in class java.lang.Object

hashCode

public int hashCode()

Overrides:

hashCode in class java.lang.Object

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object