INDIRECT1 : IRULEDEF

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

TPS documentation homepage


INDIRECT1 : MEXPR

INDIRECT1 is a top-level command.
Rule of Indirect Proof Using One Contradictory Line.
The command format for INDIRECT1 is:

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


The arguments have the following meaning:
P3 : Line to be Proven by Contradiction
P2 : Line with Contradiction
H1 : Line with Assumed Negation
B : Positive Conjunct of Contradictory Assertion
A : Assertion to be Proven by Contradiction
P3-HYPS : Hypotheses
P2-HYPS : Hypotheses
H1-HYPS : Hypotheses

TPS documentation homepage


INDIRECT1 : SRULE

INDIRECT1 is an inference rule.
Its priority is NIL

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage