INDIRECT : CONTEXT

INDIRECT is a context.
Files containing arguments for exec commands.

TPS documentation homepage


INDIRECT : IRULEDEF

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

TPS documentation homepage


INDIRECT : MEXPR

INDIRECT is a top-level command.
Rule of Indirect Proof.
The command format for INDIRECT is:

 <n>INDIRECT   P3   P2   H1    A     P3-HYPS    P2-HYPS    H1-HYPS 
"LINE" "LINE" "LINE" "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
A : Assertion to be Proven by Contradiction
P3-HYPS : Hypotheses
P2-HYPS : Hypotheses
H1-HYPS : Hypotheses

TPS documentation homepage


INDIRECT : SRULE

INDIRECT is an inference rule.
Its priority is 6

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage