�ݺ�ߣ

A Logical Revolution
Moshe Y. Vardi
Rice University

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

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

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

What is The Language of Mathematics?
Friedrich Ludwig Gottlob Frege, Begriffsschrift, 1879: a universal
mathematical language – first-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” (→)
• Quantifiers, e.g., “for all” (∀), “exists” (∃)
4

Example: Aristotle’s Syllogisms
• “All men are mortal”
• “For all x, if x is a man, then x is mortal”
• (∀x)(Man(x) → Mortal(x))
5

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

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

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

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

Russell’s Letter
A letter from Russell to Frege, June 16, 1902:
“I find myself in agreement with you in all essentials . . . I find in your
work discussions, distinctions, and definitions that one seeks in vain
in the work of other logicians . . . There is just one point where I have
encountered a difficulty.”
Appendix to Frege’s 1903 volume:
“There is nothing worse that can happen to a scientist than to have
the foundation collapse just as the work is finished. I have been placed
in this position by a letter from Mr. Bertrand Russell.”
10

Hilbert’s Program
Hilbert’s 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

The Demise of Hilbert’s Program
• Gödel (1930-3):
– Incompleteness of ordinary arithmetic – There is no systematic way of
resolving all mathematical questions.
– Impossibility of proving consistency of mathematics
Gödel (1930): “This sentence is not provable.”
• Church and Turing (1936):
Unsolvability of first-order logic:
– The set of valid first-order sentences is not computable.
12

Entscheidungsproblem
Entscheidungsproblem (The Decision Problem) [Hilbert-Ackermann,
1928]: Decide if a given first-order sentence is valid (dually, satisfiable).
Church-Turing Theorem, 1936: The Decision Problem is unsolvable.
Turing, 1936:
• Defined computability in terms of Turing machines (TMs)
• Proved that the termination problem for TMs is unsolvable (“this
machine terminates iff it does not terminate”)
• Reduced termination to Entscheidungsproblem.
13

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

The Fragment-Classification Project
Idea: Identify decidable quantificational fragments of first-order logic –
(1915-1983)
• Bernays-Schönfinkel Class (∃∗
∀∗
)
• Ackermann Class (∃∗
∀∃∗
)
• Gödel Class (w/o =) (∃∗
∀∀∃∗
)
Outcome: Very weak classes! What good is first-order logic?
15

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

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

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

Monadic Logic
Monadic Class: First-order logic with monadic predicates – captures
syllogisms.
• (∀x)P(x), (∀x)(P(x) → Q(x)) |= (∀x)Q(x)
[Löwenheim, 1915]: The Monadic Class is
decidable.
• Proof: Bounded-model property – if a sentence
is satisfiable, it is satisfiable in a structure of
bounded size.
• Proof technique: quantifier elimination.
19

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

Finite Words – Nondeterministic Finite Automata, II
Input word: a0, a1, . . . , an−1
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 1’s
Fact: NFAs deﬁne the class Reg of regular languages.
21

Logic of Finite Words
View ﬁnite word w = a0, . . . , an−1 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

Automata and Logic
Theorem [Büchi, Elgot, Trakhtenbrot, 1957-8
(independently)]: MSO ≡ NFA
• Both MSO and NFA define the class Reg.
Proof: Effective
• From NFA to MSO (A → ϕA)
• From MSO to NFA (ϕ → Aϕ)
23

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 iff there is a path in GA from S0 to F.
• Decidable in time linear in size of A, using breadth-first search or
depth-first search.
24

MSO Satisfiability – Finite Words
Satisfiability: models(ψ) = ∅
Satisfiability Problem: Decide if given ψ is satisfiable.
Lemma: ψ is satisfiable iff Aψ is nonnempty.
Corollary: MSO satisfiability is decidable.
• Translate ψ to Aψ.
• Check nonemptiness of Aψ.
25

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

Nonelementary Growth
• 22
= 4
• 223
= 256
• 2224
= 4, 294, 967, 296
• 22225
≈ 10109
27

Boole’s Symbolic Logic
Boole’s insight: Aristotle’s 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

Boolean Satisﬁability
Boolean Satisﬁability (SAT); Given a Boolean expression, using “and”
(∧) “or”, (∨) and “not” (¬), is there a satisfying solution (an assignment
of 0’s and 1’s 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

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öder, 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 effort to show hardness of search
problems.
• Cook, 1971, Levin, 1973: Boolean Satisfiability is NP-complete.
30

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

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

Program Verification
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 verification is bound to fail. We can’t see how it’s going to be able
to affect anyone’s confidence about programs.”
• Basic Argument: Acceptance of proof is a social process!
33

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

Post 1980: From Irrelevance to Relevance
A Logical Revolution:
• Relational databases
• Boolean reasoning
• Model checking
• Termination checking
• . . .
35

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

Relational Databases
Codd’s 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

Algorithmic Problems in First-Order Logic
Satisfiability Problem: Given a first-order formula ψ, is there a graph G
and binding α, such that G |=α ψ?
Truth-Evaluation Problem: Given a first-order formula ϕ(x1, . . . , xk), a
finite graph G, and a binding α, does G |=α ϕ(x1, . . . , xk)?
Contrast:
• Satisfiability is undecidable [Church, Turing 1936]
• Truth evaluation, which is query evaluation, is decidable.
38

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

Modern SAT Solving
CDCL = conflict-driven clause learning
• Backjumping
• Smart unit-clause preference
• Conflict-driven clause learning
• Smart choice heuristic (brainiac vs speed demon)
• Restarts
Key Tools: GRASP, 1996; Chaff, 2001
Current capacity: millions of variables
40

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

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

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

Examples
• always not (CS1 and CS2): safety
• always (Request implies eventually Grant): liveness
• always (Request implies (Request until Grant)): liveness
44

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

Back to Automata
Exponential-Compilation Theorem [V. Wolper, 1983–1986]: Given an
LTL formula ϕ of size n, one can construct an automaton Aϕ of size 2O(n)
such that a trace σ satisfies ϕ if and only if σ is accepted by Aϕ.
Automata-Theoretic Algorithms:
1. LTL Satisfiability:
ϕ is satisfiable iff L(Aϕ) = ∅ (PSPACE)
2. LTL Model Checking:
M |= ϕ iff L(M × A¬ϕ) = ∅ (m2O(n)
)
Today: Widespread industrial usage
• Industrial Languages: PSL, SVA (IEEE standards)
46

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

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

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

�ݺ�ߣ

Logicrevo15

More Related Content

Logicrevo15