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.
Provable \exixts∗\forall-sentences about sets with atoms
FORMISANO, Andrea;
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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
