Logic-Free Reasoning in Isabelle/Isar

DOI10.1007/978-3-540-85110-3_31MaRDI QIDQ5505517zbMATH OpenOpenAlexFDO

Authors Stefan Berghofer, Makarius Wenzel

Publication date 27 January 2009

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

Full work available at URL https://doi.org/10.1007/978-3-540-85110-3_31

Mathematics Subject Classification ID

Recommendations

• Automating free logic in Isabelle/HOL
• scientific article; zbMATH DE number 1867306
• scientific article; zbMATH DE number 2110621
• scientific article; zbMATH DE number 1696798
• Equational reasoning in Isabelle
• scientific article; zbMATH DE number 1028821
• scientific article; zbMATH DE number 1749197
• scientific article; zbMATH DE number 1614689
• On functional symbol-free logic programs
• scientific article; zbMATH DE number 1863378

Cites work

• A comparison of Mizar and Isar
• scientific article; zbMATH DE number 1531624 (Why is no real title available?)
• Interpretation of Locales in Isabelle: Theories and Proof Contexts
• The foundation of a generic theorem prover
• Untersuchungen über das logische Schliessen. II

Cited in

(6)

• Beautiful formalizations in Isabelle/Naproche
• CryptHOL: game-based proofs in higher-order logic
• Higher-order modal logics: automation and applications
• The Isabelle Framework
• scientific article; zbMATH DE number 1863378 (Why is no real title available?)
• Structured Induction Proofs in Isabelle/Isar

Describes a project that uses

Uses Software

• Isabelle
• Isar
• Isabelle/Isar

This page was built for publication: Logic-Free Reasoning in Isabelle/Isar

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