Automatic Proof and Disproof in Isabelle/HOL

From MaRDI portal
Publication:3172879

DOI10.1007/978-3-642-24364-6_2zbMath1348.68214OpenAlexW15103390MaRDI QIDQ3172879

Lukas Bulwahn, Jasmin Christian Blanchette, Tobias Nipkow

Publication date: 7 October 2011

Published in: Frontiers of Combining Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-24364-6_2



Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).


Related Items (27)

Teaching Semantics with a Proof Assistant: No More LSD Trip ProofsFrom informal to formal proofs in Euclidean geometryUnifying Heterogeneous State-Spaces with LensesAutomated Reasoning in Higher-Order Regular AlgebraA verified SAT solver framework with learn, forget, restart, and incrementalityUnifying Theories of Programming in IsabelleLeft omega algebras and regular equationsFoCaLiZe and Dedukti to the rescue for proof interoperabilityαCheck: A mechanized metatheory model checkerProgramming and automating mathematics in the Tarski-Kleene hierarchyTowards substructural property-based testingTowards a UTP Semantics for ModelicaStrategy analysis of non-consequence inference with Euler diagramsUnifying theories of reactive design contractsFrom LCF to Isabelle/HOLFormalization of Euler-Lagrange equation set based on variational calculus in HOL lightIsabelle/UTP: A Mechanised Theory Engineering FrameworkA Verified SAT Solver Framework with Learn, Forget, Restart, and IncrementalityIsabelle/HOLIntegration of formal proof into unified assurance cases with Isabelle/SACMInteractive Simplifier Tracing and Debugging in IsabelleA Vernacular for Coherent LogicTheorem proving as constraint solving with coherent logicLearning-assisted automated reasoning with \(\mathsf{Flyspeck}\)Premise selection for mathematics by corpus analysis and kernel methodsOn the fine-structure of regular algebraAutomated generation of machine verifiable and readable proofs: a case study of Tarski's geometry


Uses Software


Cites Work


This page was built for publication: Automatic Proof and Disproof in Isabelle/HOL