Structured Induction Proofs in Isabelle/Isar

DOI10.1007/11812289_3MaRDI QIDQ5756773zbMATH OpenOpenAlexFDO

Authors Makarius Wenzel

Publication date 5 September 2007

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/11812289_3

Mathematics Subject Classification ID

Computing methodologies for text processing; mathematical typography (68U15)

Recommendations

• Logic-Free Reasoning in Isabelle/Isar
• The Isabelle Framework
• scientific article; zbMATH DE number 1863378
• Interactive theorem proving from the perspective of Isabelle/Isar
• Building Formal Method Tools in the Isabelle/Isar Framework

Cited in

(8)

• The equational part of proofs by structural induction
• Eisbach: a proof method language for Isabelle
• Building Formal Method Tools in the Isabelle/Isar Framework
• The Isabelle Framework
• scientific article; zbMATH DE number 1863378 (Why is no real title available?)
• Types for Proofs and Programs
• Invertibility in Sequent Calculi
• Nominal techniques in Isabelle/HOL

Describes a project that uses

Uses Software

• Isabelle/Isar
• Isabelle
• Isar

This page was built for publication: Structured Induction Proofs in Isabelle/Isar

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5756773)