ECONJ : IRULEDEF

ECONJ is an intermediate rule definition.
*(D1) H !A(O) AND B(O)
(D2) H !A(O) Conj: D1
(D3) H !B(O) Conj: D1
Transformation: (pp D1 ss) ==> (pp D2 D3 ss)

TPS documentation homepage


ECONJ : MEXPR

ECONJ is a top-level command.
Rule to infer two conjuncts from a conjunction.
The command format for ECONJ is:

 <n>ECONJ   D1   D3   D2    B      A     D1-HYPS    D3-HYPS    D2-HYPS 
"LINE" "LINE" "LINE" "GWFF" "GWFF" "LINELIST" "LINELIST" "LINELIST"


The arguments have the following meaning:
D1 : Line with Conjunction
D3 : Line with Right Conjunct
D2 : Line with Left Conjunct
B : Right Conjunct
A : Left Conjunct
D1-HYPS : Hypotheses
D3-HYPS : Hypotheses
D2-HYPS : Hypotheses

TPS documentation homepage


ECONJ : SRULE

ECONJ is an inference rule.
Its priority is 1

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage