Transcript x - UIC - Computer Science

Extensional Reasoning
Timothy L. Hinrichs
Stanford Logic Group
Classical Logic in the World Today
Cyc
“People have silly reasons why computers don't really think. The answer is we haven't
programmed them right; they just don't have much common sense. There's been only one
large project to do something about that, that's the famous Cyc project.” ~ Marvin Minsky,
MIT, May 2001
SUMO (Suggested Upper Merged Ontology)
“[SUMO] and its domain ontologies form the largest formal public ontology in existence today.
They are being used for research and applications in search, linguistics and reasoning. SUMO
is the only formal ontology that has been mapped to all of the WordNet lexicon.”
SNOMED CT (Systemized Nomenclature of Medicine--Clinical Terms)
“... one of a suite of designated standards for use in U.S. Federal Government
systems for the electronic exchange of clinical health information and is also a
required standard in interoperability specifications of the U.S. Healthcare
Information Technology Standards Panel.”
NCI (National Cancer Institute) Ontology
“… facilitate translational research and to support the bioinformatics infrastructure of the
Institute. Topics described in the ontology include diseases, drugs, chemicals, diagnoses,
genes, treatments, anatomy, organisms, and proteins.”
Galen medical ontology, Gene ontology, …
Extensional Reasoning
2
Automated Deduction
Given:
, a set of logical sentences
, a logical sentence
Question:
Does
Extensional Reasoning

|= 
3
Entailment

|= 
if and only if
every model that
satisfies  also
satisfies 
p(a)  p(b) |= x.p(x)
Model 1
p
a
Extensional Reasoning
Model 2
p
Model 3
p
b
a
b
4
Syntactic Manipulation
Sometimes there are infinitely many models.
Nevertheless, if |=  we can demonstrate it in
finite time through syntactic manipulation.
 ,  

Automated syntactic manipulation: resolution,
tableaux, natural deduction
Extensional Reasoning
5
Common Structure
Many (large) knowledge bases share a common
structure. Syntactic manipulation fails to leverage
that structure.
Data (e.g., ABox)
parent(alice,bob)
alice(alice,charlie)
female(alice)
male(bob)
male(charlie)
Extensional Reasoning
Logical Axioms (e.g., TBox)
parent(x,y)  parent(x,z)  male(y)  brother(y,z)
parent(x,y)  parent(x,z)  female(y)  sister(y,z)
6
Extensional Reasoning
Transform an entailment query  |=1  in classical
logic into an entailment query    |=2  where
 is a set of extensions (explicitly defined tables)
 is a set of intensions (view definitions or implicitly-defined tables)
 is a database query
such that  |=1  if and only if    |=2 

Extensional Reasoning
|=1 
, 
|=2

7
Hospital Sensor Network
Two sensor readings
1
2
3
4
5
6
7
8
9
10
11 12 13
14 15
16 17 18
19
21 22
23 24 25
Patient
Extensional Reasoning
20
Oxygen
Axioms
p(c2)  p(c6)  p(c7)  p(c8)  p(c12)
xy.(p(x)  p(y)  x=y)
o(c14)  o(c18)  o(c19)  o(c20)  o(c24)
xy.(o(x)  o(y)  x=y)
xy.(n(x,y)  (w2(x,y)  w3(x,y)))
xy.(w2(x,y)  z.(a(x,z)  a(z,y)))
xy.(w3(x,y)  z.(w2(x,z)  a(z,y)))
xy.(a(x,y)  (e(x,y)  e(y,x)))
xy.(e(x,y)  ((x=c1 ^ y=c2) 
(x=c1 ^ y=c6)  …)
Queries
xy.(p(x)  o(y)  a(x,y))
xy.(p(x)  o(y)  n(x,y))
8
Database Formulation
Database Query
query :- not(counterexample)
counterexample :- possp(x)(x) ^ posso(y)(y) ^ a(x,y)
Extensions
p
o
c14c18c19c20c24
View Definitions
c02c06c07c08c12
r
e
u
c14c18c19c20c24
c14
c01
c02
c01
c14c18c19c20c24
c18
c01
c06
c02
c14c18c19c20c24
c19
c02
c03
c03
c14c18c19c20c24
c20
c02
c07
c04
c14c18c19c20c24
c24
c03
c04
c05
c02c06c07c08c12
c02
c04
c08
c06
…
…
c05
c09
c07
…
…
…
Extensional Reasoning
possp(x)(x) :- p(y) ^ r(y,x) ^ not(smp(x))
smp(x) :- p(y) ^ not(r(y,x)) ^ u(x)
posso(x)(x) :- o(y) ^ r(y,x) ^ not(smo(x))
smo(x) :- o(y) ^ not(r(x,y)) ^ u(x)
n(x,y) :- w2(x,y)
n(x,y) :- w3(x,y)
w2(x,y) :- a(x,z) ^ a(z,y)
w3(x,y) :- w2(x,z) ^ a(z,y)
a(x,y) :- e(x,y)
a(x,y) :- e(y,x)
9
Contributions
1. Extensional Reasoning for Complete Theories
Reformulation into biconditionals
2. Extensional Reasoning for Incomplete Theories
Inference rule for Theory Resolution
Entailment-preserving Theory-completion
•
•
Extensional Reasoning
poss and its properties
poss predicate definition construction
10
Finite Herbrand Logic (FHL)
Classical first-order logic without function constants.
Plus
– Domain closure axiom (DCA) over all the finitely many
object constants
x. (x=a  x=b  x=c)
– Unique names axioms (UNA)
ab
ac
bc
Entailment: coNEXPTIME-complete
Extensional Reasoning
11
Standard FHL Proof Procedures
1. First-order theorem provers
Need to include DCA and UNA.
2. Boolean SAT solvers
Need to convert FHL to propositional logic.
Extensional Reasoning
12
Deductive Databases
A deductive database is a representation of a single
model.
A model is a set of named tables.
left
adj
a b
a b
b c
b a
c d
b c
c b
c d
d c
Extensional Reasoning
13
Deductive Databases
A deductive database is a representation of a single
model.
A model is a set of named tables.
Option 1
left
adj
a b
a b
b c
b a
c d
b c
Option 2
left
a b
b c
c d
c b
c d
d c
Extensional Reasoning
adj(x,y) :- left(x,y)
adj(x,y) :- left(y,x)
14
nr-datalog
Syntax
– A set of named tables, the extensions.
– A set of view definitions: safe, nonrecursive implications
with positive heads and no function constants.
h :- []b1  …  []bn
– The table names and predicates in rule heads are disjoint.
Stratified Semantics
Minimal model semantics, iterated up the stratification
hierarchy.
Evaluation: PSPACE-complete (combined complexity)
LOGSPACE-complete (data complexity)
Extensional Reasoning
15
Comparison
Model:
left
adj
a b
a b
b c
FHL:
b a
c d
b c
xy.(adj(x,y) 
left(x,y)  left(y,x))
xy.(left(x,y) 
(x=a  y=b) 
(x=b  y=c) 
(x=c  y=d))
c b
c d
d c
nr-datalog:
left
a b
b c
c d
Extensional Reasoning
adj(x,y) :- left(x,y)
adj(x,y) :- left(y,x)
16
Contributions
1. Extensional Reasoning for Complete Theories
Reformulation into biconditionals
2. Extensional Reasoning for Incomplete Theories
Inference rule for Theory Resolution
Entailment-preserving Theory-completion
•
•
Extensional Reasoning
poss and its properties
poss predicate definition construction
17
Complete Theories
Suppose  |=  is an entailment query about a
satisfiable, complete theory in classical logic: for
every closed sentence 
 |=  or  |= 
Then there is some model M such that the query
holds if and only if M satisfies 
 |=  iff |=M 
M can be represented by a database system.
Extensional Reasoning
18
er-complete-prove
ER-COMPLETE-PROVE(, )
Assumptions:  is complete and satisfiable
Returns: T iff  |=  in FHL
1:
2:
3:
4:
5:
6:
 := to-biconds()
(D, V) := partition()
 := to-tables(D)
 := to-views(V)
 := to-query()
return db-prove(, , )
Extensional Reasoning
19
Nonrecursive Biconditionals
Theorem: In FHL,  is complete and satisfiable if and
only if it can be written as a set of nonrecursive
biconditionals with one biconditional per predicate
besides =.
NB: Not true in FOL because = is not complete.
xy.(adj(x,y)  (left(x,y)  left(y,x)))
xy.(left(x,y)  ((x=a  y=b) 
(x=b  y=c) 
(x=c  y=d)))
Extensional Reasoning
20
Example
p(x)  s(x)
p(x)  s(x)
s(x)  xa
s(x)  xb
s(x)  x=a  x=b
Suppose these sentences were originally written as a
set of nonrecursive biconditionals.
At least one of the definitions must use only =.
Extensional Reasoning
21
Example
p(x)  s(x)
p(x)  s(x)
s(x)  xa
s(x)  xb
s(x)  x=a  x=b
Suppose these sentences were originally written as a
set of nonrecursive biconditionals.
At least one of the definitions must use only =.
Extensional Reasoning
22
Example
p(x)  s(x)
p(x)  s(x)
x.(s(x)  (x=a  x=b))
Suppose these sentences were originally written as a
set of nonrecursive biconditionals.
At least one of the definitions must use only =.
Extensional Reasoning
23
Example
x.(p(x)  s(x))
x.(s(x)  (x=a  x=b))
Suppose these sentences were originally written as a
set of nonrecursive biconditionals.
Variation on the well-known CFG marking algorithm.
Extensional Reasoning
24
to-biconds Complexity
Complexity is O(n2(|| + f())
n: number of predicates
||: size of the sentence set 
f(): cost of reformulate-to-bicond
Note: reformulate-to-bicond is a metalevel
proof procedure.
Extensional Reasoning
25
to-biconds Soundness
Theorem (Soundness [HG07b]): Under the
following conditions, if to-biconds() returns
a non-empty  then  is a set of nonrecursive biconditionals with one definition
per predicate besides equality and  is
logically equivalent to .
  is a satisfiable FHL theory
• reformulate-to-bicond is sound
Extensional Reasoning
26
to-biconds Completeness
Theorem (Completeness [HG07b]): Under
the following conditions, if is a complete
theory in FHL then to-biconds() returns a
non-empty set.
  is satisfiable, nonempty, and partitioned into n pieces S1,…,Sn, where
n is the number of predicates
  is logically equivalent to the nonrecursive biconditionals {1,…,n}
 i is logically equivalent to Si and Preds(i) = Preds(Si)
• reformulate-to-biconditional is complete
Extensional Reasoning
27
partition
Database problem
– E: extensional tables and
– V: view definitions
– Q: query load
[ACN00, BPT97]: Techniques for choosing the subset
of V to materialize.
[Chirkova02]: Computing the optimal viewset to
materialize (regardless of V), given a space
constraint.
Extensional Reasoning
28
er-complete-prove
ER-COMPLETE-PROVE(, )
Assumptions:  is complete and satisfiable
Returns: T iff  |=  in FHL
1:
2:
3:
4:
5:
6:
 := to-biconds()
(D, V) := partition()
 := to-tables(D)
 := to-views(V)
 := to-query()
return db-prove(, , )
Extensional Reasoning
29
Deductive Databases
Bounded response time
Polynomial in data and exponential in query
Extensionally represented relations
Index-friendly canonical form
Negation as Failure (NAF)
Compute p using the minimum search space of p and p
Extensional Reasoning
30
Biconditional Search Space
Lemma: Consider the following biconditional b.
x.(p(x)  ((p11(x)  …  p1n1(x))
…
(pm1(x)  …  pmnm(x))))
Suppose
• P is a proof procedure that is generatively complete for
clauses up to subsumption.
• C is a clausal form converter that preserves logical
equivalence (for ps) in the absence of skolemization.
P(C(b)) will generate at least
Extensional Reasoning
i ni clauses
31
Contributions
1. Extensional Reasoning for Complete Theories
Reformulation into biconditionals
2. Extensional Reasoning for Incomplete Theories
Inference rule for Theory Resolution
Entailment-preserving Theory-completion
•
•
Extensional Reasoning
poss and its properties
poss predicate definition construction
32
Incomplete Theories
Complete theories have powerful properties, but incomplete
theories are the norm.
Incomplete theories have multiple models, and a query must
be true in all models to be entailed.
p(a)  p(b)
Model 1
p
a
Extensional Reasoning
|= x.p(x)
Model 2
p
Model 3
p
b
a
b
33
Theory Resolution
Every theory in FHL is complete for at least =.
Suppose the theory can be written as C  I.
– C is the complete portion of the theory
– I is the incomplete portion of the theory
Theory Resolution [Stickel85]: use database for C and
resolution for I.
[HG07b] When I is universal, we demonstrate a sound
and complete rule of inference for theory resolution.
Extensional Reasoning
34
Large Theories
Consider a large theory C  I where
size of C >> size of I
Suppose proof requires C’  I, where C’  C
If C’ is large, resolution must manipulate a large
amount of data.
May want/need to use the database to process all
that data effectively.
Extensional Reasoning
35
Entailment-Preserving
Theory-Completion
Def (Entailment-Preserving Theory-Completion)
Given an entailment query  |= , construct an
entailment query ’ |= ’ such that ’ is complete
and
 |= 
iff
’ |= ’
NB: This form of theory completion is unlike that studied in the nonmonotonic
reasoning literature, which is concerned with theory minimization.
Extensional Reasoning
36
Entailment-Preserving
Theory-Completion
Def (Entailment-Preserving Theory-Completion)
Given an entailment query C  I |= , construct an
entailment query C  I’ |= ’ such that I’ is
complete and
C  I |= 
iff
C  I’ |= ’
Extensional Reasoning
37
Reifying Satisfiability
Satisfiability is a complete concept in all theories.
  {} is either satisfiable or it is not satisfiable.
Create a new predicate that represents the satisfiability
(possibility) of   {}.
poss is true if and only if   {} is satisfiable
The new query: a sentence expressed using poss predicates
The completed theory: complete definitions for poss predicates
Extensional Reasoning
38
Completed Hospital Sensor Network
Incomplete
C
 xy.(p(x)  o(y)  a(x,y)
a(x,y)  (e(x,y)  e(y,x))
e(x,y)  ((x=c1 ^ y=c2) 
(x=c1 ^ y=c6)  …)
I
p(c2)  p(c6)  p(c7)  p(c8)  p(c12)
p(x)  p(y)  x=y
o(c14)  o(c18)  o(c19)  o(c20)  o(c24)
o(x)  o(y)  x=y
Complete ’ xy. (possp(x)(x)  posso(y)(y)  a(x,y))
I’
C
a(x,y)  (e(x,y)  e(y,x))
e(x,y)  ((x=c1 ^ y=c2) 
(x=c1 ^ y=c6)  …)
Extensional Reasoning
possp(x)(x) 
(x=c2  x=c6  x=c7  x=c8  x=c12)
posso(y)(x) 
(x=c14  x=c18  x=c19  x=c20  x=c24)
39
poss Examples
Universe: a, b, c
Premise
poss
•
•
•
•
{x.p(x)}
{x.p(x)}
{x. p(x)}
{x.p(x)}
possp(a) is true
possp(a) is false ensures possp(a) is true
possp(a) is true
possx.p(x) is true
•
•
•
•
•
{x.p(x)}
{x.p(x)}
{x.p(x)}
{x.p(x)}
{p(a), p(b)}
possp(x)(x)  x=a  x=b  x=c
x. possp(x)(x)
possp(x)(x)  x=a  x=b  x=c
possp(x)(x)  x=a  x=b  x=c
possp(x)(x)  x=c
Extensional Reasoning
40
How do we construct the new query?
Every entailment query can be written as a poss
query.
Refutational TP:
 |=  iff   {} is unsatisfiable
Extensional Reasoning:
 |=  if and only if poss is true
Extensional Reasoning
41
poss Properties [HG07a]
poss Distributes Over
Conditions







Independent
Complete
Nondisjunctive Existential
Theorem: If  is complete for (t) then poss(x)(t) is true if and
only if  entails (t).
NB: poss is a very restricted form of the modal logic possibility operator .
Extensional Reasoning
42
simplify applied to Hospital Query
 |= xy.(p(x)  o(y)  a(x,y))
(by the definition of poss)
possxy.(p(x)  o(y)  a(x,y))
(by logical equivalence)
possxy.(p(x)  o(y)  a(x,y))
(by distributing over )
xy.possp(x)  o(y)  a(x,y)(x,y)
(by distributing over : p, o, and a are independent)
xy.possp(x)(x)  posso(y)(y)  possa(x,y)(x,y)
(by completeness of a)
xy.possp(x)(x)  posso(y)(y)  a(x,y)
(by logical equivalence)
xy.(possp(x)(x)  posso(y)(y)  a(x,y))
Extensional Reasoning
43
Completed Hospital Sensor Network
Incomplete
C
 xy.(p(x)  o(y)  a(x,y)
a(x,y)  (e(x,y)  e(y,x))
e(x,y)  ((x=c1 ^ y=c2) 
(x=c1 ^ y=c6)  …)
I
p(c2)  p(c6)  p(c7)  p(c8)  p(c12)
p(x)  p(y)  x=y
o(c14)  o(c18)  o(c19)  o(c20)  o(c24)
o(x)  o(y)  x=y
Complete ’ xy. (possp(x)(x)  posso(y)(y)  a(x,y))
I’
C
a(x,y)  (e(x,y)  e(y,x))
e(x,y)  ((x=c1 ^ y=c2) 
(x=c1 ^ y=c6)  …)
Extensional Reasoning
possp(x)(x) 
(x=c2  x=c6  x=c7  x=c8  x=c12)
posso(y)(x) 
(x=c14  x=c18  x=c19  x=c20  x=c24)
44
poss Definition Spectrum
Evaluation Cost
Compute
S = {t | ; (t) is sat}
poss(x)(x)  x  S
Reformulation Cost
Extensional Reasoning
45
Approaches
Two approaches for computing definition for poss
Model Theoretic
– Enumerate models and check whether  is satisfied.
– Hard part: enumerating just the important models.
Proof Theoretic
– poss is true iff C  I |/- 
– Hard part: looking only at I, computing a sentence  such
that C |-  if and only if C  I |/- 
Extensional Reasoning
46
Map Coloring
xy. (color(x,y)  region(x)  hue(y))
xyz.(color(x,y)  adj(x,z)  color(z,y))
r1
r2
r3
posscolor(r1,x)  color(r2,y)  color(r3,z)(x,y,z) 
incon(r1, x, r2, y, r3, z)
incon(x1,y1,x2,y2,x3,y3) 
(region(x1)  hue(y1)  (adj(x1,x2)  y1 = y2)
region(x2)  hue(y2)  (adj(x2,x3)  y2 = y3)
region(x3)  hue(y3)  (adj(x1,x3)  y1 = y3))
Extensional Reasoning
47
poss via Proof Theory
Consider a special case:
C  *.I
Want poss definition for
[]p1(a1)  …  []pm(am)
A conjunction is inconsistent with a theory if and only
if it is inconsistent with some clause in the closure.
Note: We can always force the resolution closure to
be finite because of the finite universe.
Extensional Reasoning
48
er-incomplete-prove
ER-INCOMPLETE-PROVE(, )
Assumptions:  is satisfiable and  is closed
Returns: T iff  |=  in FHL
1: C  I := to-biconds-max()
2:
3:
4:
5:
’ simplify(poss, preds(C), I
 := poss-defns(poss-preds(’), preds(C), I)
’ := C  
return er-complete-prove(’, ’)
Extensional Reasoning
49
Coverage
[HG07c] shows how to compute the classes of
poss definitions necessary for answering the
following classes of entailment queries.
Proof-theoretic approach
C  *.I |= **.
Model-theoretic approach
C  I |= 
Extensional Reasoning
50
Completed Hospital Sensor Network
Incomplete
C
 xy.(p(x)  o(y)  a(x,y)
a(x,y)  (e(x,y)  e(y,x))
e(x,y)  ((x=c1 ^ y=c2) 
(x=c1 ^ y=c6)  …)
I
p(c2)  p(c6)  p(c7)  p(c8)  p(c12)
p(x)  p(y)  x=y
o(c14)  o(c18)  o(c19)  o(c20)  o(c24)
o(x)  o(y)  x=y
Complete ’ xy. (possp(x)(x)  posso(y)(y)  a(x,y))
I’
C
a(x,y)  (e(x,y)  e(y,x))
e(x,y)  ((x=c1 ^ y=c2) 
(x=c1 ^ y=c6)  …)
Extensional Reasoning
possp(x)(x) 
(x=c2  x=c6  x=c7  x=c8  x=c12)
posso(y)(x) 
(x=c14  x=c18  x=c19  x=c20  x=c24)
51
Contributions
1. Extensional Reasoning for Complete Theories
Reformulation into biconditionals
2. Extensional Reasoning for Incomplete Theories
Inference rule for Theory Resolution
Entailment-preserving Theory-completion
•
•
Extensional Reasoning
poss and its properties
poss predicate definition construction
52
Instances
1
2
3
4
5
6
7
8
9
10
11 12 13
14 15
16 17 18
19
21 22
20
23 24 25
Extensional Reasoning
53
Comparison
ER with Prolog
1000
Theorem Prover (Darwin)
Model Builder (Paradox)
SAT Solver (minisat)
Log of Seconds
100
10
1
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
0.1
0.01
Grid size (n x n)
Query: adj(a,b)
Extensional Reasoning
54
Comparison
ER with Prolog
100000
Theorem Prover (Darwin)
Model Builder (Paradox)
10000
SAT Solver (minisat)
Log of Seconds
1000
100
10
1
4
5
6
7
8
9
10
11
12 13
14
15
16
17
18
19
20
0.1
0.01
Grid size (n x n)
Query: adj(a,b)
Extensional Reasoning
55
Comparison
100000
ER with Prolog
10000
Theorem Prover (Darwin)
Log of Seconds
1000
100
10
1
4
5
6
7
8
9
10 11 12 13 14 15 16 17 18 19 20
0.1
0.01
Grid size (n x n)
Query: westof(a,b)
Extensional Reasoning
56
Query: xy.(p(x)  o(y)  a(x,y))
Extensional Reasoning
EP
ac
e4
M
e
Pr tis
V
am ove
p r9
V ire
am
8
pi .1
re
9.
0
M
E
ad
o
S x
PA
S
iP S
D ro
ar ve
w
r
D in 1
ar
w .3
in
1.
S 4
R
D AS
ar
S
w
in
Eq FM
ui
no
x
G
B eo
lik
se
m
Pa
r
Seconds
ATP Techniques
1000
100
10
1
0.1
Grid size: 5x5
57
Comparison
Database (Prolog)
100000
Theorem Prover (Spass)
10000
Model Builder (Paradox)
SAT Solver (Minisat)
Seconds
1000
100
10
1
5
6
7
8
9
10 11 12 13 14 15 16 17 18 19 20
0.1
0.01
Grid size (n x n)
Query: xy.(p(x)  o(y)  a(x,y))
Extensional Reasoning
58
Future Work
Nonrecursive set of guarded biconditionals
Completeness for a subset of the universe
Relax finite domain assumption
Target a full logic programming language.
Apply to modal logic
Translate an incomplete dynamic system description
to a complete dynamic system description
Extensional Reasoning
59
Automated Reasoning
SAT Solver
CSP Solver
Uniform interface
to Automated
Reasoning Tools
Relational Database
Logic Programming
Model Checker
Theorem Prover
Extensional Reasoning
60
References
[HG07a] Hinrichs, Genesereth: Reformulation for Extensional Reasoning. In proceedings for
the Symposium of Abstraction, Reformulation, and Approximation. July 2007.
[HG07b] Hinrichs, Genesereth: Extensional Reasoning. In proceedings for CADE Workshop
on Empirically Successful Automated Reasoning in Large Theories (ESARLT). July 2007.
[HG07c] Hinrichs, Genesereth: Consistency to Deduction for Extensional Reasoning. In
preparation. 2007
[ACN00] Agrawal, Chaudhuri, and Narasayya. Automated selection of materialized views and
indexes in Microsoft SQL Server. In Proc. of VLDB, pp. 496-505, 2000.
[BPT97] Baralis, Paraboschi, and Teniente. Materialized views selection in a multidimensional
database. In Proc. of VLDB, pp. 156-165, 1997.
[Chirkova02] Rada Chirkova. Automated Database Restructuring. Stanford thesis, 2002.
[Minisat] http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/
[Paradox] http://www.cs.chalmers.se/~koen/folkung/
[Spass] http://spass.mpi-sb.mpg.de/
[Stickel85] Stickel. Automated Deduction by Theory Resolution. Journal of Automated
Reasoning, pp. 333-356, 1985.
Extensional Reasoning
61
End of Talk
Extensional Reasoning
62
Model-based Reasoning
Sometimes there are only a few models.
Claim: Checking the models is sometimes more
efficient than syntactic manipulation.
Model Building:
given  find all models M that satisfy it
Model Checking:
given M,  determine if M satisfies 
Extensional Reasoning
63
Large Models
If  is only satisfied by a few models, but those
models are large, building and checking them can
be expensive.
Representation: compress size of model by
leveraging its structure
Reasoning: mitigate the effects of a compact
representation
The field where these issues are studied: Databases
Extensional Reasoning
64
Related Work
•
•
•
•
•
•
•
•
•
(Deductive) Databases
Constraint Satisfaction
Logic Programming
Model building
Model checking
Boolean SAT
Tableaux
Abduction
Semantic web language
interoperability
Extensional Reasoning
• Semantically-guided
resolution
• Knowledge Compilation
• Characteristic Models
• Inductionless induction
• Dividing and Conquering
Logic
• LP partial deduction
• Caching
• Logic program synthesis
65
Amortization
Reformulation can be expensive
FHL: coNEXPTIME-complete, Datalog: PSPACE-complete
• Complete theories: reformulate once and answer
every query in the language.
• Incomplete theories
–
–
–
–
Answer several queries with the same poss predicates
Incrementally construct poss definitions
Reformulate once, just like the complete case
Alter the complete portion of the theory.
Extensional Reasoning
66
to-biconds
TO-BICONDS(, basepreds)
1: sents := {<p,d> | d   and p  basepreds and
preds(d) is p plus a subset of basepreds}
2: preds := {p | <p,d>  sents}
3: bicond := false
4: for all p  preds
5:
partition := {d | <p,d>  sents}
6:
bicond := reformulate-to-bicond(partition, p)
7:
pred := p
8:
when bicond  false then exit for all
9: when bicond = false then return false
10: remaining :=   partition
11: when remaining = {} then return {bicond}
12: rest := to-biconds(remaining, {pred}  basepreds)
13: when rest  false then return {bicond}  rest
14: return false
Extensional Reasoning
67
Marketing for Extensional Reasoning
Theorem proving community
Datalog-based deduction
Database community
Collaborative view construction
Logic programming community
Logic program synthesis
Constraint satisfaction community
Deduction via constraint satisfaction
Extensional Reasoning
68
Theory Partitioning
How do we partition a theory based on
independence?
pq
qr
Dependency graph
p
q
Without complete predicates
p
Partitioning
r
Extensional Reasoning
pq
qr
Partitioning
r
pq
qr
69
Yesterday and Tomorrow
Natural
Efficient
Put the burden of creating an efficient formulation on the machine.
Natural
Extensional Reasoning
Efficient
70
Reformulation Cost vs. Evaluation Cost
Evaluation Cost
R: E: Compute
 |= 
R: Compute
 |= 
E: Return Ans
Reformulation Cost
Goal: Minimize Reformulation cost + Evaluation cost
Extensional Reasoning
71
to-tables, to-views, to-query
Convert to Table: xy.(r(x,y)  ((x=a  y=b)  (x=b  y=c)))
r
a
b
b
c
Convert to View (Lloyd-Topor): x.(p(x)  y. (q(y)  r(y,x)))
1. p(x) :- y. (q(y)  r(y,x))
2. p(x) :- y.(q(y)  r(y,x))
3. p(x) :- y. (q(y)  r(y,x))
4. p(x) :- not(s(x))
a) s(x)  y. (q(y)  r(y,x))
b) s(x) :- q(y) ^ not(r(y,x))
5. p(x) :- univ(x) ^ not(s(x))
Extensional Reasoning
72
Boolean SAT
Can answer FHL entailment via boolean SAT.
 |=  iff Grounding(  {) is unsatisfiable
Grounding(x.(x)) is (a1)  …  (an)
Grounding(x.(x)) is (a1)  …  (an)
Issues:
– Grounding costs exponential time and space
– Converting to CNF can also be expensive
Extensional Reasoning
73
Database Advantages
Databases represent a balance between
• Normal form
Spectrum of normal forms: from propositional CNF
(SAT solvers) to clausal form (FOL theorem
provers)
• Relational logic
Allows us to exploit the relational structure of the
original problem.
Extensional Reasoning
74
Scrap Slides Begin Here
Extensional Reasoning
75
Efficiency
35000
Database (Prolog)
30000
Seconds
Theorem Prover (Spass)
25000
Model Builder (Paradox)
20000
SAT Solver (Minisat)
15000
10000
5000
0
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
Grid size (n x n)
Query: xy.(p(x)  o(y)  a(x,y))
Extensional Reasoning
76
Computer Programming
Software for answering questions about a
theory.
Software is a complete theory about the state
of the machine.
Reformulates a (possibly) incomplete theory
into a complete theory with a different
vocabulary.
Extensional Reasoning
77
Theories
Protein Folding
Physics
Complete vs. Incomplete theories
Extensional Reasoning
78
Models
Which object cast
this shadow?
Extensional Reasoning
79
Formalization
Theory: set of logical sentences
Model: relational database (one table for each
predicate in the vocabulary)
Asking questions: deduction queries.
Given: , a set of logical sentences
, a logical sentence
Say iff every model of is a model of .
* In this talk, every theory has a finite set of finite models.
Extensional Reasoning
80
Models
Vocabulary: Symbols representing objects
Symbols representing relations
Model: objects and the relationships between them
a
c
p
p
q
b
Satisfaction: p(a,b)
p(a,b)  q(b,c)
p(b,c)
x. p(x,a)
Extensional Reasoning
81
Model-Based Computation
Model home
Extensional Reasoning
Model airplane
82
Representations of Models
Model:
left
adj
a b
a b
b c
b a
c d
b c
c b
c d
d c
Datalog:
left
adj(x,y) 
left(x,y)  left(y,x)
left(x,y) 
(x=a  y=b) 
(x=b  y=c) 
(x=c  y=d)
a b
b c
c d
Extensional Reasoning
FHL:
adj(x,y) :- left(x,y)
adj(x,y) :- left(y,x)
83
Logic
Declarative language for unambiguously expressing
laws/rules/axioms/decrees/regulations/statutes/…
Applications
• Mathematics: proof checking, proof generation
• Software/Hardware: formal verification, design
• Programming Languages: Prolog
• Theory: (Descriptive) complexity analysis
• Artificial Intelligence: logical AI
• Databases: query languages
Extensional Reasoning
84
Models
Model: objects and the relationships between them
b
a
c
q
p
d
r
e
p
Satisfaction: p(a,d)
p(a,d)  q(d,c)
p(b,c)
x. p(x,a)
Extensional Reasoning
85
Long-Term Plans
prove(, )
if (should-solve-with-er(, )) then
er-prove(, )
else
traditional-prove(, )
Focus today is
Extensional Reasoning
86
The Challenge
A database represents a single model.
Often we need to check multiple models.
In Extensional Reasoning, we will be
constructing a single model that implicitly
represents multiple models.
Extensional Reasoning
87
Syntactic Manipulation and
Model-based Reasoning
Evaluation Cost
MBR
Syntactic
Manipulation
Information
Complete theory
The number of models increases very rapidly as the
incompleteness of the theory increases.
Extensional Reasoning
88