New successes in dealing with set-theories by means of state-of-the-art theorem-provers may ensue from terse and concise axiomatic systems, such as can be moulded in the framework of the (fully equational) Tarski-Givant formalism of dyadic relations, here named ‘maps’. This paper sets the ground for systematic experimentation based on such axiomatic systems. On top of a kernel axiomatization of map algebra, we develop a layered formalization of basic set-theoretic concepts. A number of concrete experiments have been carried out in this framework, as the paper reports, with the assistance of a first-order theorem-prover. The aim is to assess the potential usefulness of the proposed layered

Layered map reasoning: An experimental approach put to trial on sets

FORMISANO, Andrea;
2001

Abstract

New successes in dealing with set-theories by means of state-of-the-art theorem-provers may ensue from terse and concise axiomatic systems, such as can be moulded in the framework of the (fully equational) Tarski-Givant formalism of dyadic relations, here named ‘maps’. This paper sets the ground for systematic experimentation based on such axiomatic systems. On top of a kernel axiomatization of map algebra, we develop a layered formalization of basic set-theoretic concepts. A number of concrete experiments have been carried out in this framework, as the paper reports, with the assistance of a first-order theorem-prover. The aim is to assess the potential usefulness of the proposed layered
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11391/119318
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 13
  • ???jsp.display-item.citation.isi??? ND
social impact