BU GRS CS 792: 
Topics in Logic and Formal Methods in Computer Science

Spring 2006

HOME PAGE

There is a variety of logics for formal reasoning in many different domains of computer science. Apart from classical first-order logic, most commonly taught in a standard course in mathematical logic, several others have a more direct bearing on computer science.  Among the latter are intuitionistic logic, modal logic, temporal logic, dynamic logic, Hoare logic, specification logic, separation logic, non-monotonic logic, affine logic, linear logic, and several variations of each of the preceding -- to name a few that have been invented by computer scientists in recent years, or have been the object of renewed interest because of applications in computer science.

During the Spring 2006 semester we will cover topics in modal logic and linear logic, in approximate equal parts. Time permitting, also based on audience interests, we may have brief introductions to separation logic and/or Hoare logic. Material will be drawn from two recent texts:

1. "Modal Logic" by P. Blackburn, M. de Rijke and Y. Venema -- paperback book available at Amazon.com for $39.97.
2. "Linear Logic" by Frank Pfenning -- lecture notes available in the CS Department office for about $10.00.

Students will take turns in making weekly presentations, drawn from the reading material, based on which they will get credit for the course.

• Meeting time and place: Thursday at 3:30 in Room MCS 180
• Instructor's email address: kfoury@cs.bu.edu
• Group email address: pl-reading-group@types.bu.edu

• Jan 19:  Organizational meeting.
  
• Jan 26:  Sections 2.1- 2.5 in notes on "Linear Logic", presented by Kevin.
  
• Feb 02:  Section 2.6 presented by Kevin. Sections 3.1 - 3.4 presented by Yarom.
  
• Feb 09:  Sections 3.4-3.5 presented by Yarom, Sections 6.1-6.2 presented by Joe.
  
• Feb 16:  Sections 6.3-6.5 presented by Joe, Section 7.1 presented by Likai.
  
• Feb 23:  Section 7.2 in "Linear Logic" presented by Likai, Section 1.2 in "Modal Logic" presented by Michael.
  
• Mar 02:   Sections 1.3-1.4 in "Modal Logic" presented by Michael. Section 2.1 in "Modal Logic" presented by Gabriel.
  
• Mar 16:   Sections 2.2-2.4 in "Modal Logic" presented by Gabriel.
  
• Mar 23:   Sections 3.1-3.2 in "Modal Logic" presented by Kevin.
  
• Mar 30:   Sections 3.3-3.4 in "Modal Logic" presented by Yarom.
  
• Apr 06:   NO SEMINAR.
• Apr 13:   Sections 4.1-4.2 in "Modal Logic" presented by Joe.
  
• Apr 18:   Exercise solving session.
• Apr 20:   Sections 4.3-4.4 in "Modal Logic" presented by Likai.
  
• Apr 27:

• Feb 09-Feb 16: In the notes on "Linear Logic",
  • Exercises 2.1, 2.2, 2.3, and 2.8, page 41 -- the last of these 4 exercises is a little repetitive, so do it for half of the 14 propositions listed on page 42.
  • Exercise 3.2, page 66. The non-admissibility proof may be tricky, also omit the last paragraph in this exercise.
• Feb 16-Feb 23: In the notes on "Linear Logic", the following supplement Sections 6.3 and 6.4:
  • Exercise 6.2, page 136. Do as much as you can, as it relates well to lazy functional programming.
  • Exercises 6.4 and 6.8, pages 136-137. Should be straightforward.
  • Exercise 6.13, page 138. I did not try it, but would be interested in seeing a solution.
• Feb 23-Mar 02: In the book "Modal Logic":
  • Exercises 1.2.2 and 1.2.3 page 16.
  • Exercises 1.3.3 and 1.3.5 page 27.
• Mar 02-Mar 16: In the book "Modal Logic":
  • Exercises 1.3.2 page 27. Exercises in deciding whether particular modal formulas are valid in two particular frames.
  • Exercises 2.1.3 and 2.1.5 page 63. Exercises showing differences between "homomorphism", "strong homomorphism", "isomorphism", and "bounded homomorphism", among other things.
  • Exercise 2.2.1 page 71. Peeking ahead, this is an easy exercise on "bisimulation".
• Mar 16-Mar 23: In the book "Modal Logic":
  • Exercises 2.2.4 and 2.2.5 page 72. These are "negative" results, showing that some predicate or operator is not definable by the logic. "Negative" results are typically more difficult to establish.
• Mar 23-Mar 30: In the book "Modal Logic":
  • Exercise 2.2.5 page 72, once more (not finished last time).
  • Exercise 3.1.1 page 130 and 3.2.1 page 137. Both are non-trivial and the second appears substantial.
• Mar 30-Apr 13: In the book "Modal Logic":
  • Exercise 3.1.1 page 130 and 3.2.1 page 137 (of previous week).
  • Exercise 3.3.2 on page 142, and Exercise 3.3.4 on page 143.
• Apr 13-Apr 20: Do as many omitted exercises as possible from preceding weeks.
• Apr 20-Apr 27:

• Basic Concepts: Sections 1.2-1.6.
• Models: Sections 2.1-2.4.
• Frames: Sections 3.1-3.4.
• Completeness: Sections 4.1-4.4.
• Computability and Complexity: Selection of sections from Chapter 6.
• Special Topics: Selection of sections from Chapter 7.

Maintained by Assaf Kfoury
Created:  05.12.28
Modified: 06.04.16