CS576 - Fall 2019 - Topics in Automated Deduction

Course Information

Course Reading Materials

Tools

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…

RLTool Command Overivew

Here is the command listing from rltool-lib.maude in the tool archive.

sort @QFForm@ @QFCTerm@ @NeQFCTermSet@ @Term@ @TermSet@ @ReachFormEx@ @LabelReachFormEx@ .
subsort @QFCTerm@ < @NeQFCTermSet@ .
subsort @Term@ < @TermSet@ .
op ((_))     : @Bubble@                      -> @Term@ [ctor] .
op _U_       : @TermSet@ @TermSet@           -> @TermSet@ [assoc comm ctor] .
op true      :                               -> @QFForm@ [ctor] .
op (_)=(_)   : @Bubble@ @Bubble@             -> @QFForm@ [ctor] .
op (_)=/=(_) : @Bubble@ @Bubble@             -> @QFForm@ [ctor] .
op _/\_      : @QFForm@ @QFForm@             -> @QFForm@ [prec 58 assoc comm ctor] .
op _\/_      : @QFForm@ @QFForm@             -> @QFForm@ [prec 59 assoc comm ctor] .
op (_)|_     : @Bubble@ @QFForm@             -> @QFCTerm@ [prec 60 ctor] .
op _\/_      : @NeQFCTermSet@ @NeQFCTermSet@ -> @NeQFCTermSet@ [prec 61 assoc comm ctor] .
op _=>_      : @NeQFCTermSet@ @NeQFCTermSet@ -> @ReachFormEx@ [prec 62 ctor] .
op _:_       : @Token@ @ReachFormEx@         -> @LabelReachFormEx@ [prec 63 ctor] .

sort MetaRLTLCommand .
--- module/var/backend setup
op select_.               : @Token@ -> MetaRLTLCommand [ctor] .
op select-rls_.           : @NeTokenList@ -> MetaRLTLCommand [ctor] .
op declare-vars_.         : @TermSet@ -> MetaRLTLCommand [ctor] .
op use`tool_for_on_.      : @Token@ @Token@ @Token@ -> MetaRLTLCommand [ctor] .
op use`tool_for_on_with_. : @Token@ @Token@ @Token@ @NeTokenList@ -> MetaRLTLCommand [ctor] .

--- goal/term state setup
op def-term-set_.         : @NeQFCTermSet@ -> MetaRLTLCommand [ctor] .
op add-goal_.             : @LabelReachFormEx@ -> MetaRLTLCommand [ctor] . --- add as goal and axiom
op add-goal!_.            : @LabelReachFormEx@ -> MetaRLTLCommand [ctor] . --- add as goal
op add-axiom_.            : @LabelReachFormEx@ -> MetaRLTLCommand [ctor] . --- add as axiom TODO: revisit this command
op inv_to_with_on_.       : @Token@ Qid @TermSet@ @NeQFCTermSet@ -> MetaRLTLCommand [ctor] .
op inv_to_on_.            : @Token@ Qid @NeQFCTermSet@ -> MetaRLTLCommand [ctor] .

--- finish setup
op start-proof`.          : -> MetaRLTLCommand [ctor] .

--- proof manipulation
--- apply basic proof strategy
op auto_.                 : Nat -> MetaRLTLCommand [ctor] .
op auto*`.                : -> MetaRLTLCommand [ctor] .
op auto`.                 : -> MetaRLTLCommand [ctor] .
--- delete unwanted goals
op focus_.                : NeSet{Nat} -> MetaRLTLCommand [ctor] .
op focus_.                : @Term@ -> MetaRLTLCommand [ctor] .
op focus_.                : @QFCTerm@ -> MetaRLTLCommand [ctor] .
op focus_/_.              : @QFCTerm@ @QFCTerm@ -> MetaRLTLCommand [ctor] .
--- change axioms used
op use-axioms_on_.        : @NeTokenList@ Nat -> MetaRLTLCommand  [ctor] .               --- modify goal to use circularities
op use-axioms_._on_.      : @NeTokenList@ @NeTokenList@ Nat -> MetaRLTLCommand  [ctor] . --- modify goal to use axioms/circularities
--- do case analysis a variable
op case_on_by_.           : Nat @Token@ @TermSet@ -> MetaRLTLCommand [ctor] .
op case_on_by_.           : @Term@ @Token@ @TermSet@ -> MetaRLTLCommand [ctor] .
op case_on_by_.           : @QFCTerm@ @Token@ @TermSet@ -> MetaRLTLCommand [ctor] .
--- split on a formula
op split_by_.             : Nat @QFForm@ -> MetaRLTLCommand [ctor] .
op split_by_.             : @Term@ @QFForm@ -> MetaRLTLCommand [ctor] .
op split_by_.             : @QFCTerm@ @QFForm@ -> MetaRLTLCommand [ctor] .
op replace_by_.           : Nat @QFForm@ -> MetaRLTLCommand [ctor] .
op replace_by_.           : @Term@ @QFForm@ -> MetaRLTLCommand [ctor] .
op replace_by_.           : @QFCTerm@ @QFForm@ -> MetaRLTLCommand [ctor] .
op split_by_and_.         : Nat @QFForm@ @QFForm@ -> MetaRLTLCommand [ctor] .
op split_by_and_.         : @Term@ @QFForm@ @QFForm@ -> MetaRLTLCommand [ctor] .
op split_by_and_.         : @QFCTerm@ @QFForm@ @QFForm@ -> MetaRLTLCommand [ctor] .
--- try to close a set of goals with default strategy---but do nothing if this process fails
op try-finish_.           : NeSet{Nat} -> MetaRLTLCommand [ctor] .
op try-finish_.           : @QFCTerm@ -> MetaRLTLCommand [ctor] .
op try-finish_/_.         : @QFCTerm@ @QFCTerm@ -> MetaRLTLCommand [ctor] .
--- try to subsume a goal by another
op subsume_by_.           : Nat Nat -> MetaRLTLCommand [ctor] .
--- resume from a debugging output pause
op continue`.             : -> MetaRLTLCommand [ctor] .
--- delete inactive goals
op delete-inactive`.      : -> MetaRLTLCommand [ctor] .

--- output commands
op show-goal-table`.           : -> MetaRLTLCommand [ctor] .
op show-goal-ids`.             : -> MetaRLTLCommand [ctor] .
op show-all-goal-ids`.         : -> MetaRLTLCommand [ctor] .
op show-goals_.                : NeSet{Nat} -> MetaRLTLCommand [ctor] .
op show-goals`.                : -> MetaRLTLCommand [ctor] .
op show-level_.                : Nat -> MetaRLTLCommand [ctor] .
op show-levels`.               : -> MetaRLTLCommand [ctor] .
op show-ancestors_generation_. : NeSet{Nat} Bound -> MetaRLTLCommand [ctor] .
op show-narrowings_.           : Nat -> MetaRLTLCommand [ctor] .
op show-maude-cmd_on_.         : @Token@ Nat -> MetaRLTLCommand [ctor] .

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
  8. 09/19 - Reachability Logic

    1. Specifying (Co-)Invariants/Relationship to other logics - From pg. 22, after Lemma 3 upto end of pg. 28 excluding Section 5 in CBRL
  9. 09/24 - Reachability Logic Inference System

    1. RL Inference System - Starting from Section 5 on pg. 28 upto but excluding Section 5.2 on pg. 37 in CBRL
  10. 09/26 - Reachability Logic Inference System & Examples

    Note that we will cover the first assigned reading quickly since it was already assigned previously.

    1. RL Inference System - Reread from the last paragraph on proof trees on pg. 33 upto and excluding Section 5.2 on pg. 37 in CBRL
    2. RL Inference System Examples - Sections 5.2 and 5.3 in CBRL
  11. 10/01 - Reachability Logic Tool Tutorial

    No readings, but see tool download link. In the tool archive, there are two parital proofs or you to complete: tests/systems/bank-account.maude and tests/systems/imp-mul.maude. They correspond to two rewrite systems: systems/bank-account.maude and systems/imp.maude. They both require either case or split commands.

  12. 10/03 - Reachability Logic Tool Tutorial (Continued)

    No readings.

  13. 10/08 - Reachability Logic Tool Tutorial (Continued) and Project Discussions

    Please begin to consider if you would like to work on verifying the ABP or else verify simple programs in an imperative programming language like the one in the reading.

    1. Sections 4 and 5 on verifying the Alternating Bit Protocol (ABP) in this paper
    2. Chapter 5, also on verifying the ABP, in Camilo Rocha’s Thesis
    3. The programming language semantics specified in systems/imp.maude in the tool archive