A Logic Prover for Text Processing

1 Introduction

Automated reasoning has been applied to many application areas [Wos 1988], but little work was done towards applying it to text processing. The challenges faced when using auto­ mated reasoning for text processing are: logic representation of open text, need of world knowledge axioms, logic repre­ sentation of semantically equivalent linguistic patterns, and others.

In this paper we argue that considerable progress was made in key areas of natural language processing and it is possible to implement logic provers for some specific NLP applica­ tions. One such application is Question Answering where the problem is to find exact answers to questions expressed in natural language by searching a large collection of doc­ uments [Voorhees 2002]. We have implemented a Logic Prover for QA, called COG EX. Integrated into a QA system, the Prover captures the syntax-based relationships such as the syntactic objects, syntactic subjects, prepositional attach­ ments, complex nominals, and adverbial/adjectival adjuncts provided by the logic representation of text. In addition to the logic representations of questions and candidate answers, the QA Logic Prover uses world knowledge axioms to link ques­ tions to answers. These axioms are provided by the WordNet glosses represented in logic forms. Additionally, the prover implements rewriting procedures for semantically equivalent lexical patterns. With this deep and intelligent representa­ tion, COGEX effectively and efficiently re-ranks candidate answers by their correctness and ultimately eliminates incor­ rect answers. In this way, the Logic Prover is a powerful tool in boosting the accuracy of the QA system. Moreover, the trace of a proof constitutes a justification for that answer.

2 Logic Prover Inputs and Outputs

A logic form provides a one to one mapping of the words of the text into the first order logic predicates. The predicate names consist of the base form of the word concate­ nated with the part of speech of the word [Moldovan and Rus 2001]. An important feature of the Logic Form representation is the fixed-slot allocation mechanism of the verb predicates [Hobbs 1993].

The term Question Logic Form (QLF) refers to the ques­ tions posed to the Question Answering system in logic form.

Question: Which company created the Internet Browser Mo­ saic?

QLF: _organization...AT(x2) ) & company .NN(x2) & cre­ ate_VB(e1,x2,x6) & Internet.NN(x3) & browser .NN(x4) & Mosaic.NN(x5) & nn.NNC(x6,x3,x4,x5)

The term Answer Logic Form (ALF) refers to the candidate answers in logic form. Candidate answers are provided by the Question Answering system [Moldovan 2002].

Answer: In particular, a program called Mosaic, developed by the National Center for Supercomputing Applications ( NCSA) at the University of Illinois at Urbana - Champaign , is gaining popularity ....

ALF: In..JN(x 1 ,x28) & particulaLJJ(x29) & progra11LNN(x 1) & caiLVB(e1,x27,x30) & Mosaic_NN(x2) & develop_VB(e2,x2,x31) & by_IN(e2,x8) & NationaLNN(x3) & Center_NN(x4) & for_NN(xS) & Supercomputing_NN(x6) & app1ica­ tion_NN(x7) & nn_NNC(x8,x3,x4,x5,x6,x7) & NCSA_NN(x9) & at..JN(e2,x15) & University_NN(x10) & oLNN(x11) & Illinois_NN(x12) & aLNN(x13) & Urbana._NN(x14) & nn_NNC(x15,x!O,x11,x12,x13,x14) & ChampaigrLNN(x16) & gain_VB(e3,x1,x17) & popularity_NN(x17) ...

Logic representation ofWordNet glosses

A major problem in QA is that often an answer is expressed in words different from those in the question. World knowl­ edge is necessary to conceptually link questions to answers. WordNet glosses contain a source of world knowledge. To be useful in automated reasoning, the glosses need to be trans­ formed into logic forms. Taking the same approach as for open text, we have parsed and represented in logic forms more than 50,000 WordNet glosses.

The question contains the verb create while the answer contains the verb develop. In order to prove that this answer is in fact correct, we need to detect and use a lexical chain between develop and create. WordNet supplies us with that chain such that: develop t+ make and make t+ create.

NLP Axioms

In addition to world knowledge axioms, a QA Logic Prover requires linguistic knowledge. This is what distinguishes an NLP prover from a traditional mathematical prover. General axioms that reflect equivalence classes of linguistic patterns need to be created and instantiated when invoked. We call these NLP axioms and show some examples below. More details are presented in [Moldovan 2003].

I. Complex nominals and coordinated conjunctions. An ax­ iom is built such that the head noun of the complex nominal in the question implies the entire noun phrase:

all xl (mosaic_nn(xl) ~ internet_nn(xl) & browser_nn(xl) & mosaicJln(xl))

2. Appositions. An apposition implies that the two noun phrases in the apposition "stand for" each other. " . .Italian Andrea Pfister, designer of the 1979 "bird cage "shoe ... uses an apposition to describe the designer. An axiom is built to link the head of the noun phrases in the apposition such that they share the same argument.

• all xl2 xl3 xl4 xiS xl6 xl7 xiS xl9 (italian..nn(xl2) & an­ drea_nn(x 13) & pfister_NN(x 14) & nn._nnc(xl5,xl2,x 13,x 14) & de­ signer_nn(x 16) & oLin(x 16,x 17) & 1979_nn(xl7) & bird..nn(x 18) & cage_nn(x 19)) -+ designer_nn(xl5) & oLin(x IS,x 17))
• Part-of relations in location questions. A location seeking question may have a candidate answer that identifies a location by referring to a part of the location. For example, an axiom is built to connect Wyoming to its part:
• all xl x2 x3 (corner_nn(xl) & ofjn(xl,x2) & wyoming_nn(x2) ~ wyomingJln(xl))
• Attribute of relations in quantity seeking questions. An axiom is built to connect the quantity to its subject, redwood: all xl x2 (_quantity _(xl) & redwood.NN(x2) ~of jn(xl,x2))
• Translating words from noun form to verb form. Axioms are built to link nouns with verbs. For example the noun seizure is linked to the verb seize, by filling the object with the tail of the predicate attached to seizure, and assigning the event argmuent to be the argument of the noun predicate for seizure.

all x7 x8 x9 (its_prp(x8,x7) & seizureJln(x8) & of jn(x8,x9) ~ seize_vb(x8,x7,x9))

3 Control Strategy

The search strategy used is the Set of Support Strategy [Wos 1988]. Axioms placed in the Usable list are: (1) Extended WordNet axioms, (2) NLP axioms, and (3) axioms based on outside world knowledge, such as people and organiza­ tions. The inference rule sets are based on hyperresolution and paramodulation.

When the proof fails, we devised a way to incrementally relax some of the conditions that hinder the completion of the proof. This relaxation process puts weights on the proof such that proofs weaker than a predefined threshold are not accepted.

4 Results

COGEX was implemented and integrated into a state-of-the­ art Question Answering system that participated in TREC 2002 [Moldovan 2003] . All questions are attempted by the prover, but if the proof fails the QA system resorts to other answer extraction methods that were part of the system be­ fore the prover. Thus, some questions are answered by the QA system without the prover, some only by the prover and some by both the non-prover system and the prover. The complete system answered 415 questions out of 500 TREC 2002 questions. Of these, 206 were answered by COGEX. A careful analysis indicates that the QA system without logic prover answered 317 questions and the prover can answer only 98 additional questions for which the system without prover failed. Table 1 summarizes these results. The added

value of automated reasoning to the QA system is 30.9% (or 98/317). The failures of the prover are due primarily to the lack of linguistic axioms.

Acknowledgment

This work was supported in part by the ARDA AQUAINT program.