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

    1 ## DESCRIPTION
    2 ## Discrete Mathematics
    3 ## ENDDESCRIPTION
    4 
    5 ## KEYWORDS('discrete mathematics','logic','proof')
    6 ## Tagged by cmd6a 8/6/06
    7 
    8 ## DBsubject('Discrete Mathematics')
    9 ## DBchapter('Logic')
   10 ## DBsection('First Order Logic')
   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 proof (of equivalence of 2 formulae) provide the justifications at each step,
   31 using the following equivalences.  Use the following key:
   32     $PAR
   33 END_TEXT
   34 TEXT(
   35     begintable(2),
   36          row( 'a', 'Idempotent Law'),
   37          row( 'b', 'Double Negation'),
   38          row( 'c', 'De Morgan~~'s Law'),
   39    row( 'd', 'Commutative Properties '),
   40          row( 'e', 'Associative Properties '),
   41          row( 'f', 'Distributive Properties '),
   42          row( 'g', 'Equivalence of Contrapositive '),
   43          row( 'h', 'Definition of Implication '),
   44          row( 'i', 'Definition of Equivalence '),
   45          row( 'j', 'Identity Laws \( (p \vee F \equiv p \wedge T \equiv p) \) '),
   46          row( 'k', 'Tautology \( (p \vee \neg p \equiv T) \) '),
   47          row( 'l', 'Contradiction \( (p \wedge \neg p \equiv F) \) '),
   48     endtable()
   49 );
   50 
   51 # Christelle+proof proofReason3.pg
   52 
   53 $version = random(1,2,1);
   54 if ($version == 1)
   55 {
   56 
   57 BEGIN_TEXT
   58     $PAR
   59     \( p \rightarrow (p \wedge q) \) \( \equiv \) $BR
   60     \( \neg p \vee (p \wedge q) \) by  \{ ans_rule(1) \}
   61 END_TEXT
   62 ANS(str_cmp("h"));
   63 
   64 BEGIN_TEXT
   65     \( \equiv \) \( (\neg p \vee p) \wedge (\neg p \vee q) \)
   66     by \{ ans_rule(1) \}
   67 END_TEXT
   68 ANS(str_cmp("f"));
   69 
   70 BEGIN_TEXT
   71     \( \equiv \) \( (p \vee \neg p) \wedge (\neg p \vee q) \)
   72     by \{ ans_rule(1) \}
   73 END_TEXT
   74 ANS(str_cmp("d"));
   75 
   76 BEGIN_TEXT
   77     \( \equiv \) \( T \wedge (\neg p \vee q) \)
   78     by \{ ans_rule(1) \}
   79 END_TEXT
   80 ANS(str_cmp("k"));
   81 
   82 BEGIN_TEXT
   83     \( \equiv \) \( (\neg p \vee q) \wedge T\)     by \{ ans_rule(1) \}
   84 END_TEXT
   85 ANS(str_cmp("d"));
   86 
   87 BEGIN_TEXT
   88     \( \equiv \) \( \neg p \vee q \) by \{ ans_rule(1) \}
   89 END_TEXT
   90 ANS(str_cmp("j"));
   91 }
   92 else
   93 {
   94 BEGIN_TEXT
   95     $PAR
   96     \( \neg(\neg p \wedge q) \wedge (p \vee q)\) $BR
   97     = \( (\neg(\neg p)\vee \neg q)\wedge( p \vee q) \) by \{ ans_rule(1) \}
   98 END_TEXT
   99 ANS(str_cmp("c"));
  100 
  101 BEGIN_TEXT
  102     = \( (p \vee \neg q) \wedge (p \vee q) \) by \{ ans_rule(1) \}
  103 END_TEXT
  104 ANS(str_cmp("b"));
  105 
  106 BEGIN_TEXT
  107     = \( p \vee (\neg q \wedge q) \) by \{ ans_rule(1) \}
  108 END_TEXT
  109 ANS(str_cmp("f"));
  110 
  111 BEGIN_TEXT
  112     = \( p \vee (q \wedge \neg q) \) by \{ ans_rule(1) \}
  113 END_TEXT
  114 ANS(str_cmp("d"));
  115 
  116 BEGIN_TEXT
  117     = \( p \vee F \) by \{ ans_rule(1) \}
  118 END_TEXT
  119 ANS(str_cmp("l"));
  120 
  121 BEGIN_TEXT
  122     = \( p \) by \{ ans_rule(1) \}
  123 END_TEXT
  124 ANS(str_cmp("j"));
  125 }
  126 
  127 ENDDOCUMENT();
  128 
  129 
  130