EGEN : IRULEDEF

EGEN is an intermediate rule definition.
(P1) H !`(LCONTR [[LAMBDA x(A) A(O)] t(A)])
*(P2) H !EXISTS x(A) A(O) EGen: t(A) P1
Restrictions: (IS-VARIABLE x(A))
Transformation: (P2 ss) ==> (P1 ss)

TPS documentation homepage


EGEN : MEXPR

EGEN is a top-level command.
Rule of Existential Generalization.
The command format for EGEN is:

 <n>EGEN   P2   P1    t    A      x   LCONTR   P2-HYPS    P1-HYPS 
"LINE" "LINE" "GWFF" "GWFF" "GWFF" "GWFF" "LINELIST" "LINELIST"


The arguments have the following meaning:
P2 : Existentially Quantified Line
P1 : Line to be Existentially Generalized
t : Term to be Generalized Upon
A : Scope of Existential Quantifier
x : Existentially Quantified Variable
LCONTR : Assertion of Line to be Generalized
P2-HYPS : Hypotheses
P1-HYPS : Hypotheses

TPS documentation homepage


EGEN : SRULE

EGEN is an inference rule.
Its priority is 3

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage