This document discusses the fundamental role that logic has played in the development of computer science over the past 50 years. It provides examples of how logic has provided a unifying foundational framework and modeling tool for areas like machine architecture, programming languages, databases, and more. The document then traces the historical developments in logic that enabled these contributions, including Boolean logic, first-order logic, automata theory, and analyses of computational complexity. Overall, it outlines how logic has become central to computer science in a way analogous to the role of calculus in traditional engineering fields.
2. Logic in Computer Science
During the past 鍖fty years there has been extensive, continuous,
and growing interaction between logic and computer science. In
many respects, logic provides computer science with both a unifying
foundational framework and a tool for modeling computational
systems. In fact, logic has been called the calculus of computer
science. The argument is that logic plays a fundamental role in
computer science, similar to that played by calculus in the physical
sciences and traditional engineering disciplines. Indeed, logic plays
an important role in areas of computer science as disparate as
machine architecture, computer-aided design, programming languages,
databases, arti鍖cial intelligence, algorithms, and computability and
complexity.
1
3. Why on Earth?
Basic Question: What on earth does an obscure, old intellectual discipline
have to do with the youngest intellectual discipline?
M. Davis (1988): In鍖uences of Mathematical Logic on Computer Science:
When I was a student, even the topologists regarded mathematical logicians
as living in outer space. Today the connections between logic and computers
are a matter of engineering practice at every level of computer organization.
Question: Why on earth?
2
4. The Fundamental Method of Physical Sciences
The basic method of physical science:
Construct a mathematical model for physical reality.
Analyze mathematical model.
Compare analysis results with physical reality.
Basic Question: What is a mathematical model?
3
5. What is The Language of Mathematics?
Friedrich Ludwig Gottlob Frege, Begri鍖sschrift, 1879: a universal
mathematical language 鍖rst-order logic logicism
Objects, e.g., 2
Predicates (relationships), e.g., 2 < 3
Operations (functions), e.g., 2 + 3
Boolean operations, e.g., and (), or (), implies ()
Quanti鍖ers, e.g., for all (), exists ()
4
7. First-Order Logic
A formalism for specifying properties of mathematical structures, such as
graphs, partial orders, groups, rings, 鍖elds, . . .
Mathematical Structure: [Tarski, 1933]
A = (D, R1, . . . , Rk, f1, . . . , fl),
D is a non-empty set universe
Ri is an m-ary relation on A, for some m (that is, Ri Am
)
fj is an n-ary function on A, for some n (that is, fi : An
D)
6
8. Examples
Graph: G = (V, E)
V : nodes
E V 2
: edges
(x)(y)E(x, y)
Group: G = (V, 揃)
V : elements
揃 : V 2
V : product
(x)(y)x 揃 y = y 揃 x
7
9. First-Order Logic on Graphs
Syntax:
First-order variables: x, y, z, . . . (range over nodes)
Atomic formulas: E(x, y), x = y
Formulas: Atomic Formulas + Boolean Connectives + First-Order
Quanti鍖ers x, x, . . .
8
10. Examples:
node x has at least two distinct neighbors
(y)(z)(測(y = z) E(x, y) E(x, z))
Concept: x is free in the above formula, which expresses a property of
nodes. Truth de鍖nition requires a binding 留. G |=留 (x)
each node has at least two distinct neighbors
(x)(y)(z)(測(y = z) E(x, y) E(x, z))
Concept: The above is a sentence, that is, a formula with no free
variables; it expresses a property of graphs. G |=
9
11. Russells Letter
A letter from Russell to Frege, June 16, 1902:
I 鍖nd myself in agreement with you in all essentials . . . I 鍖nd in your
work discussions, distinctions, and de鍖nitions that one seeks in vain
in the work of other logicians . . . There is just one point where I have
encountered a di鍖culty.
Appendix to Freges 1903 volume:
There is nothing worse that can happen to a scientist than to have
the foundation collapse just as the work is 鍖nished. I have been placed
in this position by a letter from Mr. Bertrand Russell.
10
12. Hilberts Program
Hilberts Program (1922-1930): Formalize mathematics and establish
that:
Mathematics is consistent: a mathematical statement and its negation
cannot ever both be proved.
Mathematics is complete: all true mathematical statements can be
proved.
Mathematics is decidable: there is a mechanical way to determine
whether a given mathematical statement is true or false.
11
13. The Demise of Hilberts Program
G即odel (1930-3):
Incompleteness of ordinary arithmetic There is no systematic way of
resolving all mathematical questions.
Impossibility of proving consistency of mathematics
G即odel (1930): This sentence is not provable.
Church and Turing (1936):
Unsolvability of 鍖rst-order logic:
The set of valid 鍖rst-order sentences is not computable.
12
14. Entscheidungsproblem
Entscheidungsproblem (The Decision Problem) [Hilbert-Ackermann,
1928]: Decide if a given 鍖rst-order sentence is valid (dually, satis鍖able).
Church-Turing Theorem, 1936: The Decision Problem is unsolvable.
Turing, 1936:
De鍖ned computability in terms of Turing machines (TMs)
Proved that the termination problem for TMs is unsolvable (this
machine terminates i鍖 it does not terminate)
Reduced termination to Entscheidungsproblem.
13
15. Mathematical Logic 1936
Logic as Foundations of Mathematics:
Incomplete (example: Continuum Hypothesis)
Cannot prove its own consistency
Unsolvable decision problem
Can we get some positive results?
Focus on special cases!
14
16. The Fragment-Classi鍖cation Project
Idea: Identify decidable quanti鍖cational fragments of 鍖rst-order logic
(1915-1983)
Bernays-Sch即on鍖nkel Class (
)
Ackermann Class (
)
G即odel Class (w/o =) (
)
Outcome: Very weak classes! What good is 鍖rst-order logic?
15
17. Logic of Integer Addition
Integer Addition:
Domain: N (natural numbers)
Dyadic predicate:
Addition function: +
y = 2x: y = x + x
x = 0: (y)(x y)
x = 1: x = 0 (y)(y = 0 x y)
y = x + 1: (z)(z = 1 y = x + z)
Bottom Line: Theory of Integer Addition can express Integer
Programming (integer inequalities) and much more.
16
18. Presburger Arithmetics
Moj卒zesz Presburger, 1929:
Sound and complete axiomatization of integer addition
Decidability: There exists an algorithm that decides whether a given
鍖rst-order sentence in integer-addition theory is true or false.
Decidability is shown using quanti鍖er elimination, supplemented by
reasoning about arithmetical congruences.
Decidability can also be shown using automata-theoretic techniques.
17
19. Complexity of Presburger Arithmetics
Complexity Bounds:
Oppen, 1978: TIME(222poly
) upper bound
Fischer&Rabin, 1974: TIME(22lin
) lower bound
Rabin, 1974: Theoretical Impediments to Arti鍖cial Intelligence: the
complexity results point to a need for a careful examination of the goals
and methods in AI.
18
20. Monadic Logic
Monadic Class: First-order logic with monadic predicates captures
syllogisms.
(x)P(x), (x)(P(x) Q(x)) |= (x)Q(x)
[L即owenheim, 1915]: The Monadic Class is
decidable.
Proof: Bounded-model property if a sentence
is satis鍖able, it is satis鍖able in a structure of
bounded size.
Proof technique: quanti鍖er elimination.
19
21. Finite Words Nondeterministic Finite Automata, I
A = (裡, S, S0, , F)
Alphabet: 裡
States: S
Initial states: S0 S
Nondeterministic transition function:
: S 裡 2S
Accepting states: F S
20
22. Finite Words Nondeterministic Finite Automata, II
Input word: a0, a1, . . . , an1
Run: s0, s1, . . . , sn
s0 S0
si+1 (si, ai) for i 0
Acceptance: sn F
Recognition: L(A) words accepted by A.
Example: -
6
蔵 臓
0
1-
0
6
蔵 臓
1
ends with 1s
Fact: NFAs de鍖ne the class Reg of regular languages.
21
23. Logic of Finite Words
View 鍖nite word w = a0, . . . , an1 over alphabet
裡 as a mathematical structure:
Domain: 0, . . . , n 1
Dyadic predicate:
Monadic predicates: {Pa : a 裡}
Monadic Second-Order Logic (MSO):
Monadic atomic formulas: Pa(x) (a 裡)
Dyadic atomic formulas: x y
Set quanti鍖ers: P, P
Example: (x)((y)(測(x y)) P1(x)) last letter is 1.
22
24. Automata and Logic
Theorem [B即uchi, Elgot, Trakhtenbrot, 1957-8
(independently)]: MSO NFA
Both MSO and NFA de鍖ne the class Reg.
Proof: E鍖ective
From NFA to MSO (A A)
From MSO to NFA ( A)
23
25. NFA Nonemptiness
Nonemptiness: L(A) =
Nonemptiness Problem: Decide if given A is nonempty.
Directed Graph GA = (S, E) of NFA A =
(裡, S, S0, , F):
Nodes: S
Edges: E = {(s, t) : t (s, a) for some a
裡}
Lemma: A is nonempty i鍖 there is a path in GA from S0 to F.
Decidable in time linear in size of A, using breadth-鍖rst search or
depth-鍖rst search.
24
26. MSO Satis鍖ability Finite Words
Satis鍖ability: models() =
Satis鍖ability Problem: Decide if given is satis鍖able.
Lemma: is satis鍖able i鍖 A is nonnempty.
Corollary: MSO satis鍖ability is decidable.
Translate to A.
Check nonemptiness of A.
25
27. Complexity Barrier
Computational Complexity:
Naive Upper Bound: Nonelementary Growth
2揃揃揃2n
(tower of height O(n))
Lower Bound [Stockmeyer, 1974]: Satis鍖ability of FO over 鍖nite words
is nonelementary (no bounded-height tower).
26
29. Booles Symbolic Logic
Booles insight: Aristotles syllogisms are about classes of objects, which
can be treated algebraically.
If an adjective, as good, is employed as a term of description, let us
represent by a letter, as y, all things to which the description good
is applicable, i.e., all good things, or the class of good things. Let
it further be agreed that by the combination xy shall be represented
that class of things to which the name or description represented by
x and y are simultaneously applicable. Thus, if x alone stands for
white things and y for sheep, let xy stand for white sheep.
28
30. Boolean Satis鍖ability
Boolean Satis鍖ability (SAT); Given a Boolean expression, using and
() or, () and not (測), is there a satisfying solution (an assignment
of 0s and 1s to the variables that makes the expression equal 1)?
Example:
(測x1 x2 x3) (測x2 測x3 x4) (x3 x1 x4)
Solution: x1 = 0, x2 = 0, x3 = 1, x4 = 1
29
31. Complexity of Boolean Reasoning
History:
William Stanley Jevons, 1835-1882: I have given much attention,
therefore, to lessening both the manual and mental labour of the process,
and I shall describe several devices which may be adopted for saving trouble
and risk of mistake.
Ernst Schr即oder, 1841-1902: Getting a handle on the consequences
of any premises, or at least the fastest method for obtaining these
consequences, seems to me to be one of the noblest, if not the ultimate
goal of mathematics and logic.
1950-60s: Perebor: Futile e鍖ort to show hardness of search
problems.
Cook, 1971, Levin, 1973: Boolean Satis鍖ability is NP-complete.
30
32. NP-Completeness
Complexity Class NP: problems where solutions can be checked in
polynomial time.
Factoring numbers
Hamiltonian Cycle
Signi鍖cance: Tens of thousands of optimization problems are in NP!!!
CAD, 鍖ight scheduling, chip layout, protein folding, . . .
NP-complete: Hardest problems in NP.
If one NP-complete problem can be solved in polynomial time, then
all NP-complete problems can be solved in polynomial time.
31
33. Is P = NP?
S. Aaronson, MIT: If P = NP, then the world would be a profoundly
di鍖erent place than we usually assume it to be. There would be no special
value in creative leaps, no fundamental gap between solving a problem and
recognizing the solution once it is found. Everyone who could appreciate
a symphony would be Mozart; everyone who could follow a step-by-step
argument would be Gauss.
Common Belief: Boolean SAT cannot be solved in polynomial time.
32
34. Program Veri鍖cation
The Dream Hoare, 1969: When the correctness of a program, its
compiler, and the hardware of the computer have all been established with
mathematical certainty, it will be possible to place great reliance on the
results of the program.
The Nightmare De Millo, Lipton, and Perlis, 1979: We believe that . . .
program veri鍖cation is bound to fail. We cant see how its going to be able
to a鍖ect anyones con鍖dence about programs.
Basic Argument: Acceptance of proof is a social process!
33
35. Logic in Computer Science: c. 1980
Status: Logic in CS is not too useful!
Unsolvable termination problem.
First-order logic is undecidable.
The decidable fragments are either too weak or too intractable.
Even Boolean logic is intractable.
Program veri鍖cation is hopeless.
34
36. Post 1980: From Irrelevance to Relevance
A Logical Revolution:
Relational databases
Boolean reasoning
Model checking
Termination checking
. . .
35
37. From Model Theory to Relational Databases
A sentence is either true or false on a given graph G. In particular,
sentences specify classes of graphs: models() = {G : G |= }
Model Theory: Logic provides a metatheory for mathematical modeling.
E.F. Codd, 1970: Formulas (x1, . . . , xk) de鍖ne queries:
(G) = { 留(x1), . . . , 留(xk) : G |=留 (x1, . . . , xk)}
Example: (y)(z)(測(y = z) E(x, y) E(x, z)) List nodes that
have at least two distinct neighbors
Turing Awards: Codd, 1981, Stonebraker, 2014
Relational Databases: $30B+ industry
36
38. Relational Databases
Codds Two Fundamental Ideas:
Tables are relations: a row in a table is just a tuple in a relation; order
of rows/tuples does not matter!
Formulas are queries: they speci鍖ed the what rather then the how
declarative programming!
Reduction to Practice:
System R, IBM, 1976
Ingress, UC Berkeley, 1976
Oracle, Relational Software, 1979
DB2, IBM, 1982
37
39. Algorithmic Problems in First-Order Logic
Satis鍖ability Problem: Given a 鍖rst-order formula , is there a graph G
and binding 留, such that G |=留 ?
Truth-Evaluation Problem: Given a 鍖rst-order formula (x1, . . . , xk), a
鍖nite graph G, and a binding 留, does G |=留 (x1, . . . , xk)?
Contrast:
Satis鍖ability is undecidable [Church, Turing 1936]
Truth evaluation, which is query evaluation, is decidable.
38
40. Algorithmic Boolean Reasoning: Early History
Newell, Shaw, and Simon, 1955: Logic Theorist
Davis and Putnam, 1958: Computational Methods in The
Propositional calculus, unpublished report to the NSA
Davis and Putnam, JACM 1960: A Computing procedure for
quanti鍖cation theory
Davis, Logemman, and Loveland, CACM 1962: A machine program
for theorem proving
DPLL Method: Propositional Satis鍖ability Test
Convert formula to conjunctive normal form (CNF)
Backtracking search for satisfying truth assignment
Unit-clause preference
39
41. Modern SAT Solving
CDCL = con鍖ict-driven clause learning
Backjumping
Smart unit-clause preference
Con鍖ict-driven clause learning
Smart choice heuristic (brainiac vs speed demon)
Restarts
Key Tools: GRASP, 1996; Cha鍖, 2001
Current capacity: millions of variables
40
42. S. A. Seshia 1
Some Experience with SAT Solving
Sanjit A. Seshia
Speed-up of 2012 solver over other solvers
1
10
100
1,000
Solver
Speed-up(logscale)
41
43. Applications of SAT Solving in SW Engineering
Leonardo De Moura+Nikolaj Bj即orner, 2012: applications of Z3 at Microsoft
Symbolic execution
Model checking
Static analysis
Model-based design
. . .
42
44. The Temporal Logic of Programs
Crux: Need to specify ongoing behavior rather than input/output relation!
Temporal logic to the rescue [Pnueli, 1977]:
Linear temporal logic (LTL) as a logic for the
speci鍖cation of non-terminating programs
Model checking via reduction to MSO
But: nonelementary complexity!
43
45. Examples
always not (CS1 and CS2): safety
always (Request implies eventually Grant): liveness
always (Request implies (Request until Grant)): liveness
44
46. Model Checking
Algorithmic veri鍖cation [Clarke Emerson,
1981, Queille Sifakis, 1982]: Model checking
programs of size m wrt CTL formulas of size n
can be done in time mn.
Linear-Time Response [Lichtenstein Pnueli, 1985]: Model checking
programs of size m wrt LTL formulas of size n can be done in time m2O(n)
(tableau heuristics).
Seemingly:
Automata: Nonelementary
Tableaux: exponential
45
47. Back to Automata
Exponential-Compilation Theorem [V. Wolper, 19831986]: Given an
LTL formula of size n, one can construct an automaton A of size 2O(n)
such that a trace satis鍖es if and only if is accepted by A.
Automata-Theoretic Algorithms:
1. LTL Satis鍖ability:
is satis鍖able i鍖 L(A) = (PSPACE)
2. LTL Model Checking:
M |= i鍖 L(M A測) = (m2O(n)
)
Today: Widespread industrial usage
Industrial Languages: PSL, SVA (IEEE standards)
46
48. Solving the Unsolvable
B. Cook, A. Podelski, and A. Rybalchenko, 2011:in contrast to popular
belief, proving termination is not always impossible
The Terminator tool can prove termination or divergence of many
Microsoft programs.
Tool is not guaranteed to terminate!
Explanation:
Most real-life programs, if they terminate, do so for rather simple reasons.
Programmers almost never conceive of very deep and sophisticated
reasons for termination.
47
49. Logic: from failure to success
Key Lessons:
Algorithms
Heuristics
Experimentation
Tools and systems
Key Insight: Do not be scared of worst-case complexity.
It barks, but it does not necessarily bite!
48
50. Limits of Logic
Blaise Pascal, 1623-1662:
Two excesses: to exclude reason, to admit nothing but reason.
The heart has its reasons, which reason knows not.
49