Abstract
An experimentation activity in automated set-reasoning is reported. The methodology adopted is based on an equational re- engineering of ZF set theory within the ground formalism \(\mathcal{L}^ \times\)developed by Tarski and Givant. On top of a kernel axiomatization of map algebra we develop a layered formalization of basic set-theoretical concepts. A first-order theorem prover is exploited to obtain automated certification and validation of this layered architecture.
This research was partially funded by the Italian IASI-CNR (coordinated project log(SETA)) and by MURST (PGR-2000—Automazione del ragionamento in teorie insiemistiche).
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
F. Aureli, A. Formisano, E. G. Omodeo, and M. Temperini. Map calculus: Initial application scenarios and experiments based on Otter. Rep. 466, IASI-CNR, 1998.
J. L. Bell and A. B. Slomson. Models and unltraproducts: An introduction. North-Holland, Studies in Logic and the Foundations of Mathematics, 3rd printing, 1974.
R. Boyer, E. Lusk, W. McCune, R. Overbeek, M. Stickel, and L. Wos. Set theory in first-order logic: Clauses for Gödel’s axioms. JAR, 2(3), 1986.
A. Chiacchiaretta, A. Formisano, and E. G. Omodeo. Benchmark #1 for equational set theory. Giornata “Analisi Sperimentale di Algoritmi per l’Intelligenza Artificiale” (Rome, 16, December 1999).
A. Chiacchiaretta, A. Formisano, and E. G. Omodeo. Map reasoning through existential multigraphs. Rep. 05/00, Dipartimento di Matematica Pura ed Applicata, Università di L’Aquila, April 2000.
A. Formisano and E. G. Omodeo. An equational re-engineering of set theories. In Caferra and Salzer eds., Automated Deduction in Classical and Non-Classical Logics, LNCS 1761 (LNAI), pages 175–190. Springer, 2000.
M. K. Kwatinetz. Problems of expressibility in finite languages. PhD thesis, University of California, Berkeley, 1981.
W. W. McCune. OTTER 3.0 Reference Manual and Guide. Argonne National Laboratory/IL, USA, 1994.
P. A. J. Noёl. Experimenting with Isabelle in ZF set theory. JAR, 10(1):15–58, 1993.
L. C. Paulson. Set Theory for verification. II: Induction and recursion. JAR, 15(2):167–215, 1995.
A. Quaife. Automated deduction in von Neumann-Bernays-Gödel Set Theory. JAR, 8(1):91–147, 1992.
A. Quaife. Automated development of fundamental mathematical theories. Kluwer Academic Publishers, 1992.
G. Schmidt and T. Ströhlein. Relation algebras: Concept of points and represent ability. Discrete Mathematics, 54:83–92, 1985.
E. Schröder. Vorlesungen über die Algebra der Logik (exakte Logik). B. Teubner, Leipzig, 1891–1895. [Reprinted by Chelsea Publishing Co., New York, 1966.]
A. Tarski and S. Givant. A formalization of set theory without variables. Vol. 41 of Colloquium Publications. AMS, 1987.
L. Wos. Automated reasoning. 33 basic research problems. Prentice Hall, 1988.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Formisano, A., Omodeo, E.G., Temperini, M. (2001). Instructing Equational Set-Reasoning with Otter. In: Goré, R., Leitsch, A., Nipkow, T. (eds) Automated Reasoning. IJCAR 2001. Lecture Notes in Computer Science, vol 2083. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45744-5_12
Download citation
DOI: https://doi.org/10.1007/3-540-45744-5_12
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42254-9
Online ISBN: 978-3-540-45744-2
eBook Packages: Springer Book Archive