INEG : IRULEDEF

INEG is an intermediate rule definition.
(H1) H,H1 !A(O) Hyp
(P2) H,H1 !FALSEHOOD
*(P3) H !~A(O) NegIntro: P2
Transformation: (P3 ss) ==> (P2 H1 ss)

TPS documentation homepage


INEG : MEXPR

INEG is a top-level command.
Rule of Negation Introduction
The command format for INEG is:

 <n>INEG   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 with Negation
P2 : Line with Contradiction
H1 : Line with Assumption
A : Wff Whose Negation is to be Proved
P3-HYPS : Hypotheses
P2-HYPS : Hypotheses
H1-HYPS : Hypotheses

TPS documentation homepage


INEG : SRULE

INEG is an inference rule.
Its priority is NIL

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage