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

All Superinterfaces:

Reason

All Known Implementing Classes:

SubstFreeVo

public interface SubstFree
extends Reason

Usage of substitute free subject variable by term.

   A(x)
  ---------------
   A(t)
 

Author:

Michael Meyling

Method Summary

java.lang.String	getReference() Get reference to already proven formula.
Element	getSubjectVariable() Get free subject variable that should be replaced.
SubstFree	getSubstFree() Get this reason.
Element	getSubstituteTerm() Get replacement term.

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

getName, getReferences

Method Detail

getSubstFree

SubstFree getSubstFree()

Get this reason.

Returns:

This reason.

getReference

java.lang.String getReference()

Get reference to already proven formula.

Returns:

Reference to previously proved formula.

getSubjectVariable

Element getSubjectVariable()

Get free subject variable that should be replaced.

Returns:

Subject variable.

getSubstituteTerm

Element getSubstituteTerm()

Get replacement term.

Returns:

Replacement term.