CalcCheck Instances for COMPSCI&SFWRENG 2DM3, Fall 2020

(Accessing the notebooks from here bypasses Avenue, so you won't be able to save, nor see your previous saves.)

Introduction to Calculational Proofs

• Example 1.1: Portia's Suitor's Dilemma
• Example 1.2: The Answer
• Homework 1: Simple Calculations in CalcCheck
• Exercise 1.1: Simple Calculations in CalcCheck
• Exercise 1.2: Calculations using the Equational Theory of Integers
• Exercise 1.3: Boolean Calculations
• Exercise 2.1: An Equational Theory of Integers
• Homework Notebook 2.1: Identity Jamboree
• Homework Notebook 2.2: Implication
• Exercise 2.2: Substitution
• Exercise 2.3: Proving in the Equational Theory of Integers with Rigid Matching
• Exercise 2.4: Proving in the Equational Theory of Integers without Automatic Associativity and Symmetry
• Exercise 2.5: Proving in the Equational Theory of Integers for Masochists
• Homework Notebook 3.1: Substitution
• Homework Notebook 3.2: Correctness of Assignment Commands
• Exercise 2.6: Assignment Commands with Boolean Variables
• Homework Notebook 4.1: Working with ‘Interfaces’, ‘Specifications’
• Homework Notebook 4.2: Swap

Propositional Calculus, Natural Induction

• Homework Notebook 4.3: First Steps in Propositional Calculus
• Reference Notebook on Propositional Calculus: From Equivalence to Inequivalence
• Exercise 3.1: Knights and Knaves
• Exercise 3.2: Propositional Calculus: Disjunction
• Exercise 3.3: Propositional Calculus: Conjunction
• Exercise 3.1b: Knights and Knaves — Using `_says-⟪_⟫`
• Assignment 1: “Midterm 1: Magmas, Monoids, and Groups”
• Homework 5 Notebook 1: Reversed Command Correctness Notation
• Homework 5 Notebook 2: Conjunction
• Homework 5 Notebook 3: Natural Numbers and Induction
• Exercise 4.1: Implication
• Exercise 4.2: Natural Numbers and Induction: Addition and Multiplication
• Exercise 4.3: Monus Subtraction
• Reference Notebook 4.1: Inequality
• Homework 6 Notebook 1: Propositional Calculus: An Alternate Definition of Conjunction
• Homework 6 Notebook 2: Zero Sums and Products in ℕ; Factorial
• Homework 7 Notebook 1: Implication
• Homework 7 Notebook 2: Leibniz as Axiom, Replacement
• Exercise 5.1: Leibniz as Axiom, Replacement
• Exercise 5.2: Order and Strict-order on ℕ

Structured Proofs and Sum/Product Quantification

• Homework 8 Notebook 1: Quantification Expansion
• Homework 8 Notebook 2: Quantification Expansion
• Homework 8 Notebook 3: Quantification Expansion
• Homework 8 Notebook 4: Monotonicity
• Homework 8 Notebook 5: Predecessors in ℕ
• Homework 8 Notebook 6: Predecessors in ℕ
• Exercise 6.1: Implication Chains and Monotonicity
• Exercise 6.2: Simple Proofs `By cases` on ℕ
• Assignment 2: Order Theory
• Reference Notebook 6.1: Sum Quantification in ℕ
• Exercise 6.3: Quantification Expansion
• Exercise 6.4: Manipulating Ranges in ℕ
• Exercise 6.5: “Split-off Term” Theorems for Sum Quantification on ℕ

Quantification and Predicate Logic

• Homework 9 Notebook 1: Substituting into Quantifications
• Homework 9 Notebook 2: Conditional Expressions
• Homework 10 Notebook 1: Midterm 3 Prep
• Reference Notebook 6.2: Product Quantification in ℕ
• Reference Notebook 6.3: Universal Quantification
• Reference Notebook 6.4: Existential Quantification
• Exercise 7.1: Positivity
• Exercise 7.2: Partial Solutions to Exercise 7.1: Positivity
• Exercise 7.3: Order on Integers
• Homework 11 Notebook 1: Introduction to Instantiation
• Homework 11 Notebook 2: Practice with Universal and Existential Quantification in the Setting of ℕ
• Exercise 7.4: Practice with Universal and Existential Quantification in the Setting of ℕ
• Homework 12: Quantification Proofs: Monotonicity of Sum Quantification in ℕ
• Homework 13: Using the Induction Principle for `_+ 1` in ℕ
• Exercise 8.1: Indirect Equality, Maximum, and Minimum on Integers
• Exercise 8.2: Practice with Universal and Existential Quantification in the Setting of ℤ
• Exercise 8.3: “Mixed Monotonicity”
• Assignment 3: Residuals — A Theory of Divisions
• Homework 14: Introduction to Sequences
• Exercise 9.1: Sequences
• Homework 15: Sets
• Reference Notebook 9.1: Set Theory
• Exercise 9.2: Set Theory

Relations, Graphs, etc.

• Homework 16 Notebook 1: Pairs and Cartesian Products
• Homework 16 Notebook 2: Relations via Set Theory I
• Assignment 4: Converse — A Theory of “Undoability”
• Homework 17: Relations via Set Theory II
• Exercise 10.1: Relations via Set Theory: Properties of the Basic Operators
• Exercise 10.2: Relation-Algebraic Formalisation
• Exercise 10.3: Relations via Set Theory: Counterexamples for Non-Properties
• Homework 18: Heterogeneous Relation Properties
• Exercise 11.1: Starting Abstract Relation Algebra from Inclusion, Composition, and Converse
• Exercise 11.2: Continuing Abstract Relation Algebra with Intersection
• Reference Notebook 11.1: Abstract Relation Algebra: Starting from Inclusion, Composition, and Converse
• Reference Notebook 11.2: Continuing Abstract Relation Algebra with Intersection
• Reference Notebook 11.3: Abstract Relation Algebra: Binary Union
• Reference Notebook 11.4: Abstract Relation Algebra: Least Relations
• Homework 19: Operators Combining Sets and Relations
• Assignment 5: Permutations and Combinations
• Bonus Assignment 6: Permutations and Combinations
• Reference Notebook 12.1: Abstract Relation Algebra: Union Quantification
• Exercise 12.1: Binary Trees
• Exercise 12.2: More Relation-algebraic Proofs
• Exercise 12.3: Abstract Relation Algebra: Reflexive-transitive Closure
• Homework 20 Notebook 1: Discrete Probability
• Homework 20 Notebook 2: Huffman Trees