Goals and benchmarks for automated map reasoning

Tarski-Givant's map calculus is briefly reviewed, and a plan of research is outlined aimed at investigating applications of this ground equational for malism in the theorem-proving field. The main goal is to create synergy bet ween first-order predicate calculus and the map calculus. Techniques for tr anslating isolated sentences, as well as entire theories, from first-order logic into map calculus are designed, or in some cases simply brought neare r through the Exercise of specifying properties of a few familiar structure s (natural numbers, nested lists, finite sets, lattices). It is also highli ghted to what extent a state-of-the-art theorem-prover for first-order logi c, namely Otter, can be exploited not only to emulate, but also to reason a bout, map calculus. Issues regarding "safe" forms of map reasoning are sing led out, in sight of possible generalizations to the database area. (C) 200 0 Academic Press.