×

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].

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B35 Mechanization of proofs and logical operations
03E99 Set theory

Software:

OTTER
PDFBibTeX XMLCite
Full Text: Link