Structured Induction Proofs in Isabelle/Isar | Zendy

Makarius Wenzel | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Structured Induction Proofs in Isabelle/Isar

Author(s) -

Makarius Wenzel

Publication year - 2006

Publication title -

lecture notes in computer science

Language(s) - English

Resource type - Book series

SCImago Journal Rank - 0.249

H-Index - 400

eISSN - 1611-3349

pISSN - 0302-9743

ISBN - 3-540-37104-4

DOI - 10.1007/11812289_3

Subject(s) - mathematical proof , inverse synthetic aperture radar , computer science , proof assistant , programming language , proof of concept , natural language processing , artificial intelligence , radar , mathematics , radar imaging , telecommunications , geometry , operating system

Isabelle/Isar is a generic framework for human-readable formal proof documents, based on higher-order natural deduction. The Isar proof language provides general principles that may be instantiated to particular object-logics and applications. We discuss specific Isar language elements that support complex induction patterns of practical importance. Despite the additional bookkeeping required for induction with local facts and parameters, definitions, simultaneous goals and multiple rules, the resulting Isar proof texts turn out well-structured and readable. Our techniques can be applied to non-standard variants of induction as well, such as co-induction and nominal induction. This demonstrates that Isar provides a viable platform for building domain-specific tools that support fully-formal mathematical proof composition.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research