- Instructor: JosÃ© Meseguer
- Time: Tuesday/Thursday 3:30PM - 4:45PM
- Location: Siebel Center Room 1131
- Office Hours: TBD
- Course Piazza Forum

- A Constructor-Based Reachability Logic for Rewrite Theories (CBRL)
- CS476 Lecture 2 Slides
- CS476 Lecture 3 Slides
- CS476 Lecture 9 Slides
- CS476 Lecture 4 Slides
- CS476 Lecture 5 Slides
- CS476 Lecture 7 Slides
- CS476 Lecture 14 Slides
- CS476 Lecture 15 Slides
- CS476 Lecture 16 Slides

In every lecture, we will discuss a particular topic (see the list below for a rough overview). For some lectures, there will be assigned reading materials. Unless otherwise specified, assigned readings should be completed BEFORE attending the given lecture.

The lecture overview list has the following format:

Date - Topic

Optional comment.

- First assigned reading
- Second assigned reading
- Etcâ€¦

08/27 - Course Introduction

08/29 - CBRL Preliminaries

Readings cover material in CBRL Preliminaries upto and including Theorem 1 on pg. 7.

- Many-sorted/Order-sorted Signatures, Equational Theories, Maude Modules: pgs. 2-19 in CS476 Lecture 2 Slides
- Many-sorted/Order-sorted Algebras: pgs. 2-16 in CS 476 Lecture 3 Slides
- Term Algebras, Substitutions, Equations: pgs. 17-30 in CS476 Lecture 3 Slides
- Many-sorted/Order-sorted Homomorphisms: pgs. 2-9 in CS476 Lecture 9 Slides
- The Initiality Theorem (Theorem 1 in CBRL): pgs. 10-12 in CS476 Lecture 9 Slides

09/03 - CBRL Preliminaries

Readings cover material in CBRL Preliminaries upto middle of pg. 10 (excluding the defn. of rewrite theories).

- Term Rewriting, Equational Logic, Rewriting Modulo Axioms: all of CS476 Lecture 4 Slides
- Executability Conditions, Canonical Term Algebras, Sufficient Completeness: all of CS 476 Lecture 5 Slides
- Unification: pgs. 3-18 in CS476 Lecture 7 Slides

09/05 - CBRL Preliminaries

Readings cover material in CBRL Preliminaries upto end of pg. 11.

- Rewrite Theory and Examples: pgs. 5-37 of CS476 Lecture 14 Slides and pgs. 2-17 of CS476 Lecture 15 Slides
- Coherence of Rules w.r.t. Oriented Equations Modulo Axioms: pgs. 10-14 of CS476 Lecture 16 Slides

09/10 - CBRL Preliminaries

Since the reading for this lecture is quite dense, please complete the following exercise BEFORE the lecture:

In subsection

*Variants in a Nutshell*, several examples of variants are presented. Check that these examples are indeed variants according to the definition. Then, develop some other examples of variants for yourself using some other set of convergent equations of your choice.This lecture will provide additional examples and go into greater depth on the topcis: narrowing, variant narrowing, variant unification, and variant satisfiability of quantifier-free formulas.

- Variants: section
*Variants in a Nutshell*of CBRL on pg. 12 excluding*A Running Example*

- Variants: section
09/12 - Constrained Constructor Pattern Predicates

Readings from now on are based on a revised version of CBRL available for download now; please redownload if you have an older copy.

- Constrained Constructor Pattern Predicates - Section 3 of CBRL upto but excluding
*Parameterized Intersections*on pg. 17

- Constrained Constructor Pattern Predicates - Section 3 of CBRL upto but excluding
09/17 - Constrained Constructor Pattern Predicates/Reachability Logic