Title of article :
Goals and Benchmarks for Automated Map Reasoning
Author/Authors :
ANDREA FORMISANO and ENRICO PONTELLI، نويسنده , , Eugenio G. Omodeo، نويسنده , , Marco Temperini، نويسنده ,
Issue Information :
روزنامه با شماره پیاپی سال 2000
Pages :
39
From page :
259
To page :
297
Abstract :
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.
Journal title :
Journal of Symbolic Computation
Serial Year :
2000
Journal title :
Journal of Symbolic Computation
Record number :
805428
Link To Document :
بازگشت