First-order logic (FOL) is undecidable - that is, no algorithm exists that can decide whether a formula of FOL is valid or not. However, there are various fragments of FOL that are known to be decidable. FO2, the two-variable fragment of FOL, is one of such languages [1, 2]. FO2 is a first-order language where formulas have maximally two variables, no function symbols, but possibly do have equality. FO2 has the finite model property [1], which means that if a formula of FO2 is satisfiable, it is satisfiable in a finite model. In this paper we propose a controlled fragment of Discourse Representation Theory (DRT, [3]) with a semantics formalised on the basis of the two-variable fragment with equality. DRT encapsulates the idea of text interpretation that “one and the same structure serves simultaneously as content and context” [4], where content refers to the semantic interpretation of sentences already processed, and context serves in aiding the interpretation of anaphoric expressions in subsequent sentences. However, providing a two-variable natural language fragment is, in itself, not a new idea. In fact, the framework presented here is very much inspired by Ian Pratt-Hartmann's language E2V [5]. But as Pratt-Hartmann himself notes, E2V is “certainly not proposed as a useful controlled language”. Our aim is to try to find out how useful a controlled language based on the two-variable fragment actually can be, mostly from a computational linguistic point of view. We will do this by: - defining a transparant translation from the DRT fragment to FO2; - including events, thematic roles, pronouns, and plurals in the fragment; - specifying a syntax-semantics interface.
The syntax-semantic interface of our choice will be based on combinatory categorial grammar (CCG, [6]), rather than, say, a simple definite clause grammar. Because of its type transparency principle, CCG will enable us to set up a clean interface, where each syntactic category uniformly corresponds to a semantic type. CCG gives us further means for incremental processing [6], and large databases of texts annotated with CCG-derivations are available [7], which might aid us in enlarging the lexicon for practical applications.
The fragment of DRT that we introduce here, blessed Economical DRT, is decidable, because we can (rather straightforwardly) show that EDRT can be translated to FO2. An EDRS (Economical Discourse Representation Structure) is an ordered pair [D,C] where D stands for the domain (a possibly empty set of discourse referents), and C is a set of EDRS-conditions. Unlike standard DRT, the domain of an EDRS has at most one discourse referent. There are only two discourse referents, named “1” and “2”. This restriction doesn’t mean that we can only name two different discourse referent in an EDRS — we may re-use discourse referents as often as we like, nested in sub-EDRSs. Examples below will illustrate this technique. We will use the box-notation of DRSs in examples below, or, for convenience, a flat notation in definitions and alike. EDRS-conditions are recursively defined as follows: If P is a one-place predicate symbol, and u is a discourse referent, then P(u) is an EDRS-condition; If R is a two-place predicate symbol, and u and u0 are discourse referents, then R(u,u0) is an EDRS-condition; If u and u0 are discourse referents, then u = u0 is an EDRS-condition; If B is an EDRS, then +B and −B are EDRS-conditions; If B1 and B2 are EDRSs, then B1⇒B2 and B1∨B2 are EDRS-conditions; Nothing else is an EDRS-condition. Most of these resemble the normal DRS-conditions, with two exceptions: −B marks negative information, and +B marks positive information.
The EDRS language is interpreted by translation to FO2 with the aid of the function [.]fo2. This function is defined for discourse referents, EDRS-conditions, and EDRSs. This translation always produces a formula of FO2, simply because it only yields at most two different variables (x and y):
[< ∅, {c1, . . . , cn} >]fo2 = ([c1]fo2 ∧ . . . ∧ [cn]fo2) [< {u}, {c1, . . . , cn} >]fo2 = ∃[u]fo2([c1]fo2 ∧ . . . ∧ [cn]fo2) [< ∅, {c1, . . . , cn} >⇒B]fo2 = ([c1]fo2 ∧ . . . ∧ [cn]fo2) → [B]fo2) [< {u}, {c1, . . . , cn} >⇒B]fo2 = ∀[u]fol2([c1]fo2 ∧ . . . ∧ [cn]fo2) → [B]fo2) [B1∨B2]fo2 = ([B1]fo2 ∨ [B2]fo2) [+B]fo2 = [B]fo2 [−B]fo2 = ¬[B]fo2 [u=u0]fo2 = [u]fo2 = [u0]fo2 [R(u,u0)]fo2 = R([u]fo2,[u0]fo2) [P(u)]fo2 = P([u]fo2) [1]fo2 = x [2]fo2 = y
We borrow some terminology of standard DRT to clarify the concepts subordination, accessibility, and insertability. Given an EDRS B, a DRS B1 subordinates a DRS B2 if and only if +B2 is a condition of B1, −B2 is a condition of B1, B∨B2 is a condition of B1, B2∨B is a condition of B1, B2⇒B is a condition of B1, B1⇒B2 is a condition of B, or B1 subordinates B, and B subordinates B2. A discourse referent in a DRS B is accessible from a DRS B0 if B subordinates B0, or if B=B0. A DRS can be inserted into B (B is insertable) if B is not subordinated to any other DRS (i.e., is the outermost DRS), or if +B is a condition of B0 and B0 is insertable.
Accessibility is an important notion in DRT for establishing anaphoric links. Our EDRS language inherits the nice properties of accessibility of antecedents of pronouns, but also controls the use of pronouns by adding further restrictions on the structure of discourse. Insertability is the EDRT concept for conjoining sentences — below we will illustrate this mechanism. 3
We use a sortal ontology to distinguish between event, collection, and individual (they are all disjoint concepts). This is coded as background knowledge and can be straigthforwardly specified as axioms of FO2. We adopt a neo-Davidsonian representation of events. Thematic roles are two-place relations between events and other entities. We use the inventory of VerbNet to assign thematic roles to verbal arguments [8], such as agent, patient and theme. The neo-Davidsonian representation is central to our technique of re-using discourse referents, as illustrated by the examples below.
No man who loves a woman whistles.
There are several linguistic constraints implied by this fragment. First of all, a sentence can have at most one universal quantifier (triggered by, for instance, every or no). The current syntax-semantic interface requires this to be the subject noun phrase. Similarly, a sentence can have only one pronoun referring back to an antecedent in a previous sentence. Different insertability possibilities allow a pronoun to have several possible antecedents. For instance, in the example above, a DRS for the sentence “She smiled” could be inserted in the deepest embedded +DRS, thereby establishing an anaphoric link between the third-person pronoun and “a woman”. Proper names (and definite descriptions) trigger a uniqueness presupposition, accommodated as part of the background knowledge. Uniqueness statements can obviously be represented with two variables — an an example consider the proper name Lou and the presupposition ∀x∀y((lou(x)∧lou(y))→x=y).
A man saw a woman.
1
man(
2
+
see(
1
+
woman(
1
+
woman(
To obtain syntactic structure we employ a categorial grammar with basic categories n, np, s, pp (the notation of slashes follows CCG). Each syntactic category corresponds to a (typed) partial EDRS. Because we only have two different discourse referents, β-conversion with renaming of variables to overcome accidental capture of free variables is not needed — instead it is safe to use unification for substitution. We will do so with a two-place operator (A·B), similar to lambdaabstraction, where B is always an EDRS, and A discourse referent or another dot operation. Partial EDRSs can also only contain at most two distinct discourse referents.
Cat
Partial EDRS
Tokens
n (1·h∅, {car(
We adopt a theory of collections to model plurals [9]. Membership is stated by a two-place relation between individuals and collections, for convenience designated by the ∈ symbol. Two example EDRSs with respectively a counting quantifier and summation, are shown on the next page. Both examples illustrate the distributive reading. The collective reading can also be obtained by relating the thematic role of the event directly with the discourse referent denoting the collection. The interpretation of the counting quantifier is defined by meaning postulates and part of the background knowledge. Here we show how it can be done by using at most two variables for the cardinal two. The first of these axioms says that a collection with the property “two” has two members, and the second states that these are distinct members. It should be clear that the method can be extended to numerals with higher cardinality, without resorting to more than two variables.
∀x(two(x) → (∃y first-member(x,y) ∧ ∃y second-member(x,y))) ∀x(two(x) → ¬∃y(first-member(x,y) ∧ second-member(x,y))) ∀x∀y(first-member(x,y) → x∈y) ∀x∀y(second-member(x,y) → x∈y)
Two men walk.
2
1 ∈ 2
1
1 ∈ 2
⇒
⇒
man(
1 1 1 ∈ 2 ⇒ +
1
2
+
walk(
The presented DRT fragment is of course far more restricted than the full blown version of DRT (EDRT cannot represent donkey sentences). Nevertheless, we hope to have shown that the two-variable fragment has some potential for (quasi) natural language applications. For instance, the use of neo-Davidsonian eventstyle semantics has no restrictions on the number of modifiers (but it does on pronouns or universal quantified noun phrases).
This is work in progress. Space limitations forced us to leave out a number of issues. In a more elaborated paper we plan to further illustrate incremental parsing, the generation of background knowledge axioms, and the syntax-semantic interface for plurals.