CASES is an intermediate rule definition.
*(D1) H !A(O) OR B(O)
(H2) H,H2 !A(O) Case 1: D1
(P3) H,H2 !C(O)
(H4) H,H4 !B(O) Case 2: D1
(P5) H,H4 !C(O)
*(P6) H !C(O) Cases: D1 P3 P5
Transformation: (P6 D1 ss) ==> (P3 H2 ss) (P5 H4 ss)

TPS documentation homepage


CASES is a top-level command.
Rule of Cases.
The command format for CASES is:

 <n>CASES   P6   D1   P5   H4     P3     H2      B      A      C     P6-HYPS    D1-HYPS    P5-HYPS    H4-HYPS    P3-HYPS    H2-HYPS 

The arguments have the following meaning:
P6 : Conclusion for Both Cases
D1 : Line with Disjunction
P5 : Conclusion in Case 2
H4 : Line with Assumption for Case 2 (Right Disjunct)
P3 : Conclusion in Case 1
H2 : Line with Assumption for Case 1 (Left Disjunct)
B : Right Disjunct
A : Left Disjunct
C : Conclusion
P6-HYPS : Hypotheses
D1-HYPS : Hypotheses
P5-HYPS : Hypotheses
H4-HYPS : Hypotheses
P3-HYPS : Hypotheses
H2-HYPS : Hypotheses

TPS documentation homepage


CASES is an inference rule.
Its priority is 1

TPS documentation homepage

© 1988-99, Carnegie Mellon University.

TPS homepage