CIS 682 Friendly Logics Fall 2015

Moore 212, Tu Th 5-6:30


Instructor:
Val Tannen
Levine 570
Email: val@cis.upenn.edu
Tel: +1 (215) 898-2665

The use of logical formalisms in Computer Science is dominated by a fundamental conflict: expressiveness vs. algorithmic tractability. Researchers in formal methods, programming languages, databases, artificial intelligence, etc., have studied formalisms that are reasonable compromises in this conflict:
(1) they are expressive enough for practical specifications, and
(2) there exist interesting algorithms for the automated manipulation of these specifications.
This course is about the search for such "friendly logics". We will adhere to several themes:

a) The fundamental questions of Mathematical Logic and how they led to the birth of Computability/Complexity Theory (and, arguably, contributed to the birth of Computer Science).

b) Some topics in Finite Model Theory: complexity of first-order (FO) model checking, FO definability, and the 0-1 Law for first-order logic (FOL)--- an interesting connection with probabilities.

c) Beyond FOL: the bad (the dangers of wild second-order logic (SOL)) and the good (some fragments of SOL and fixpoint extensions of FOL; some Descriptive Complexity).

d) Some Equational Logic/Rewriting (if we have time).

In addition to the content described above the class also has a specific methodological goal: to give you tools for navigating between areas and thus, for example, understand how a problem you might be facing (say) in databases in 201X has in fact been solved in (say) a formal methods article from 199Y.

No textbook: reading materials will be posted on this web page and/or will be distributed in class.

Grading will be even friendlier than the logics: a bit of homework and a short presentation to the class.
My lecture notes on computability [pdf]

"On the Unusual Effectiveness of Logic in Computer Science" [pdf] by Halpern, Harper, Immerman, Kolaitis, Vardi, and Vianu

Lecture Notes 1 [pdf]

Homework 1 [pdf]

Chronology of events related to the role of Mathematical Logic in the birth of Computer Science (according to my humble understanding) [pdf]

Lecture Notes 2 [pdf]

Lecture Notes 3 (provisional) [pdf]

Lecture Notes 4 [pdf]

Homework 2 [pdf]

Lecture Notes 5 [pdf]

_________________________________
Val Tannen (val@cis.upenn.edu)