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.
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 |