Pointing to places in a deductive geospatial theory

Pointing to places in a deductive geospatial theory Richard Waldinger Artificial Intelligence Center SRI International waldinger@ai.sri.com Peter Jarvis Artificial Intelligence Center SRI International jarvis@ai.sri.com Jennifer Dungan Ecosystem Science and Technology Branch NASA Ames Research Center jennifer@gaia.arc.nasa.gov Abstract Issues in the description of places are discussed in the context of a logical geospatial theory. This theory lies at the core of the system Ge- oLogica, which deduces answers to geographi- cal questions based on knowledge provided by multiple agents. 1 Introduction Many questions cannot be answered from information in a single geographical source; often the answer must be deduced from information provided by several sources. It may not be obvious which sources to consult. Because multiple sources seldom agree on conventions of nomen- clature or notation, it becomes a problem to determine what place corresponds to a particular description. The same name may apply to many places, and the same place may have many names. In the system GeoLogica, the coordination between multiple information sources is carried out by an auto- mated deduction system, or theorem prover, that operates in a formal geospatial theory. GeoLogica differs from a search engine in that, instead of merely finding a list of documents with vocabulary that matches the question, it attempts to understand the question and provide an an- swer. In developing this system, we have been forced to de- velop systematic ways for naming places, and for identi- fying places corresponding to given descriptions. In this paper, we shall first describe the GeoLogica sys- tem. We’ll present the representation of place names and discuss mechanisms for finding places corresponding to a given description. We’ll discuss the solution of a sample problem, mention some related work, and describe pro- posed extensions. 2 Outline of GeoLogica Questions are posed to GeoLogica in a subset of English and translated into logic by a natural language parser, the system Gemini (Dowding et al., 1993). The logi- cal form of the question is rephrased as a theorem and presented to the theorem prover SNARK (Stickel et al., 2000). (A knowledgeable user of GeoLogica may pre- fer to bypass the parser and phrase the query directly in logical form.) The geospatial theory that SNARK uses for this application consists of a set of axioms, logical sentences that provide definitions and describe properties of important spatial constants, functions, and relations, including those in the logical form of the query. When SNARK proves a theorem, it shows that the theorem fol- lows logically from the axioms in the theory. SNARK also has an answer-extraction mechanism; in addition to proving the validity of the theorem, it can extract from the proof an answer to the query encoded in the theorem, us- ing mechanisms originally developed for automated pro- gram synthesis as well as question answering.(Manna and Waldinger, 1980) Using the appropriate axioms, SNARK transforms and decomposes the query to simpler and simpler subqueries. If the right subqueries of the query are answered, SNARK can extract the answer to the main query from …

Content truncated to 500 words