Completing the documentation. Fixed a sample. Some cosmetic improvements.

samples/fitch/README.md

@@ -1,4 +1,6 @@
-This project demonstrates the use of constraint rules to validate proofs in [propositional logic](http://logic.stanford.edu/intrologic/glossary/propositional_logic.html). The proof system is [Fitch](http://logic.stanford.edu/intrologic/glossary/fitch_system.html).
+# Fitch system
+
+This project demonstrates the use of type checking to validate proofs in [propositional logic](http://logic.stanford.edu/intrologic/glossary/propositional_logic.html). The proof system is [Fitch](http://logic.stanford.edu/intrologic/glossary/fitch_system.html).
 
 This project is developed with [JetBrains MPS](https://www.jetbrains.com/mps/) using the [plugin](https://github.com/fisakov/constraints-typechecking) that provides an experimental feature: *type checking with constraint rules*.
 
@@ -13,6 +15,14 @@ This project is developed with [JetBrains MPS](https://www.jetbrains.com/mps/) u
 4. Clone this repository and open the project with MPS
 5. Execute 'Rebuild Project'
 
+### Using the proof checker
+
+Open a proof and invoke «Mark All Types» (Cmd+F7 on Mac). 
+
+![](img/menu.png)
+
+If the proof is valid, the goal is underlined with green, otherwise the goal and the reasoning(s) that have errors are marked with red. 
+
 ### Propositional logic language
 
 The language enables to write boolean expressions and consist of propositional constants and the following logical operations: conjunction (And), disjunction (Or), negation (Not), implication (If), and biconditional (Iff). The following table summarises the operations and symbols that are used to represent them.
@@ -36,7 +46,7 @@ p => q
 
 ### Proof language 
 
-Proofs in propositional logic are built from reasonings and subproofs. A reasoning always have a sentence serving as conclusion, and zero, one, or more bases (premises) that refer other reasonings. A subproof has a similar structure, with the exception that premises here always come in form of assumptions. Here is the list of proposition types: 
+Proofs in propositional logic are built from reasonings and subproofs. A reasoning always has a sentence serving as conclusion, and zero, one, or more bases (premises) that refer other reasonings. A subproof has a similar structure, with the exception that premises here always come in form of assumptions. Here is the list of proposition types: 
 
 | Proposition | Number of bases | Usage |
 |:--|:--|:--|
@@ -61,30 +71,91 @@ The rules of inference are defined by the used [system](http://logic.stanford.ed
 | Biconditional Introduction | <=>I | 2 |
 | Biconditional Elimination | <=>E | 1 |
 
-And Introduction, And Elimination, Or Introduction, Or Elimination, Negation Introduction, Negation Elimination, Implication Introduction, Implication Elimination, Biconditional Introduction, Biconditional Elimination.
-
 Here is a sample proof in propositional logic.
 
 ![An example of proof in Fitch system](img/sample-proof.png)
 
+The proof is validated using experimental type checking with constraint rules, which is a new feature being developed for MPS. The sentences that constitute judgements in the proof are represented as terms in the internal language of constraint rules. The inference rules use terms unification to match sentences and extract sub-sentences. Every judgement is assigned a conclusion and, if the judgement is proved to be correct, it is marked as valid. 
+
 Here is a sample of an inference rule written in the language of constraint rules processing.
 
 ![An example of inference rule](img/sample-rule.png)
 
+This rule is activated when **all** of the following is true:
+
+- The judgement `ne` is assigned a conclusion (captured in `Con`)
+- The judgement’s premise is assigned a conclusion 
+- The premise’s conclusion matches `~~Con`
+- The premise is valid
+
+The result of the rule’s activation is simply that the judgement `ne` is marked as valid.
+
 ### Inner workings
 
-Rule templates are applied to each of the reasoning nodes and produce a constraint rules program, that is then evaluated. First the automatic rules are triggered, which activate constraint «conclusion» binding reasoning to the propositional term corresponding to the sentence contained in the reasoning. 
+Rule templates are applied to each of the reasoning nodes and produce a constraint rules program, that is then evaluated. First the automatic rules, the rules that are always generated, are triggered, which activate constraint `conclusion` binding reasoning to the propositional term corresponding to the sentence contained in the reasoning. 
 
-Constraint «valid» signifies the validity of a reasoning. Premise, Assumption and Reiteration are valid automatically.
+![Automatic rule activating `conclusion` constraint](img/judgement_conclusion.png)
 
-Activated constraints «conclusion» and «valid» trigger the rest of the constraint rule, which correspond to inference rules. 
+Constraint `valid` signifies the validity of a reasoning. Premise and Assumption are valid automatically. Reiteration is valid if its conclusion matches the conclusion of the judgement being reiterated.
 
-The rule input is matched against «conclusion» constraints corresponding to reasonings from rule’s premises and conclusions, unifying matching terms denoted with same logical variable. If rule succeeds, a constraint «valid» is activated for the analysed judgement. 
+![](img/auto_valid.png)
 
-The proof’s goal is unified with the last **top-level** reasoning. If the last reasoning is marked valid, so is the goal.
+Activated constraints `conclusion` and `valid` trigger the rest of the constraint rules, which correspond to inference rules. 
+
+The formal definition of And Introduction and And Elimination inference rules are the following. 
+
+![And Introduction and And Elimination](img/and_rules.png)
+
+For simplicity, in this sample project we restrict ourselves to only two conjunctions, but we should account for premises being enumerated in any order. Here are the two inference rules for conjunction in the language of constraint rules. 
+
+![And Introduction inference rule](img/and_intro.png)
+![And Elimination inference rule](img/and_elim.png)
+
+All inference rules are organised similarly: the premises (the part above the horizontal separator) are the input, which triggers the rule, and the conclusion is what the rule produces. All constraints in the input part are to be «kept», that is they are stored for future use by other rules after this rule completes. 
+
+![Or Introduction and Or Elimination](img/or_rules.png)
+
+As with conjunction, we only support two disjunct in a disjunction, but their order can be arbitrary.
+
+![Or Introduction inference rule](img/or_intro.png)
+
+![Or Elimination inference rule](img/or_elim.png)
+
+![Negation Introduction and Negation Elimination](img/neg_rules.png)
+
+Negation introduction requires two premises, but their order is not specified, so we have two versions of an inference rule to account for this. There is only one version of Negation Elimination inference rule. 
+
+![Negation Introduction inference rule](img/not_intro.png)
+
+![Negation Elimination inference rule](img/not_elim.png)
+
+![Implication Introduction and Implication Elimination](img/if_rules.png)
+
+In the case of Implication Introduction the premise is not a judgement, but a subproof. We need to create one additional rule for the singular case, whereas the subproof serving as the premise has only the assumption. This is because we’re referring to both the first and the last judgments in the subproof, and the rule requires both to have a conclusion in the form of a constraint, which in the case of a singular assumption is the same constraint.  
+
+![Implication Introduction inference rules](img/if_intro.png)
+
+![Implication Elimination inference rule](img/if_elim.png)
+
+![Biconditional Introduction and Biconditional Elimination](img/iff_rules.png)
+
+We create two versions of both Biconditional Introduction and Biconditional Elimination rules to account for arbitrary order of premises and arbitrary selection of the conclusion.
+
+![Biconditional Introduction inference rule](img/iff_intro.png)
+
+![Biconditional Elimination inference rule](img/iff_elim.png)
+
+
+The constraint `goal` is activated automatically to associate the goal of the proof with its formal sentence.
+
+![Goal](img/goal.png)
+
+The proof’s goal is unified with the last **top-level** reasoning. Since reasonings are organised in a hierarchy using subproofs, the last reasoning in the proof is automatically the last top-level one. If that reasoning is marked valid, so is the goal.
+
+![Goal validation rule](img/goal_valid.png)
 
 ### Type checking
 
-All reasonings are checked in the second stage. Reasonings that don’t have «valid» constraint are marked with error. 
+The actual type checking is trivial. The first stage of the constraint rules program does all the job and produces `valid` constraints, which are then analysed. All reasonings are checked in the second stage. Reasonings that don’t have `valid` constraint are marked with error. 
 
-There is only one type «OK». Only the goal gets assigned a type in case it matches the last top-level term in the proof.
+There is only one type «OK». Only the goal gets assigned a type in case it marked as `valid`, otherwise an error is produced. 

samples/fitch/languages/jetbrains.mps.fitch/sandbox/models/jetbrains.mps.fitch.sandbox.mps

@@ -1529,6 +1529,51 @@
         </node>
       </node>
     </node>
+    <node concept="2jWza5" id="3eN$koMSiRw" role="2jVTa7">
+      <node concept="2jWGsN" id="3eN$koMSiRx" role="2jWza4">
+        <node concept="2jWLFD" id="3eN$koMSiRW" role="3MT$nN">
+          <property role="TrG5h" value="p" />
+        </node>
+      </node>
+      <node concept="2jWz52" id="3eN$koMSiS2" role="2jWza4">
+        <node concept="2jWMwi" id="3eN$koMSiSc" role="2jWFax">
+          <ref role="2jWMyc" node="5A8qZLXfUx1" />
+        </node>
+        <node concept="2jWLFQ" id="3eN$koMSiSf" role="3MT$nN">
+          <node concept="2jWLFD" id="3eN$koMSiSh" role="2jWLFT">
+            <property role="TrG5h" value="q" />
+          </node>
+        </node>
+      </node>
+    </node>
+    <node concept="2jWAjC" id="3eN$koMSiSP" role="2jVTa7">
+      <node concept="2jWMwi" id="3eN$koMSiTs" role="2jWFax">
+        <ref role="2jWMyc" node="3eN$koMSiRw" />
+      </node>
+      <node concept="2jWM_K" id="3eN$koMSiTz" role="3MT$nN">
+        <node concept="2jWLFD" id="3eN$koMSiTv" role="2jWM_N">
+          <property role="TrG5h" value="p" />
+        </node>
+        <node concept="2jWLFQ" id="3eN$koMSiTE" role="2jWM_P">
+          <node concept="2jWLFD" id="3eN$koMSiTG" role="2jWLFT">
+            <property role="TrG5h" value="q" />
+          </node>
+        </node>
+      </node>
+    </node>
+    <node concept="2jWz57" id="3eN$koMSiUl" role="2jVTa7">
+      <node concept="2jWMwi" id="3eN$koMSiV2" role="2jWFax">
+        <ref role="2jWMyc" node="5A8qZLXfUzE" />
+      </node>
+      <node concept="2jWMwi" id="3eN$koMSiVh" role="2jWFax">
+        <ref role="2jWMyc" node="3eN$koMSiSP" />
+      </node>
+      <node concept="2jWLFQ" id="3eN$koMSiVc" role="3MT$nN">
+        <node concept="2jWLFD" id="3eN$koMSiVe" role="2jWLFT">
+          <property role="TrG5h" value="p" />
+        </node>
+      </node>
+    </node>
     <node concept="GyqZO" id="5A8qZLXfUwQ" role="GyqZB">
       <node concept="2jWLFQ" id="5A8qZLXfUwX" role="GyqZP">
         <node concept="2jWLFD" id="5A8qZLXfUwU" role="2jWLFT">