CalcCheck Instances for COMPSCI&SFWRENG 2DM3, Fall 2018

Introduction to Calculational Reasoning via an Equational Theory of Integers

• Example 1.1: Portia's Suitor's Dilemma
• Example 1.2: The Answer
• Exercise 1.1: Calculations using the Equational Theory of Integers
• Reference 1.1: Operator Precedences in the Spirit of LADM
• Reference 1.2: Equational Axioms for Integers
• Exercise 1.2: Substitutions
• Exercise 1.3: An Equational Theory of Integers
• Homework 1: Simple Calculations in CalcCheck
• Exercise 1.4: Proving in the Equational Theory of Integers without Automatic Associativity and Symmetry
• Exercise 1.5: Proving in the Equational Theory of Integers with Rigid Matching
• Exercise 1.6: Proving in the Equational Theory of Integers for Masochists
• Assignment 1.1: Calculations using the Equational Theory of Integers
• Assignment 1.2: Building An Equational Theory of Integers
• Assignment 1.3: Very Explicit Proving in the Equational Theory of Integers

Propositional Calculus

• Homework 2: Evaluating Boolean Expressions
• Homework 3: First Steps in Propositional Calculus
• Exercise 2.1: Propositional Calculus: From Equivalence to Inequivalence
• Exercise 2.2: Propositional Calculus: Disjunction
• Exercise 2.3: Propositional Calculus: Conjunction
• Assignment 2.1: An Alternate Characterisation of Subtraction for the Theory of Integers
• Assignment 2.2: Propositional Calculus: An Alternate Definition of Conjunction
• Exercise 3.1: Propositional Calculus: Implication
• Homework 4.1: Propositional Calculus: Conjunction
• Homework 4.2: Propositional Calculus: Implication
• Homework 5: Leibniz’s Rule as an Axiom, Replacement Theorems
• Homework 6: Monotonicity in the Integers
• Assignment 3: An Alternate Approach to Implication
• Exercise 4.1: Leibniz as Axiom, Replacement

Structured Proofs

• Exercise 4.2: Natural Numbers and Induction
• Exercise 4.3: Implication Chains and Monotonicity
• Homework 7: Order on the Natural Numbers
• Exercise 5.1: Inequality
• Exercise 5.2: Positivity
• Exercise 5.3: Order on the Integers
• Exercise 5.4: Cancellation Properties for the Natural Numbers
• Assignment Question 4.1: Order on the Integers
• Assignment Question 4.2: Exploring Minimum and Maximum of Natural Numbers

Quantification, Predicate Logic, and Sets

• Homework 8: Substituting into Quantifications
• Homework 9 Notebook 1: Quantification Expansion
• Homework 9 Notebook 2: More Quantification Expansion
• Exercise 6.2: Even More Quantification Expansion
• Exercise 6.3: Sum Quantification in ℕ
• Exercise 6.4: Universal Quantification
• Exercise 7.2: Existential Quantification
• Homework 10: Introduction to Instantiation
• Assignment 5 Question 1: Sum Quantification in ℕ
• Assignment 5 Question 2: Universal Quantification
• Exercise 7.3: Practice with Universal and Existential Quantification in the setting of ℕ
• Assignment 6 Question 1: Maximum and Minimum on ℤ
• Assignment 6 Question 2: Practice with Universal and Existential Quantification in the setting of ℤ
• Exercise 8.1: Sets
• Exercise 8.2: Conditional
• Homework 11 Question 1: Sets
• Homework 11 Question 2: Cartesian Products
• Assignment 7 Question 1: Sets
• Assignment 7 Question 2: Quantification with Sets of Natural Numbers

Relations, Sequences, ...

• Homework 12: Relations
• Exercise 9.1: Inductive Theory of Sequences
• Exercise 9.2: Relations via Set Theory: Properties of the Basic Operators
• Exercise 9.3: Relations via Set Theory: Counterexamples for Non-Properties
• Homework 13: Relations via Set Theory: Properties of Relations
• Assignment 8 Question 1: Inductive Theory of Sequences
• Assignment 8 Question 2: Relations via Set Theory: More Properties
• Exercise 10.1: Relations via Set Theory: Yet More Properties
• Exercise 10.2: Permutations and Combinations
• Homework 14: Heterogeneous Relation Properties
• Assignment 9: Sequences
• Exercise 10.3A: M2Q2A
• Exercise 10.3B: M2Q2B
• Exercise 11.1: Abstract Relation Algebra: Starting from Inclusion, Composition, and Converse
• Homework 15 Notebook 1: Starting Abstract Relation Algebra
• Homework 15 Notebook 2: Continuing Abstract Relation Algebra with Intersection
• Exercise 12.1: Continuing Abstract Relation Algebra with Intersection
• Homework 16: More Relation-algebraic Proofs
• Exercise 12.2: Abstract Relation Algebra: Binary Union
• Exercise 12.3: Abstract Relation Algebra: Least Relations
• Exercise 12.4: Abstract Relation Algebra: Arbitrary Unions
• Assignment 10.1: Abstract Relation Algebra: Symmetric Closure
• Assignment 10.2: Abstract Relation Algebra: Reflexive-transitive Closure