Evaluation of a new recursion induction principle for automated induction
[Examensarbete på avancerad nivå]
Structural induction is a powerful tool for proving properties of functions with recursive structure, but it is useless when the functions do not preserve the structure of the input. Many of today’s cutting-edge automated theorem provers use structural induction, which makes it impossible for them to prove properties about non-structurally recursive functions. We introduce a new induction principle, where the induction is done over a function application. This principle makes it possible to prove properties about non-structurally recursive functions automatically. We compare structural and application induction and the result indicates that application induction is the more powerful induction method, proving more properties, even though structural induction tends to be faster.
Nyckelord: Computer science, Automatic theorem proving, Application induction, Structural induction, Induction, Master’s thesis
Oracle XML Developers Kit 10.2.0.2.0 - Production
XML-25011: Error processing XSLT stylesheet: ../index.xsl
file:////usr/local/tomcat/webapps/chex/local/xsl/output/html/normal/body.xsl<Line 340, Column 84>: XML-22021: (Error) Error parsing external document: 'Förbindelse vägras'.