The Isabelle Framework

DOI10.1007/978-3-540-71067-7_7zbMath1165.68478OpenAlexW1571434026MaRDI QIDQ3543647

Tobias Nipkow, Makarius Wenzel, Lawrence Charles Paulson

Publication date: 4 December 2008

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-71067-7_7

Mathematics Subject Classification ID

Related Items (29)

Presentation and manipulation of Mizar properties in an Isabelle object logic ⋮ Classification of alignments between concepts of formal mathematical systems ⋮ Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation ⋮ Formalization of Forcing in Isabelle/ZF ⋮ The role of entropy in guiding a connection prover ⋮ Aligning concepts across proof assistant libraries ⋮ Big Math and the one-brain barrier: the tetrapod model of mathematical knowledge ⋮ Tools for the Investigation of Substructural and Paraconsistent Logics ⋮ Proof-Producing Reflection for HOL ⋮ Pattern Matches in HOL: ⋮ Taming Paraconsistent (and Other) Logics ⋮ Automating formalization by statistical and semantic parsing of mathematics ⋮ Combining higher-order logic with set theory formalizations ⋮ Verified verifying: SMT-LIB for strings in Isabelle ⋮ Psi-calculi in Isabelle ⋮ Learning-assisted theorem proving with millions of lemmas ⋮ Higher-Order Tarski Grothendieck as a Foundation for Formal Proof. ⋮ Superposition for Bounded Domains ⋮ TacticToe: learning to prove with tactics ⋮ Machine learning guidance for connection tableaux ⋮ N. G. de Bruijn's contribution to the formalization of mathematics ⋮ Isabelle ⋮ Validating QBF Validity in HOL4 ⋮ Heterogeneous Proofs: Spider Diagrams Meet Higher-Order Provers ⋮ Semantics of Mizar as an Isabelle object logic ⋮ Proof assistants: history, ideas and future ⋮ Matching Concepts across HOL Libraries ⋮ First steps towards a formalization of forcing ⋮ Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL

Uses Software

• Isabelle/HOL
• Isabelle/Isar
• Metis_
• Isar
• Mizar
• Proof General
• Isabelle/ZF
• HOL
• Flyspeck
• Nominal Isabelle
• Locales
• Tame Graphs

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Nominal techniques in Isabelle/HOL
• Set theory for verification. I: From foundations to functions
• Isabelle. A generic theorem prover
• Organizing numerical theories using axiomatic type classes
• Edinburgh LCF. A mechanized logic of computation
• A comparison of Mizar and Isar
• Set theory for verification. II: Induction and recursion
• Flyspeck II: The basic linear programs
• Mechanizing the metatheory of LF
• Types, bytes, and separation logic
• Source-Level Proof Reconstruction for Interactive Theorem Proving
• Building Formal Method Tools in the Isabelle/Isar Framework
• A Compiled Implementation of Normalization by Evaluation
• Imperative Functional Programming with Isabelle/HOL
• Constructive Type Classes in Isabelle
• Flyspeck I: Tame Graphs
• Partial Recursive Functions in Higher-Order Logic
• Local Theory Specifications in Isabelle/Isar
• HOLCF = HOL + LCF
• Natural deduction as higher-order resolution
• The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle⁄zf
• A formally verified proof of the prime number theorem
• Context Aware Calculation and Deduction
• Formal Pervasive Verification of a Paging Mechanism
• Logic-Free Reasoning in Isabelle/Isar
• Types for Proofs and Programs
• Structured Induction Proofs in Isabelle/Isar
• Interpretation of Locales in Isabelle: Theories and Proof Contexts

This page was built for publication: The Isabelle Framework