Scheme software is required to run the .scm files in this section.
This calendar shows the weekly schedule for the course, which usually includes three lecture and group problem solving sessions per week. This calendar provides links to course notes, problem sets, and other relevant resources. These materials are also provided separately in the readings, assignments, and tools sections of this course.
Week 1
Wednesday (First day of class)
Week 2
Readings

Notes 1: Proving Arithmetic Equations, pp. 1–6 (PDF)
Assignments
Monday

Diagnostic Questionnaire (PDF) and Solutions (PDF)
Wednesday
Friday
Week 3
Readings

Notes 1: Proving Arithmetic Equations, final sections (PDF)
Wednesday
Friday

Exercise: Convert a tree proof to a substitution proof (PDF)

Scheme code (SCM) for the conversion

Arithmetic inequalities

Pattern matcher match.scm (SCM)
Week 4
Readings

Pattern matcher match.scm (SCM)

Patternmatch based procedure proofmatch.scm (SCM) for converting a sequenceofequations proof into a tree proof

Notes 2: Substitution into Arithmetic Expressions (PDF)

Also, from last week, see Scheme code for converting a tree proof to a substitution proof (SCM)
Monday

Structural induction proof of the Substitution Lemma and Soundness of Substitution Proofs (see Notes 2: Substitution into Arithmetic Expressions (PDF))

Intro to pattern matching, with patternmatch based procedure proofmatch.scm (SCM) for converting a sequenceofequations proof into a tree proof
Wednesday
Friday
Week 5
Readings

Notes 3: A Scheme Substitution Model, Sections 1–6 (pp. 1–14) (PDF)

Monday

Bring your laptop loaded with the files for running the Substitution Model

Observe the submodel running on expressions in testsubmodel.scm (SCM)
Wednesday
Friday

Further example file for Substitution Model evaluation politician.scm (SCM)
Week 6
Readings

Notes 4: Term Models (PDF)
Assignments

Due on Monday of Week 7: Problems 1–3 in Notes 4: Term Models (PDF)
Monday
Wednesday
Friday
Week 7
Monday
Wednesday
Friday
Week 8
Assignments

Due on Monday of Week 10: Problem Set 1 (PDF)
Monday
Wednesday
Friday
Week 9
Monday
Week 10
Assignments

Due at the end of Week 10: Problem 18 from Notes 5: Scheme Computability, Part I (PDF)
Monday
Wednesday

Notes 5: Scheme Computability, Part I (PDF)
Friday
Week 11
Wednesday

Notes 7: Counter Machines (PDF)

Notes 8: Semigroup Word Problems (PDF)

Notes 9: 1storder Theory of Concatenation (PDF)
Friday

Notes 3: Scheme Substitution Model (PDF)

Notes 5: Scheme Computability, Part I (PDF)

Notes 6: Scheme Computability, Part II (PDF)
Week 12
Assignments
Monday
Wednesday

Halting Problem for 2Counter Machines
≤_{m} Th(∑*, ·)
≤_{m} Th({1,2}*, ·)
≤_{m} Th(N,+,×, ≦)
≡_{m} Th(Z,+,, ×, ≦),
where Th(M) denotes the 1storder formulas valid in model M
Friday

Complete proof that [2CM Halting Problem ≤_{m} Th(∑*, ·)]

Observe that Halts reduces to the set of closed formulas of the form ∃z.G where all quantifiers in G range over subwords of z
Week 13
Assignments

Due at the beginning of this week: Course project (PDF) proposals
Monday
Wednesday
Friday

Diophantine Predicates closed under ∧, ∨, ∃, but not ¬ (negation)

A Diophantine polynomial whose nonnegative range is the nonprimes
Week 14
Assignments

Due at the end of this week: Term project (PDF)
Monday

Excerpt: pp. 174–181 on Undecidability of Exponential Diophantine Polynomials, from Jones, Neil D. "Computability and Complexity: from a Programming Perspective," MIT Press, c. 1997, 466pp.
Wednesday (Last class)