Sciweavers

Share
JSC
2000

Goals and Benchmarks for Automated Map Reasoning

12 years 1 months ago
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.
Andrea Formisano, Eugenio G. Omodeo, Marco Temperi
Added 19 Dec 2010
Updated 19 Dec 2010
Type Journal
Year 2000
Where JSC
Authors Andrea Formisano, Eugenio G. Omodeo, Marco Temperini
Comments (0)
books