ENEG : IRULEDEF

ENEG is an intermediate rule definition.
*(D1) H !~A(O)
(P2) H !A(O)
*(P3) H !FALSEHOOD NegElim: D1 P2
Transformation: (P3 D1 ss) ==> (P2 ss)

TPS documentation homepage


ENEG : MEXPR

ENEG is a top-level command.
Rule of Negation Elimination.
The command format for ENEG is:

 <n>ENEG   P3   D1   P2    A     P3-HYPS    D1-HYPS    P2-HYPS 
"LINE" "LINE" "LINE" "GWFF" "LINELIST" "LINELIST" "LINELIST"


The arguments have the following meaning:
P3 : Line with Falsehood
D1 : Line with Negative Wff
P2 : Line with Positive Wff
A : Wff
P3-HYPS : Hypotheses
D1-HYPS : Hypotheses
P2-HYPS : Hypotheses

TPS documentation homepage


ENEG : SRULE

ENEG is an inference rule.
Its priority is NIL

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage