Formisano, Andrea; Omodeo, Eugenio G.; Temperini, Marco Instructing equational set-reasoning with Otter. (English) Zbl 0988.68164 Goré, Rajeev (ed.) et al., Automated reasoning. 1st international joint conference, IJCAR 2001, Siena, Italy, June 18-22, 2001. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2083, 152-167 (2001). Summary: 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 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.For the entire collection see [Zbl 0968.00052]. Cited in 4 Documents MSC: 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010) 03B35 Mechanization of proofs and logical operations 03E99 Set theory Keywords:et reasoning; map algebra; first-order theorem proving Software:OTTER PDFBibTeX XMLCite \textit{A. Formisano} et al., Lect. Notes Comput. Sci. 2083, 152--167 (2001; Zbl 0988.68164) Full Text: Link