DEDUCT : IRULEDEF

DEDUCT is an intermediate rule definition.
(H1) H,H1 !A(O) Hyp
(D2) H,H1 !B(O)
*(P3) H !A(O) IMPLIES B(O) Deduct: D2
Transformation: (P3 ss) ==> (D2 H1 ss)

TPS documentation homepage


DEDUCT : MEXPR

DEDUCT is a top-level command.
The deduction rule.
The command format for DEDUCT is:

 <n>DEDUCT   P3   D2   H1    B      A     P3-HYPS    D2-HYPS    H1-HYPS 
"LINE" "LINE" "LINE" "GWFF" "GWFF" "LINELIST" "LINELIST" "LINELIST"


The arguments have the following meaning:
P3 : Line with Implication
D2 : Line with Conclusion
H1 : Line with Hypothesis
B : Succedent of Implication
A : Antecendent of Implication
P3-HYPS : Hypotheses
D2-HYPS : Hypotheses
H1-HYPS : Hypotheses

TPS documentation homepage


DEDUCT : SRULE

DEDUCT is an inference rule.
Its priority is 2

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage