Fix a sample proof, improve another.

crisperdue · Feb 12, 2016 · 6acb8ed · 6acb8ed
1 parent a5ce9bc
commit 6acb8ed
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 4 deletions.
diff --git a/introduction.html b/introduction.html
@@ -328,7 +328,7 @@ <h3>Building a simple proof</h3>
   // Modus ponens
   var mp1 = rules.assume('p');
   var mp2 = rules.assume('p => q');
-  var mp3 = rules.forwardChain(mp1, mp2);
+  var mp3 = rules.modusPonens(mp1, mp2);
   var mp4 = rules.asImplication(mp3);
   Toy.renderProof(mp4, $('#modusPonens'));
 

diff --git a/js/sample-proofs.js b/js/sample-proofs.js
@@ -407,9 +407,11 @@ $(function() {
 
     forwardChain: {
       args: function() {
-        var step1 = Toy.rules.assume('p x & (p x => q x)');
-        var step2 = Toy.rules.tautology('a & (a => b) => b');
-        return [step1, step2];
+        var step1 = Toy.rules.assume('p x');
+        var step2 = Toy.rules.assume('p x => q x');
+        var step3 = Toy.rules.makeConjunction(step1, step2);
+        var step4 = Toy.rules.tautology('a & (a => b) => b');
+        return [step3, step4];
       },
       level: 1
     },