author = {Dietmar Kerbl},
title = {{An automated induction prover for finite sets implemented in the Theorema system}},
language = {english},
abstract = {In this thesis we introduce an extension of the Theorema set theory prover. We implement a prover in Theorema that is able to automatically prove correctness properties about recursive algorithms dealing with finite sets. This prover contains inference rules for setting up an induction over the cardinality of finite sets and rules dealing with the 'an arbitrary element of a set'-language construct in Theorema. We discuss various inference rules and present five case studies demonstrating the new prover and its interaction with the existing Theorema system, in particular the set theory prover. },
number = {10-24},
year = {2010},
month = {October},
length = {79},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}