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 Lx 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. © Springer-Verlag Berlin Heidelberg 2001.
Author supplied keywords
Cite
CITATION STYLE
Formisano, A., Omodeo, E. G., & Temperini, M. (2001). Instructing equational set-reasoning with otter. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2083 LNAI, pp. 152–167). Springer Verlag. https://doi.org/10.1007/3-540-45744-5_12
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
