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.
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/919039
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact