Logic and Discrete Mathematics in Software Engineering
CAS 701 — Fall 2007
- 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
- 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
- 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
- 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