CalcCheck Instances for COMPSCI 2LC3, Fall 2021

(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: 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
• Homework 2: Substitution
• Exercise 2.1: An Equational Theory of Integers
• Exercise 2.2: Substitution
• Exercise 2.3: Re-Proving the Equational Theory of Integers with Rigid Matching
• Exercise 2.4: Re-Proving the Integer Theorems without Automatic Associativity and Symmetry
• Exercise 2.5: Re-Proving the Integer Theorems for Masochists
• Homework 3 Notebook 1: Correctness of Assignment Commands
• Homework 3 Notebook 2: First Steps in Propositional Calculus
• Exercise 2.6: Assignment Commands with Boolean Variables
• Exercise 2.7: Propositional Calculus: From Equivalence to Inequivalence
• Exercise 3.1: Knights and Knaves
• Exercise 3.2: Propositional Calculus: Disjunction
• Exercise 3.3: Propositional Calculus: Conjunction
• Homework 4: Conjunction
• Homework 5 Notebook 1: Natural Numbers and Induction
• Assignment 1 Notebook 1: Proving Theorems in the Equational Theory of Integers
• Assignment 1 Notebook 2: An Alternative Characterisation of Subtraction of Integers
• Assignment 1 Notebook 3: Assignment Commands with Boolean Variables
• Exercise 3.4: Implication
• Exercise 3.5: Natural Numbers and Induction: Addition and Multiplication
• Homework 5 Notebook 2: Implication
• Reference Notebook 3.1: Inequality
• Homework 6 Notebook 1: Leibniz as Axiom, Replacement
• Homework 6 Notebook 2: Quantification Expansion 1
• Homework 6 Notebook 3: Quantification Expansion 2
• Assignment 2 Notebook 1: Propositional Calculus
• Assignment 2 Notebook 2: More About the Natural Numbers
• Homework 7: Monotonicity
• Exercise 4.1: Monus Subtraction
• Exercise 4.2: Leibniz as Axiom, Replacement
• Exercise 4.3: Monotonicity
• Exercise 4.4: Assuming the Antecedent
• Exercise 4.5: Quantification Expansion 3
• Extra Exercise 4.6: Order and Strict-order on ℕ
• Homework 8: Reversed Command Correctness Notation
• Extra Exercise 4.7: Predecessors in ℕ

Quantification and Predicate Logic

• Homework 9: Substituting into Quantifications
• Exercise 5.1: Simple Proofs `By cases` on ℕ
• Exercise 5.2: Manipulating Ranges in ℕ
• Exercise 5.3: Conditional Commands
• Exercise 5.4: Positivity
• Exercise 5.5: Partial Solutions to Exercise 5.4: Positivity
• Exercise 5.6: Order on Integers
• Homework 10: Introduction to Instantiation
• Assignment 3 Notebook 1: Minima and Maxima in ℕ
• Assignment 3 Notebook 2: Replacement
• Assignment 3 Notebook 3: Monotonicity
• Reference Notebook 6.1: Sum Quantification in ℕ
• Reference Notebook 6.2: Product Quantification in ℕ
• Reference Notebook 6.3: Universal Quantification
• Reference Notebook 6.4: Existential Quantification
• Homework 11 Notebook 1: Practice with Universal and Existential Quantification in the Setting of ℕ
• Homework 11 Notebook 2: Introduction to Sequences
• Exercise 6.1: Practice with Universal and Existential Quantification in the Setting of ℕ
• Exercise 6.2: Sequences
• Assignment 4 Notebook 1: Proofs about Sum Quantification on ℕ
• Assignment 4 Notebook 2: Practice with ∀ and ∃ in the Setting of ℤ
• Assignment 4 Notebook 3: Correctness of `rev`
• Homework 12: Sets
• Exercise 7.1: Indirect Equality, Maximum, and Minimum on Integers
• Exercise 7.2: “Mixed Monotonicity”
• Exercise 7.3: Set Theory
• Exercise 7.4: Pairs and Cartesian Products
• Homework 13: Using the Induction Principle for `_+ 1` in ℕ
• Reference Notebook 7.1: Set Theory
• Assignment 5: Set Theory

Relations, Graphs, etc.

• Reference Notebook 8.1: Relations
• Homework 14: Relations via Set Theory I
• Exercise 8: Relations via Set Theory II
• Homework 15: Correctness of `while` Loops
• Exercise 9.1: Properties of Relations Shown as Simple Graphs
• Exercise 9.2: Correctness of `while` Loops
• Exercise 9.3: Relations via Set Theory III
• Reference Notebook 9.1: Properties of the Basic Relation Operations
• Reference Notebook 9.2: Operators Combining Sets and Relations
• Exercise 9.4: Operators Combining Sets and Relations
• Reference Notebook 10.1: Abstract Relation Algebra: Starting from Inclusion and Composition
• Reference Notebook 10.2: Abstract Relation Algebra: Continuing with Converse after Inclusion and Composition
• Exercise 10.1: Starting Abstract Relation Algebra from Inclusion, Composition, and Identity
• Exercise 10.2: Abstract Relation Algebra: Continuing with Converse after Inclusion and Composition
• Exercise 10.3: Continuing Abstract Relation Algebra with Intersection
• Exercise 10.4: Binary Trees
• Reference Notebook 11.1: Continuing Abstract Relation Algebra with Intersection
• Reference Notebook 11.2: Abstract Relation Algebra: Binary Union
• Reference Notebook 11.3: Abstract Relation Algebra: Least Relations
• Reference Notebook 11.4: Abstract Relation Algebra: Arbitrary Unions
• Assignment 6 Notebook 1: Heterogeneous Relation Properties
• Assignment 6 Notebook 2: Partial-Function Application
• Assignment 6 Notebook 3: Abstract Relation Algebra: More Union Material
• Assignment 6 Notebook 4: Correctness of `while` Loops
• Exercise 11.1: More Relation-algebraic Proofs
• Exercise 11.2: Abstract Relation Algebra: Reflexive-transitive Closure
• Homework 16: Getting Started wityh Frama-C
• Reference Notebook 12.1: Abstract Kleene Algebra
• Exercise 12.1: Abstract Kleene Algebra
• Exercise 12.2: Bags
• Exercise 12.3: Correctness of array modifications
• Assignment 7: Correctness of Simple RTC Calculation
• Exercise 13.1: Relational Semantics of Imperative Programs