User:Lord Farin/Long-Term Projects/MLCS
Processing of 'Mathematical Logic for Computer Science (3e)'
First page it covers: Definition:Statement.
First page covered by Appendices: Definition:Set.
A book extensively and rigorously building the basic foundations of logic.
Progress thus far
Up to Definition:Language of Propositional Logic/Alphabet/Sign/Connective. --Lord_Farin (talk) 15:48, 16 February 2013 (UTC)
Up to $\S 3.3$. Ended at Soundness and Completeness of Gentzen Proof System. — Lord_Farin (talk) 23:00, 3 April 2014 (UTC)
Up to $\S 3.6$. Ended at Principle of Commutation/Forward Implication/Formulation 2/Proof 2. — Lord_Farin (talk) 10:57, 5 April 2014 (UTC)
Skipped thus far (that is, what needs to be done still)
- Part of $\S 2.7.2$ proving Completeness Theorem for Semantic Tableaus using Hintikka sets.
- Proving correctness of heuristic adaptation of Semantic Tableau Algorithm, Exc. 2.19.
- Covering of derived rules of inference from $\S 3.4$, probably most easily done by introducing a third formulation on existing rules. Applies to $3.15,3.17,3.19,3.21,3.24,3.26$. Skipped rest of $\S 3.4$ and $\S 3.5$ because of this.
- Equivalence of Definitions of Semantic Equivalence for Boolean Interpretations
- Classification of Alpha-Formulas
- Classification of Beta-Formulas