CIS 682 Friendly Logics Fall 2015
Moore 212, Tu Th 5-6:30
- Val Tannen
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
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
"On the Unusual Effectiveness of Logic in Computer Science"
[pdf] by Halpern, Harper, Immerman, Kolaitis, Vardi, and Vianu
Lecture Notes 1
Chronology of events related to the role of Mathematical Logic
in the birth of Computer Science (according to my humble understanding)
Lecture Notes 2
Lecture Notes 3 (provisional)
Lecture Notes 4
Lecture Notes 5
Val Tannen (firstname.lastname@example.org)