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

All Superinterfaces:

Reason

All Known Implementing Classes:

ExistentialVo

public interface Existential
extends Reason

Rule of existential generalization.

            A(x) -> B
  -----------------------
   exists x A(x) -> B
 

Author:

Michael Meyling

Method Summary

Existential	getExistential() Get this reason.
java.lang.String	getReference() Get reference to formula.
Element	getSubjectVariable() Get free subject variable we want to quantify over.

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

getName, getReferences

Method Detail

getExistential

Existential getExistential()

Get this reason.

Returns:

This reason.

getReference

java.lang.String getReference()

Get reference to formula. Usually this a formula of type A(x) -> B

Returns:

Reference to previously proved formula.

getSubjectVariable

Element getSubjectVariable()

Get free subject variable we want to quantify over.

Returns:

Free subject variable.