Abstract
In this paper we consider the relative expressive power of two very common operators applicable to sets and multisets: the with and the union operators. For such operators we prove that they are not mutually expressible by means of existentially quantified formulae. In order to prove our results, canonical forms for set-theoretic and multiset-theoretic formulae are established and a particularly natural axiomatization of multisets is given and studied.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Aliffi, D., Dovier, A., Rossi, G.: From set to hyperset unification. Journal of Functional and Logic Programming 1999(10), 1–48 (1999)
Arenas-Sánchez, P., Dovier, A.: A minimality study for set unification. Journal of Functional and Logic Programming 1997(7), 1–49 (1997)
Baader, F., Búttner, W.: Unification in commutative and idempotent monoids. Theoretical Computer Science 56, 345–352 (1988)
Baader, F., Schulz, K.U.: Unification theory. In: Bibel, W., Schmidt, P.H. (eds.) Automated Deduction: A Basis for Applications. Foundations: Calculi and Methods, vol. 1. Kluwer Academic Publishers, Dordrecht (1998)
Bernays, P.: A system of axiomatic set theory. Part I. The Journal of symbolic logic 2, 65–77 (1937)
Cantone, D., Ferro, A., Omodeo, E.G.: Computable Set Theory. Int’l Series of Monographs on Computer Science, vol. 1. Clarendon Press, Oxford (1989)
Dantsin, E., Voronkov, A.: A nondeterministic polynomial-time unification algorithm for bags, sets and trees. In: Thomas, W. (ed.) FOSSACS 1999. LNCS, vol. 1578, pp. 180–196. Springer, Heidelberg (1999)
Dovier, A.: A Language with Finite Sets Embedded in the CLP Scheme. In: Dyckhoff, R. (ed.) ELP 1993. LNCS, vol. 798, pp. 77–93. Springer, Heidelberg (1994)
Dovier, A.: Computable Set Theory and Logic Programming. PhD thesis, Universitá degli Studi di Pisa, TD-1/96 (March 1996)
Dovier, A., Omodeo, E.G., Pontelli, E., Rossi, G.: {log} : A Language for Programming in Logic with Finite Sets. J. of Logic Programming 28(1), 1–44 (1996)
Dovier, A., Piazza, C., Pontelli, E., Rossi, G.: On the Representation and Management of Finite Sets in CLP-languages. In: Jaffar, J. (ed.) Proc. of 1998 Joint Int’l Conf. and Symp. on Logic Programming, pp. 40–54. The MIT Press, Cambridge (1998)
Dovier, A., Piazza, C., Pontelli, E., Rossi, G.: ACI1 constraints. In: De Schreye, D. (ed.) ICLP 1999, 16th International Conference on Logic Programming, pp. 573–587. The MIT Press, Cambridge (1999)
Dovier, A., Policriti, A., Rossi, G.: A uniform axiomatic view of lists, multisets and the relevant unification algorithms. Fundamenta Informaticae 36(2/3), 201–234 (1998)
Grumbach, S., Milo, T.: Towards tractable algebras for bags. Journal of Computer and System Sciences 52(3), 570–588 (1996)
Jaffar, J., Maher, M., Marriott, K., Stuckey, P.: The semantics of constraint logic programs. Journal of Logic Programming 1-3(37), 1–46 (1998)
Kunen, K.: Set Theory. An Introduction to Independence Proofs. In: Studies in Logic. North Holland, Amsterdam (1980)
Omodeo, E.G., Policriti, A.: Solvable set/hyperset contexts: I. some decision procedures for the pure, finite case. Communication on Pure and Applied Mathematics 9-10, 1123–1155 (1995)
Parlamento, F., Policriti, A.: The logically simplest form of the infinity axiom. American Mathematical Society 103, 274–276 (1988)
Shmueli, O., Tsur, S., Zaniolo, C.: Compilation of set terms in the logic data language (LDL). Journal of Logic Programming 12(1-2), 89–119 (1992)
Shoenfield, J.R.: Mathematical Logic. Addison-Wesley, Reading (1967)
Stolzenburg, F.: An algorithm for general set unification and its complexity. Journal of Automated Reasoning 22 (1999)
Vaught, R.L.: On a Theorem of Cobham Concerning Undecidable Theories. In: Nagel, E., Suppes, P., Tarski, A. (eds.) Proceedings of the 1960 International Congress, pp. 14–25. Stanford University Press, Stanford (1962)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dovier, A., Piazza, C., Policriti, A. (2000). Comparing Expressiveness of Set Constructor Symbols. In: Kirchner, H., Ringeissen, C. (eds) Frontiers of Combining Systems. FroCoS 2000. Lecture Notes in Computer Science(), vol 1794. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10720084_18
Download citation
DOI: https://doi.org/10.1007/10720084_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67281-4
Online ISBN: 978-3-540-46421-1
eBook Packages: Springer Book Archive