CS576 - Fall 2019 - Topics in Automated Deduction

Course Information

Course Reading Materials

Course Structure

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:

  1. Date - Topic

    Optional comment.

    1. First assigned reading
    2. Second assigned reading
    3. Etc…

Lecture Overview

  1. 08/27 - Course Introduction

  2. 08/29 - CBRL Preliminaries

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

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

  3. 09/03 - CBRL Preliminaries

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

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

  4. 09/05 - CBRL Preliminaries

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

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

  5. 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.

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

  6. 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.

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

  7. 09/17 - Constrained Constructor Pattern Predicates/Reachability Logic

    1. Constrained Constructor Pattern Predicates - from Parameterized Intersections on pg. 17 to the end of Section 3 in CBRL
    2. Reachability Formulas and Semantics - Section 4 upto and including Lemma 3 on pg. 22 in CBRL