[npl] / trunk / NationalProblemLibrary / SUNYSB / contradiction.pg Repository:
ViewVC logotype

View of /trunk/NationalProblemLibrary/SUNYSB/contradiction.pg

Parent Directory Parent Directory | Revision Log Revision Log


Revision 323 - (download) (annotate)
Sun Aug 13 01:05:41 2006 UTC (6 years, 9 months ago) by jj
File size: 4701 byte(s)
Fixed typesetting.

    1 ## DESCRIPTION
    2 ## Discrete Mathematics
    3 ## ENDDESCRIPTION
    4 
    5 ## KEYWORDS('discrete mathematics','logic','proof by contradiction')
    6 ## Tagged by cmd6a 8/6/06
    7 
    8 ## DBsubject('Discrete Mathematics')
    9 ## DBchapter('Logic')
   10 ## DBsection('Reasoning')
   11 ## Date('')
   12 ## Author('')
   13 ## Institution('SUNYSB')
   14 ## TitleText1('')
   15 ## EditionText1('')
   16 ## AuthorText1('')
   17 ## Section1('')
   18 ## Problem1('')
   19 
   20 DOCUMENT();
   21 loadMacros('PG.pl',
   22            'PGbasicmacros.pl',
   23            'PGchoicemacros.pl',
   24            'PGanswermacros.pl'
   25 );
   26 TEXT(beginproblem());
   27 $showPartialCorrectAnswers = 0;
   28 
   29 BEGIN_TEXT
   30     For the following $BBOLD proof by contradiction $EBOLD provide the justifications at each step,
   31 using the following equivalences and inference rules.  Use the following keys:
   32 END_TEXT
   33 TEXT(
   34     begintable(2),
   35          row( 'a', 'Idempotent Law'),
   36          row( 'b', 'Double Negation'),
   37          row( 'c', 'De Morgan~~'s Law'),
   38    row( 'd', 'Commutative Properties '),
   39          row( 'e', 'Associative Properties '),
   40          row( 'f', 'Distributive Properties '),
   41          row( 'g', 'Equivalence of Contrapositive '),
   42          row( 'h', 'Definition of Implication '),
   43          row( 'i', 'Definition of Equivalence '));
   44 BEGIN_TEXT
   45      \{  row( 'j', 'Identity Laws \((p \vee F = p \wedge T = p) \) ')\}
   46      \{  row( 'k', 'Tautology \((p \vee \neg p = T) \) ') \}
   47      \{  row( 'l', 'Contradiction \((p \wedge \neg p = F) \) ') \}
   48 END_TEXT
   49 TEXT(
   50          row( 'm', 'Negation of the goal to prove '),
   51          row( 'n', 'Modus Ponens'),
   52          row( 'o', 'Modus Tollens'),
   53          row( 'p', 'Transitivity of Implication'),
   54          row( 'q', 'Conjunctive Simplification'),
   55          row( 'r', 'Conjunctive Addition'),
   56          row( 's', 'Disjunctive Addition'),
   57     endtable()
   58 );
   59 
   60 $version = random(1,3,1);
   61 if ($version == 1)
   62 {
   63 
   64 BEGIN_TEXT
   65     $PAR
   66     We want to prove \(s\) by a proof by contradiction from the following propositions.
   67 END_TEXT
   68 
   69 TEXT( begintable(1));
   70 BEGIN_TEXT
   71   \{     row( '\( p \rightarrow q \)' ) \}
   72   \{     row( '\( r \rightarrow q \)' ) \}
   73   \{     row( '\( \neg q \)' ) \}
   74   \{     row( '\( \neg(s \wedge T) \rightarrow p \)' ) \}
   75 END_TEXT
   76 TEXT( endtable() );
   77 
   78 BEGIN_TEXT
   79     $PAR
   80     \( \neg s \) by \{ ans_rule(1) \}
   81 END_TEXT
   82 ANS(str_cmp("m"));
   83 
   84 BEGIN_TEXT
   85     $PAR
   86     \( \neg p \) by  \{ ans_rule(1) \} between \( p \rightarrow q \) and \( \neg q \)
   87 END_TEXT
   88 ANS(str_cmp("o"));
   89 
   90 BEGIN_TEXT
   91     $PAR
   92     \( s \wedge T \) by  \{ ans_rule(1) \} between \( \neg(s \wedge T) \rightarrow p \) and \( \neg p \) previously deduced.
   93 END_TEXT
   94 ANS(str_cmp("o"));
   95 
   96 BEGIN_TEXT
   97     $PAR
   98     \( s \) by  \{ ans_rule(1) \} of \( s \wedge T \)
   99 END_TEXT
  100 ANS(str_cmp("q"));
  101 
  102 BEGIN_TEXT
  103     $PAR
  104     We have \( s \) and \( \neg s \) true, therefore we have a contradiction.
  105 END_TEXT
  106 }
  107 elsif ($version == 2)
  108 {
  109 BEGIN_TEXT
  110     $PAR
  111     We want to prove \(d\) by a proof by contradiction from the following propositions.
  112 
  113 \{    begintable(1) \}
  114 \{         row( '\( a \rightarrow b \)' ) \}
  115 \{         row( '\( r \rightarrow b \)' ) \}
  116 \{         row( '\( \neg b \)' ) \}
  117 \{         row( '\( \neg(d \wedge T) \rightarrow a \)' ) \}
  118 \{    endtable() \}
  119 
  120     $PAR
  121     \( \neg d \) by \{ ans_rule(1) \}
  122 END_TEXT
  123 ANS(str_cmp("m"));
  124 
  125 BEGIN_TEXT
  126     $PAR
  127     \( \neg a \) by  \{ ans_rule(1) \} between \( a \rightarrow b \) and \( \neg b \)
  128 END_TEXT
  129 ANS(str_cmp("o"));
  130 
  131 BEGIN_TEXT
  132     $PAR
  133     \( d \wedge T \) by  \{ ans_rule(1) \} between \( \neg(d \wedge T) \rightarrow a \) and \( \neg a \) previously deduced.
  134 END_TEXT
  135 ANS(str_cmp("o"));
  136 
  137 BEGIN_TEXT
  138     $PAR
  139     \( d \) by  \{ ans_rule(1) \} of \( d \wedge T \)
  140 END_TEXT
  141 ANS(str_cmp("q"));
  142 
  143 BEGIN_TEXT
  144     $PAR
  145     We have \( d \) and \( \neg d \) true, therefore we have a contradiction.
  146 END_TEXT
  147 }
  148 else
  149 {
  150 BEGIN_TEXT
  151     $PAR
  152     We want to prove \(s\) by a proof by contradiction from the following propositions.
  153 
  154 \{    begintable(1) \}
  155 \{         row( '\( p \rightarrow b \)' ) \}
  156 \{         row( '\( r \rightarrow b \)' ) \}
  157 \{         row( '\( \neg b \)' ) \}
  158 \{         row( '\( \neg(s \wedge T) \rightarrow p \)' ) \}
  159 \{    endtable() \}
  160 
  161     $PAR
  162     \( \neg s \) by \{ ans_rule(1) \}
  163 END_TEXT
  164 ANS(str_cmp("m"));
  165 
  166 BEGIN_TEXT
  167     $PAR
  168     \( \neg p \) by  \{ ans_rule(1) \} between \( p \rightarrow b \) and \( \neg b \)
  169 END_TEXT
  170 ANS(str_cmp("o"));
  171 
  172 BEGIN_TEXT
  173     $PAR
  174     \( s \wedge T \) by  \{ ans_rule(1) \} between \( \neg(s \wedge T) \rightarrow p \) and \( \neg p \) previously deduced.
  175 END_TEXT
  176 ANS(str_cmp("o"));
  177 
  178 BEGIN_TEXT
  179     $PAR
  180     \( s \) by  \{ ans_rule(1) \} of \( s \wedge T \)
  181 END_TEXT
  182 ANS(str_cmp("q"));
  183 
  184 BEGIN_TEXT
  185     $PAR
  186     We have \( s \) and \( \neg s \) true, therefore we have a contradiction.
  187 END_TEXT
  188 }
  189 
  190 ENDDOCUMENT();
  191 
  192 
  193 
  194 
  195 

aubreyja at gmail dot com
ViewVC Help
Powered by ViewVC 1.0.9