The Isabelle Framework
From MaRDI portal
Publication:3543647
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
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
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
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