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 logicClassification of alignments between concepts of formal mathematical systemsSelf-formalisation of higher-order logic. Semantics, soundness, and a verified implementationFormalization of Forcing in Isabelle/ZFThe role of entropy in guiding a connection proverAligning concepts across proof assistant librariesBig Math and the one-brain barrier: the tetrapod model of mathematical knowledgeTools for the Investigation of Substructural and Paraconsistent LogicsProof-Producing Reflection for HOLPattern Matches in HOL:Taming Paraconsistent (and Other) LogicsAutomating formalization by statistical and semantic parsing of mathematicsCombining higher-order logic with set theory formalizationsVerified verifying: SMT-LIB for strings in IsabellePsi-calculi in IsabelleLearning-assisted theorem proving with millions of lemmasHigher-Order Tarski Grothendieck as a Foundation for Formal Proof.Superposition for Bounded DomainsTacticToe: learning to prove with tacticsMachine learning guidance for connection tableauxN. G. de Bruijn's contribution to the formalization of mathematicsIsabelleValidating QBF Validity in HOL4Heterogeneous Proofs: Spider Diagrams Meet Higher-Order ProversSemantics of Mizar as an Isabelle object logicProof assistants: history, ideas and futureMatching Concepts across HOL LibrariesFirst steps towards a formalization of forcingTowards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL


Uses Software


Cites Work


This page was built for publication: The Isabelle Framework