IRIS - Res&Arch Institutional Research Information System - Research & Archive
Anagrafe della Ricerca dell'Università degli Studi di Perugia.
EnglishTiny equational theories of aggregates, where each \exists*\forall-sentence is either provable or refutable, are tersely specified in the map calculus. Three kinds of aggregates are considered: pure sets, pure hypersets, and sets involving atoms---atoms being treated as self-singletons. A known approach to deciding \exists*\forall-validity, which reduces the single $\forall$ to occurrences of restricted universal quantifiers, is adapted from the pure case to the case of atoms. A problem tightly related to the one of \exists*\forall-validity, namely unification for the set/hyperset constructs (\emptyset, with), is solved for sets with self-singleton atoms through a novel goal-driven algorithm.
Scheda prodotto non validato
Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo
| Titolo: | Provable \exixts∗\forall-sentences about sets with atoms |
| Autori: | |
| Data di pubblicazione: | 1999 |
| Abstract: | Tiny equational theories of aggregates, where each \exists*\forall-sentence is either provable or refutable, are tersely specified in the map calculus. Three kinds of aggregates are considered: pure sets, pure hypersets, and sets involving atoms---atoms being treated as self-singletons. A known approach to deciding \exists*\forall-validity, which reduces the single $\forall$ to occurrences of restricted universal quantifiers, is adapted from the pure case to the case of atoms. A problem tightly related to the one of \exists*\forall-validity, namely unification for the set/hyperset constructs (\emptyset, with), is solved for sets with self-singleton atoms through a novel goal-driven algorithm. |
| Handle: | http://hdl.handle.net/11391/919039 |
| Appare nelle tipologie: | 4.1 Contributo in Atti di convegno |
File in questo prodotto:
Copyright © 2020