A Logic of Arbitraryand Indefinite Objects: A Logic of Arbitrary and Indefinite Objects Stuart C. Shapiro
Department of Computer Science and Engineering,
and Center for Cognitive Science
University at Buffalo, The State University of New York
201 Bell Hall, Buffalo, NY 14260-2000
shapiro@cse.buffalo.edu
http://www.cse.buffalo.edu/~shapiro/
Collaborators: Collaborators Jean-Pierre Koenig
David R. Pierce
William J. Rapaport
The SNePS Research Group
What Is It?: What Is It? A logic
For KRR systems
Supporting NL understanding & generation
And commonsense reasoning
LA
Sound & complete via translation to Standard FOL
Based on Arbitrary Objects, Fine (’83, ’85a, ’85b)
And ANALOG, Ali (’93, ’94), Ali & Shapiro (’93)
Outline of Paper: Outline of Paper Introduction and Motivations
Introduction to Arbitrary Objects
Informal Introduction to LA
Formal Syntax of LA
Translations Between and LA Standard FOL
Semantics of LA
Proof Theory of A
Soundness & Completeness Proofs
Subsumption Reasoning in LA
MRS and LA
Implementation Status
Outline of Talk: Outline of Talk Introduction and Motivations
Informal Introduction to LA
with examples
Basic Idea: Basic Idea Arbitrary Terms
(any x R(x))
Indefinite Terms
(some x (y1 … yn) R(x))
Motivations : Motivations See paper for other logics
that each satisfy some of these motivations
Motivation 1Uniform Syntax: Motivation 1 Uniform Syntax Standard FOL:
White(Dolly)
x(Sheep(x) White(x))
x(Sheep(x) White(x))
LA:
White(Dolly)
White(any x Sheep(x))
White(some x ( ) Sheep(x))
Motivation 2Locality of Phrases: Motivation 2 Locality of Phrases Every elephant has a trunk.
Standard FOL
x(Elephant(x) y(Trunk(y) Has(x,y))
LA:
Has(any x Elephant(x), some y (x) Trunk(y))
Motivation 3Prospects for Generalized Quantifiers: Motivation 3 Prospects for Generalized Quantifiers Most elephants have two tusks.
Standard FOL
??
LA:
Has(most x Elephant(x), two y Tusk(y))
(Currently, just notation.)
Motivation 4Structure Sharing: Motivation 4 Structure Sharing any x Elephant(x) some y ( ) Trunk(y) Has( , ) Flexible( ) Every elephant has a trunk. It’s flexible.
Quantified terms are “conceptually complete”.
Fixed semantics (forthcoming).
Motivation 5Term Subsumption: Motivation 5 Term Subsumption Hairy(any x Mammal(x))
Mammal(any y Elephant(y))
Hairy(any y Elephant(y))
Pet(some w () Mammal(w))
Hairy(some z () Pet(z)) Hairy Mammal Elephant Pet
Outline of Talk: Outline of Talk Introduction and Motivations
Informal Introduction to LA
with examples
Quantified Terms: Quantified Terms Arbitrary terms:
(any x [R(x)])
Indefinite terms:
(some x ([y1 … yn]) [R(x)])
Compatible Quantified Terms : (Q v ([a1 … an]) [R(v)]) (Q u ([a1 … an]) [R(u)])
(Q v ([a1 … an]) [R(v)]) (Q v ([a1 … an]) [R(v)])
Compatible Quantified Terms different
or
same All quantified terms in an expression must be compatible.
Quantified Terms in an Expression Must be Compatible: Quantified Terms in an Expression Must be Compatible Illegal:
White(any x Sheep(x)) Black(any x Raven(x))
Legal
White(any x Sheep(x)) Black(any y Raven(y))
White(any x Sheep(x)) Black(any x Sheep(x))
Capture: Capture White(any x Sheep(x)) Black(x)
White(any x Sheep(x)) Black(x) bound free same Quantifiers take wide scope!
Examples of Dependency: Examples of Dependency Has(any x Elephant(x), some(y (x) Trunk(y))
Every elephant has (its own) trunk.
(any x Number(x)) < (some y (x) Number(y))
Every number has some number bigger than it.
(any x Number(x)) < (some y ( ) Number(y))
There’s a number bigger than every number.
Closure: Closure x … contains the scope of x
Compatibility and capture rules
only apply within closures.
Closure and Negation: Closure and Negation White(any x Sheep(x))
Every sheep is not white.
x White(any x Sheep(x))
It is not the case that every sheep is white.
White(some x () Sheep(x))
Some sheep is not white.
x White(some x () Sheep(x))
No sheep is white.
Closure and Capture: Closure and Capture Odd(any x Number(x)) Even(x)
Every number is odd or even.
x Odd(any x Number(x))
x Even(any x Number(x))
Every number is odd or every number is even.
Tricky Sentences:Donkey Sentences: Tricky Sentences: Donkey Sentences Every farmer who owns a donkey beats it.
Beats(any x Farmer(x)
Owns(x, some y (x) Donkey(y)),
y)
Tricky Sentences:Branching Quantifiers: Tricky Sentences: Branching Quantifiers Some relative of each villager and some relative of each townsman hate each other.
Hates(some x (any v Villager(v)) Relative(x,v),
some y (any u Townsman(u)) Relative(y,u))
Closure & Nested Beliefs(Assumes Reified Propositions): Closure & Nested Beliefs (Assumes Reified Propositions) There is someone whom Mike believes to be a spy.
Believes(Mike, Spy(some x ( ) Person(x))
Mike believes that someone is a spy.
Believes(Mike, xSpy(some x ( ) Person(x))
There is someone whom Mike believes isn’t a spy.
Believes(Mike, Spy(some x ( ) Person(x))
Mike believes that no one is a spy.
Believes(Mike, xSpy(some x ( ) Person(x))
Current Implementation Status: Current Implementation Status Partially implemented as the logic of SNePS 3
Summary: Summary LA is
A logic
For KRR systems
Supporting NL understanding & generation
And commonsense reasoning
Uses arbitrary and indefinite terms
Instead of universally and existentially quantified variables.
Arbitrary & Indefinite Terms: Arbitrary & Indefinite Terms Provide for uniform syntax
Promote locality of phrases
Provide prospects for generalized quantifiers
Are conceptually complete
Allow structure sharing
Support subsumption reasoning.
Closure: Closure Contains wide-scoping of quantified terms