| … | |
… | |
| 38 | row( 'd', 'Commutative Properties '), |
38 | row( 'd', 'Commutative Properties '), |
| 39 | row( 'e', 'Associative Properties '), |
39 | row( 'e', 'Associative Properties '), |
| 40 | row( 'f', 'Distributive Properties '), |
40 | row( 'f', 'Distributive Properties '), |
| 41 | row( 'g', 'Equivalence of Contrapositive '), |
41 | row( 'g', 'Equivalence of Contrapositive '), |
| 42 | row( 'h', 'Definition of Implication '), |
42 | row( 'h', 'Definition of Implication '), |
| 43 | row( 'i', 'Definition of Equivalence '), |
43 | row( 'i', 'Definition of Equivalence ')); |
|
|
44 | BEGIN_TEXT |
| 44 | row( 'j', 'Identity Laws \((p \vee F = p \wedge T = p) \) '), |
45 | \{ row( 'j', 'Identity Laws \((p \vee F = p \wedge T = p) \) ')\} |
| 45 | row( 'k', 'Tautology \((p \vee \neg p = T) \) '), |
46 | \{ row( 'k', 'Tautology \((p \vee \neg p = T) \) ') \} |
| 46 | row( 'l', 'Contradiction \((p \wedge \neg p = F) \) '), |
47 | \{ row( 'l', 'Contradiction \((p \wedge \neg p = F) \) ') \} |
|
|
48 | END_TEXT |
|
|
49 | TEXT( |
| 47 | row( 'm', 'Negation of the goal to prove '), |
50 | row( 'm', 'Negation of the goal to prove '), |
| 48 | row( 'n', 'Modus Ponens'), |
51 | row( 'n', 'Modus Ponens'), |
| 49 | row( 'o', 'Modus Tollens'), |
52 | row( 'o', 'Modus Tollens'), |
| 50 | row( 'p', 'Transitivity of Implication'), |
53 | row( 'p', 'Transitivity of Implication'), |
| 51 | row( 'q', 'Conjunctive Simplification'), |
54 | row( 'q', 'Conjunctive Simplification'), |
| … | |
… | |
| 61 | BEGIN_TEXT |
64 | BEGIN_TEXT |
| 62 | $PAR |
65 | $PAR |
| 63 | We want to prove \(s\) by a proof by contradiction from the following propositions. |
66 | We want to prove \(s\) by a proof by contradiction from the following propositions. |
| 64 | END_TEXT |
67 | END_TEXT |
| 65 | |
68 | |
| 66 | TEXT( |
69 | TEXT( begintable(1)); |
| 67 | begintable(1), |
70 | BEGIN_TEXT |
| 68 | row( '\( p \rightarrow q \)' ), |
71 | \{ row( '\( p \rightarrow q \)' ) \} |
| 69 | row( '\( r \rightarrow q \)' ), |
72 | \{ row( '\( r \rightarrow q \)' ) \} |
| 70 | row( '\( \neg q \)' ), |
73 | \{ row( '\( \neg q \)' ) \} |
| 71 | row( '\( \neg(s \wedge T) \rightarrow p \)' ), |
74 | \{ row( '\( \neg(s \wedge T) \rightarrow p \)' ) \} |
| 72 | endtable() |
75 | END_TEXT |
| 73 | ); |
76 | TEXT( endtable() ); |
| 74 | |
77 | |
| 75 | BEGIN_TEXT |
78 | BEGIN_TEXT |
| 76 | $PAR |
79 | $PAR |
| 77 | \( \neg s \) by \{ ans_rule(1) \} |
80 | \( \neg s \) by \{ ans_rule(1) \} |
| 78 | END_TEXT |
81 | END_TEXT |
| … | |
… | |
| 104 | elsif ($version == 2) |
107 | elsif ($version == 2) |
| 105 | { |
108 | { |
| 106 | BEGIN_TEXT |
109 | BEGIN_TEXT |
| 107 | $PAR |
110 | $PAR |
| 108 | We want to prove \(d\) by a proof by contradiction from the following propositions. |
111 | We want to prove \(d\) by a proof by contradiction from the following propositions. |
| 109 | END_TEXT |
|
|
| 110 | |
112 | |
| 111 | TEXT( |
|
|
| 112 | begintable(1), |
113 | \{ begintable(1) \} |
| 113 | row( '\( a \rightarrow b \)' ), |
114 | \{ row( '\( a \rightarrow b \)' ) \} |
| 114 | row( '\( r \rightarrow b \)' ), |
115 | \{ row( '\( r \rightarrow b \)' ) \} |
| 115 | row( '\( \neg b \)' ), |
116 | \{ row( '\( \neg b \)' ) \} |
| 116 | row( '\( \neg(d \wedge T) \rightarrow a \)' ), |
117 | \{ row( '\( \neg(d \wedge T) \rightarrow a \)' ) \} |
| 117 | endtable() |
118 | \{ endtable() \} |
| 118 | ); |
|
|
| 119 | |
119 | |
| 120 | BEGIN_TEXT |
|
|
| 121 | $PAR |
120 | $PAR |
| 122 | \( \neg d \) by \{ ans_rule(1) \} |
121 | \( \neg d \) by \{ ans_rule(1) \} |
| 123 | END_TEXT |
122 | END_TEXT |
| 124 | ANS(str_cmp("m")); |
123 | ANS(str_cmp("m")); |
| 125 | |
124 | |
| … | |
… | |
| 149 | else |
148 | else |
| 150 | { |
149 | { |
| 151 | BEGIN_TEXT |
150 | BEGIN_TEXT |
| 152 | $PAR |
151 | $PAR |
| 153 | We want to prove \(s\) by a proof by contradiction from the following propositions. |
152 | We want to prove \(s\) by a proof by contradiction from the following propositions. |
| 154 | END_TEXT |
|
|
| 155 | |
153 | |
| 156 | TEXT( |
|
|
| 157 | begintable(1), |
154 | \{ begintable(1) \} |
| 158 | row( '\( p \rightarrow b \)' ), |
155 | \{ row( '\( p \rightarrow b \)' ) \} |
| 159 | row( '\( r \rightarrow b \)' ), |
156 | \{ row( '\( r \rightarrow b \)' ) \} |
| 160 | row( '\( \neg b \)' ), |
157 | \{ row( '\( \neg b \)' ) \} |
| 161 | row( '\( \neg(s \wedge T) \rightarrow p \)' ), |
158 | \{ row( '\( \neg(s \wedge T) \rightarrow p \)' ) \} |
| 162 | endtable() |
159 | \{ endtable() \} |
| 163 | ); |
|
|
| 164 | |
160 | |
| 165 | BEGIN_TEXT |
|
|
| 166 | $PAR |
161 | $PAR |
| 167 | \( \neg s \) by \{ ans_rule(1) \} |
162 | \( \neg s \) by \{ ans_rule(1) \} |
| 168 | END_TEXT |
163 | END_TEXT |
| 169 | ANS(str_cmp("m")); |
164 | ANS(str_cmp("m")); |
| 170 | |
165 | |
Parent Directory
| 
Revision Log
| 
Patch