狠狠撸

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, 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

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 ?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 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 ?nished. 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¨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

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

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-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

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¨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

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¨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

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

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

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¨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

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 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 can’t see how it’s going to be able
to a?ect anyone’s con?dence 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
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

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 = 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

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 σ 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

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