McMaster University
Logic and Discrete Mathematics in Software Engineering

CAS 701 — Fall 2007

Presentations

14 November:

• Explain what group and ring homomorphisms are.
• Give a quick introduction to category theory.
• Structured Specifications in CASL, Part 1
• Structured Specifications in CASL, Part 2

19 November:

• LTL Syntax and Semantics, Part 1, Part 2
• LTL Specifications and Model Checking, Part 1
• LTL Specifications and Model Checking, Part 2

• [Huth, Ryan] Chapter 3
• E. A. Emerson, Temporal and Modal Logic. In Handbook of Theoretical Computer Science, vol. B. Elsevier Science Publishers B.V., 1990, pp. 995–1072

21 November:

• CTL Syntax and Semantics, Part 1
• CTL Syntax and Semantics, Part 2
• CTL* ([Huth, Ryan] Section 3.5)
• Decidability and Complexity of Different Temporal Logics

26 November:

• Term Rewriting Basics, Part 1, Part 2

See also the Rewriting home page and the Wikipedia rewriting page

• Present the Knuth-Bendix completion procedure for transforming a finite set of equations into a “well-behaved” rewriting system.
• Explain Lindenmayer systems and show some nice examples. ; examples and tool: .tar.bz2

28 November:

• Present Church's lambda calculus.
• Present and explain arithmetic with Church numerals
• Present the simply-typed lambda calculus.
• Present the higher-order logic HOL.

3 December:

• Present a sound and complete resolution proof system for first-order logic. Explain why proof systems of this kind are employed in automated theorem provers like Otter.
• Context-Free Graph Grammars (Hyperedge Replacement Grammars)
• Double-Pushout Graph Rewriting