In this paper, we present a framework of natural language semantics combined with formal ontology to deal with lexical and world knowledge. We build on a framework of Dependent Type Semantics (DTS), a framework of natural language semantics based on dependent type theory. We show how to handle natural language inferences with part-whole relations, in particular, bridging inferences and inferences with the socalled total and partial predicates, in this framework.
Entailment relations are of central importance in the study of formal semantics for natural languages. Generally speaking, the task of determining whether one sentence intuitively entails another sentence requires vast amounts of lexical and world knowledge. Over the past several decades, however, formal semanticists have concentrated on a relatively small set of entailment relations that arise from the compositional structure of a sentence, and in doing so, have abstracted away from how logical inferences interact with a rich body of lexical and world knowledge.
Meanwhile, since the emergence of statistical parsers
based on sophisticated syntactic theories
In this paper, we propose a framework of natural language
semantics combined with formal ontology to deal with
lexical and world knowledge. We build on a framework of
DeCopyright ⃝c 2015 for this paper by its authors. Copying permitted
for private and academic purposes.
pendent Type Semantics (DTS), a framework of natural
language semantics based on dependent type theory
Formal semantics has been developed as sentence semantics and then further extended to discourse semantics in 1980’s. However, the attempt to combine formal semantics with lexical semantics is still underdeveloped. The present paper also aims to contribute to filling this gap, by means of enriching type-theoretical semantics of DTS with a mechanism to handle inferences based on lexical knowledge.
Textual entailment and formal ontology To recognize an entailment relation between sentences requires one to grasp a piece of world knowledge that is not explicitly delivered in given premises. To formally capture the relevant knowledge, we focus on two types of semantic links between concepts: is-a links and part-of links.
The so-called monotonicity inference
Part-of links are used to describe parthood relations
between concepts. An important class of inferences that
depend on part-of links is bridging inference
To establish an anaphoric relation between the underlined
noun phrases, one needs to use the knowledge that a buffet
car is part of a Eurostar. What plays a crucial role in
deriving such a bridging inference is role concept
To derive entailment relations and resolve anaphoric dependencies, one needs to give a formal description of world knowledge and then combine it with semantic representations (SRs) for the premises and conclusion. In this paper, we use a framework of DTS for building semantic representations. The entire system of building semantic representations and deriving entailment relations is pictured in Fig. 1.
Anaphora resolution The complete SR in DTS run(john) Inference
Prover
Yes (valid)
No (invalid)
We use Combinatory Categorial Grammar (CCG) as a
syntactic framework
There are two kind of syntactic categories, basic categories like S, N and N P and complex categories of the forms X=Y and XnY . Complex categories of the form X=Y expect their argument Y to their right, while those of the form XnY expect Y to their left. Categories are combined by an application of combinatory rules. Each rule serves as a meaning composition rule, specifying how to combine the meanings (semantic representations) of expressions into a larger unit. In Fig. 2, the combinatory rule (>) on the left means that an expression having a category X=Y and a meaning f , combined with an expression having a category Y and a meaning a, yields an expression having a category X and a meaning f a. Each meaning is represented as a term. By virtue of this clear connection between syntax and semantics, CCG is particularly suitable for implementing compositional semantics.
X=Y : f X : f a > < DTS (Bekki 2014) is a computational framework of natural language semantics based on dependent type theory. DTS gives a semantic representation for natural language sentences using -types and -types in dependent type theory. -types correspond to universal quantifiers, while types correspond to existential quantifiers. An object of type ( x : A) B(x) is a function f such that for any object a of type A, f a has type B(a). Implication A ! B is a degenerate form of -type: when x does not occur free in B, ( x : A) B(x) is written as A ! B.
An object of type ( x : A) B(x) is a pair (a; b) of an
object a of type A and an object b of type B(a). Conjunction
A^B is a degenerate form of -type: when x does not occur
free in B, ( x : A) B(x) is written as A ^ B. Projection
function 1 and 2 are defined for objects of -types, with
the computation rules: 1(a; b) = a and 2(a; b) = b. See,
e.g.,
In DTS, -types and -types are written as follows: -type ( x : A) B(x)
-type ( x : A) B(x)
if x ̸2 f v(B) (x : A) ! B(x)
A ! B [ x:A ]
B(x) Here f v(B) means the set of free variables occurring in B. DTS uses the following abbreviation for -types. [ x : A ]
B C
2 x:A 3 def 4 [ B ] 5
C Fig.3 shows introduction and elimination rules for -types and -types.
Dependent type theory has been used as an alternative to
dynamic semantics
.
M : B (x : A) ! B : type x:M : (x : A) ! B ( I)
M : (x : A) ! B
N : A M N : B[N=x] ( E)
M :
2(M ) : B[ 1(M )=x]
( E)
picking up a proof term of this type (= proposition) in
terms of 1u we can properly capture the anaphoric
relation between the antecedent quantifier and the pronoun. We
can also capture the accessibility constraints on anaphora
A characteristic of DTS is that it is enriched with
underspecified terms to give a fully compositional analysis of
inferences involving anaphora. In the next section, we will
apply this framework to the analysis of bridging inferences.
Converting world knowledge into DTS formula
We will explain by examples how to convert world
knowledge into DTS formulas. Concepts such as train and wheel in
ontology correspond to 1-place predicates. The part-whole
relation, “x is part of y”, corresponds to the 2-place
predicate x ≼ y, where ≼ is a partial order. Is-a links and part-of
links are converted into DTS axioms in the following way.
Here Entity represents the type of entities, and ! is
rightassociative. We use the graphical notations for the semantic
links
DTS axiom (x : Entity) ! Eurostar(x) ! Train(x)
train wheel is-a p/o
[ y: Entity ] Wheel(y) y ≼ x
(x : Entity) ! Train(x) !
A part-of link has an axiom that derives the existence of the
parts from the whole. It is known that FOL can be
embedded into dependent type theory
Bridging inferences are special in that the antecedent is
inferred given the information explicitly provided in a
previous discourse and some relevant world knowledge
In DTS, the process of searching the antecedent of an anaphoric pronoun, including the case of bridging inferences, is formulated as a process of proof search, so that it can treat anaphora resolution and inferences with world knowledge in a unified way. DTS is augmented with an operator @ to represent anaphoric elements.
As an illustration, consider the discourse in (1) simplified as follows: (3) a. John got on a Eurostar.
b. But the buffet car was not open. (3a) and (3b) are translated as shown in Fig. 4. Lexical entries and CCG-derivations for these sentences are provided in Appendix. In Fig. 4, the two semantic representations (SRs) are conjoined using dynamic conjunction M ; N , which is defined as follows:
M ; N def c: [ u: M c ]
N (c; u) Here c is a proof term that encodes the information provided by the previous discourse; then, the pair (c; u), where u is the proof term for the SR of the first sentence, is passed to the SR of the second sentence. This context-passing mechanism allows us to handle dynamic binding. The bridging inference is triggered by the expression standing for the role concept buffet car, which is represented in terms of an @-operator. In the conjoined SR in Fig. 4, we have the following formula: (4) [ y: Entity
BuffetCar(y) y ≼ @2(c; v) : Entity ] )) A term of the form @ic : is called type annotation, where specifies the type of the term @ic. The underspecified term @i is a function that takes a local context c as argument. In the case of (4), the term @2(c; v) is annotated with the type Entity and the term @1(c; v) with the type corresponding to the proposition “there is a buffet car which is part of @2(c; v)” represented as a -type.
To begin with, we resolve the embedded @-term, that is, @2. The underspecified term @2 takes a local context (c; v) as argument and returns an entity. The type of the @-operator can be specified in terms of type inferences; for instance, the type of @2 can be specified in the following way: (5)
2 2
[ x: Entity u: Eurostar(x) GetOn(j; 1u)
3 Here is the type of the previous context c. The process of resolving anaphora is a process to construct a proof term 2 c: 4
[ x:Entity ] 3 u: Eurostar(x) 5
GetOn(j; 1u) ] 6 v: 4 6 )) = c: 6
66 [ y: Entity } 4 :Open( 1(@1(c; v) : yBu≼ffe@tC2(acr;(vy)) : Entity 7 7 7 ] 77 )) 5 having this type and then replace the @-term by it. In this case, c′: 1( 1( 2c′)) gives a suitable term having the type in (5).
The @1 is a term which requires, given the context (c; v), an object x of type Entity and a proof that x is a buffet car that is part of the entity given by the @2(c; v). The intended anaphoric relation can be obtained by picking out the first element by means of the projection 1. The type of the @1 can be specified in a similar way to (5).
The knowledge required for the present example is given by the part-of relation “Eurostar has a buffet car”, which is translated into the DTS formula (with a proof term w): 2 y: Entity 3 w : (x : Entity) ! Eurostar(x) ! 4 BuffetCar(y) 5 y ≼ x Using this knowledge, we can construct a proof term in question and substitute it for the @1-term. Then we can obtain the following semantic representation for the whole discourse in (3).
(6)
2 c: 66 v: 4 4 2 [ x: Entity ] 3 u: Eurostar(x) 5
GetOn(j; 1u) :Open( 1(w( 1( 1v))( 2( 1v)))) 3
Inferences with total and partial predicates
In this section, we focus on adjectival predicates as an
instance of predicate that requires the interaction between
lexical knowledge and world knowledge. A pair of antonyms
like dirty and clean is known to enable inferences
depending on part-whole relations
(7) a. Are the toys dirty? b. Are the toys clean? If some of the toys are dirty, the answer to the question in (7a) should be “yes”. In the case of (7b), by contrast, unless all of the toys are clean, the answer should be “no”. We call predicates like dirty “partial predicates”, and predicates like clean “total predicate”. Fig. 5 shows typical examples of total predicates and the corresponding partial predicates. For example, as for the pair of open and closed, we can judge that a door is open when it is slightly open, while we usually judge that a door is closed only when it is completely closed.
There is a test which can be applied to distinguish
between total and partial predicates
a. ?It is slightly clean/safe. total predicate
b. It is slightly dirty/dangerous. partial predicate
Another characteristic properly of total and partial
predicates is concerned with entailment patterns: for a pair of
antonyms of total and partial predicates, not only the
assertion (P ) of one form entails the negation (:N ) of the other,
but also the negation (:N ) of one form entails the assertion
(P ) of the other
a. clean ) not dirty b. dirty ) not clean a. not clean ) dirty b. not dirty ) clean P ) :N P ) :N :P ) N :P ) N In the case of standard degree adjectives such as small, the assertion (P ) of one form entails the negation (:N ) of the other, but the converse does not hold; thus, not small does not entail large and not large does not entail small. For the proper treatment of inferences with lexical knowledge, it is important to specify such differences in entailment patterns for antonyms.
The lexical knowledge concerning partial and total predicates is conversed into DTS axioms as follows. Here E is an abbreviation for Entity. total predicate
(x : E) ! (y : E) ! clean(x) ! y ≼ x ! clean(y) partial predicate
(x : E) ! (y : E) ! dirty(x) ! x ≼ y ! dirty(y) A total predicate holds of a part if it holds of its whole; by contrast, a partial predicate holds of the whole if it holds p :
Premise [ train(a) ]
clean(a) 2p : clean(a) ( E) x : E (2) f ax : clean(a) ! x ≼ a ! clean(x) ( E)
Axiom for the total predicate “clean” a : E f : (x : E) ! (y : E) ! clean(a) ! x ≼ a ! clean(x) f a : (y : E) ! clean(a) ! y ≼ a ! clean(y) ( E) ( E) x:f ax( 2p)( 2q) : q x:f ax( 2p)( 2q) : (x : E) ! [ window(x) ] x ≼ a
! clean(x) [ window(x) ] x ≼ a ! clean(x) f ax( 2p)( 2q) : clean(x) f ax( 2p) : x ≼ a ! clean(x)
( E) ( I); (1) [ window(x) ] (1) x ≼ a 2q : x ≼ a
( E) of its part. The entailment patterns of antonym pairs can be converted in a similar way; we omit the details here.
As an illustration of how an inference is derived using lexical and world knowledge, consider the following example: (12)
Premise : Conclusion :
The train is clean.
The windows are clean.
Fig.6 shows a derivation of this inference. Here, the subject train in the premise is represented by the constant a of type E, thus we assume a : E in the derivation. The subject the windows in the conclusion has to be interpreted as the train’s windows via a bridging inference. For simplicity, we assume a semantic representation after resolving the bridging for the conclusion in (12). The axiom for total predicates is available for the predicate clean: we use the term f for the proof term of this axiom.
Predicates functioning and broken are antonyms that can be taken as total and partial predicates, respectively; given that a brake is part of a train, the following inferences are naturally taken to be valid, while the opposite directions are not.
The train is functioning The brake is functioning The brake is broken The train is broken ) ) However, the same inference does not hold for the following pair of examples, even if a window is part of a train.
The train is functioning
The window is broken ̸) ̸) This suggests that the proper treatment of inferences with predicates functioning and broken will involve some additional complexity. A detailed investigation of this issue is left for another occasion.
The window is functioning
The train is broken
In this paper, we have presented a framework combining DTS with formal ontology to handle inferences involving knowledge of part-whole relations. We have showed how to formalize bridging inferences and inferences with partial and total predicates, both being sensitive to part-whole relations among structured objects.
The inference component in our framework can be implemented using a modern proof assistant based on dependent Syntactic category : Semantic representation N P : j V P nN P : ( yxc)GetOn(x; y)
2 V P n(V P=N P )=N : ( npxc) 4 N : ( xc)Eurostar(x) (S=V P )=N : ( npc)(p 1(@ic) :
[ BuffetCar(x) N : ( xc) x ≼ @ic : Entity V P=V P : ( pxc)(pxc) V P=V P : ( pxc)(:pxc) V P : ( xc) Open(x) ]
[ y : Entity ] 3
u : nyc 5
p( 1u)xc
[ x : Entity ]
nxc
)
type theory such as Coq, which has been applied to the
formalization of natural language inferences
We thank the three anonymous reviewers for helpful comments and suggestions. We also thank Riichiro Mizoguchi and Masaharu Yoshioka for useful discussions. This work was supported by MEXT/JSPS KAKENHI Grant Number #15K00301 and #26770009.
Fig. 7 provides lexical entires for the example in (3). Here V P is an abbreviation of the syntactic category SnN P in CCG. Compositional derivations of (3a) and (3b) are given in Fig. 8 and Fig. 9, respectively.
John NP : j
got on (SnNP )=NP : ( yxc)GetOn(x; y) [ x : Entity ]) nxc
N : ( xc) S=(SnNP )
2 x : Entity : ( pc)(p 1(@1c)c : 64 BuffetCar(x) x ≼ @2c : Entity 3 (SnNP )n((SnNP )=NP ) : ( pxc) 64 u : [ yEu:roEsnttairt(yy) ] 73
5 p( 1u)xc < >
was (SnNP )=(SnNP ) : ( pxc)(pxc) 2 x : Entity S : c::Open( 1(@1c) : 64 BuffetCar(x) x ≼ @2c : Entity 3
open Bekki, D. 2010. A Formal Theory of Japanese Grammar: The Conjugation System, Syntactic Structures, and Semantic Composition. Kuroshio.
Bekki, D. 2014. Representing anaphora with dependent types. In LACL 2014, volume 8535 of Lecture Notes in Computer Science. Springer. 14–29.