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 formalism in the theorem-proving field. The main goal is to create synergy between first-order predicate calculus and the map calculus. Techniques for translating isolated sentences, as well as entire theories, from first-order logic into map calculus are designed, or in some cases simply brought nearer through the exercise of specifying properties of a few familiar structures (natural numbers, nested lists, finite sets, lattices). It is also highlighted to what extent a state-of-the-art theorem-prover for first-order logic, namely Otter, can be exploited not only to emulate, but also to reason about, map calculus. Issues regarding “safe" forms of map reasoning are singled out, in sight of possible generalizations to the database area.