INDIRECT2 : IRULEDEF

INDIRECT2 is an intermediate rule definition.
(H1) H,H1 !~A(O) Assume negation
(P2) H,H1 !B(O)
(P3) H,H1 !~B(O)
*(P4) H !A(O) Indirect: P2 P3
Transformation: (P4 ss) ==> (P2 H1 ss) (P3 H1 ss)

TPS documentation homepage


INDIRECT2 : MEXPR

INDIRECT2 is a top-level command.
Rule of Indirect Proof Using Two Contradictory Lines.
The command format for INDIRECT2 is:

 <n>INDIRECT2   P4   P3   P2   H1      B      A     P4-HYPS    P3-HYPS    P2-HYPS    H1-HYPS 
"LINE" "LINE" "LINE" "LINE" "GWFF" "GWFF" "LINELIST" "LINELIST" "LINELIST" "LINELIST"


The arguments have the following meaning:
P4 : Line to be Proven by Contradiction
P3 : Line with Negated Consequence of Assumption
P2 : Line with Positive Consequence of Assumption
H1 : Line with Assumed Negation
B : One of Two Contradictory Consequences of Assumption
A : Assertion to be Proven by Contradiction
P4-HYPS : Hypotheses
P3-HYPS : Hypotheses
P2-HYPS : Hypotheses
H1-HYPS : Hypotheses

TPS documentation homepage


INDIRECT2 : SRULE

INDIRECT2 is an inference rule.
Its priority is NIL

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage