Logika: Programming Logics
Logika: Programming Logics¶
These notes were adapted from the Programming Logics lecture notes by David A. Schmidt.
The main adaptation of the work is to use the Sireum Logika formal input language as the notations for the propositional, predicate, and programming logics.
This adaptation work is licensed under a newer license version of Schmidt's -- Creative Commons Attribution 4.0 International License (CC BY 4.0). © Copyright 2016, Robby.
- 1. Introduction: Why bother?
- 2. Circuits and Truth Tables
- 3. Propositional Logic
- 3.1. Propositions
- 3.2. The Sequent
- 3.3. Inference Rules
- 3.4. Logika Proof Syntax
- 3.5. The premise Justification
- 3.6. The assume Justification
- 3.7. Logical Operator Based Justifications
- 3.8. And-Introduction and And-Elimination
- 3.9. Or-Introduction and Or-Elimination
- 3.10. Implies-Introduction and Implies-Elimination
- 3.11. Negation
- 3.12. Negation Introduction
- 3.13. Proof by Contradiction
- 3.14. Important Equivalences
- 3.15. Models of Propositional Logic: Soundness and Completeness
- 3.16. Summary of Rules and Tactics
- 4. The Predicate-Logic Quantifiers
- 5. Programming Logic for Assignments and Conditionals
- 6. Loops and Loop Invariants
- 7. Functions and Procedures