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 Proofs ⋮ From informal to formal proofs in Euclidean geometry ⋮ Unifying Heterogeneous State-Spaces with Lenses ⋮ Automated Reasoning in Higher-Order Regular Algebra ⋮ A verified SAT solver framework with learn, forget, restart, and incrementality ⋮ Unifying Theories of Programming in Isabelle ⋮ Left omega algebras and regular equations ⋮ FoCaLiZe and Dedukti to the rescue for proof interoperability ⋮ αCheck: A mechanized metatheory model checker ⋮ Programming and automating mathematics in the Tarski-Kleene hierarchy ⋮ Towards substructural property-based testing ⋮ Towards a UTP Semantics for Modelica ⋮ Strategy analysis of non-consequence inference with Euler diagrams ⋮ Unifying theories of reactive design contracts ⋮ From LCF to Isabelle/HOL ⋮ Formalization of Euler-Lagrange equation set based on variational calculus in HOL light ⋮ Isabelle/UTP: A Mechanised Theory Engineering Framework ⋮ A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality ⋮ Isabelle/HOL ⋮ Integration of formal proof into unified assurance cases with Isabelle/SACM ⋮ Interactive Simplifier Tracing and Debugging in Isabelle ⋮ A Vernacular for Coherent Logic ⋮ Theorem proving as constraint solving with coherent logic ⋮ Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\) ⋮ Premise selection for mathematics by corpus analysis and kernel methods ⋮ On the fine-structure of regular algebra ⋮ Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Lightweight relevance filtering for machine-generated resolution problems
- Set theory for verification. I: From foundations to functions
- Isabelle/HOL. A proof assistant for higher-order logic
- Edinburgh LCF. A mechanized logic of computation
- Set theory for verification. II: Induction and recursion
- Translating higher-order clauses to first-order clauses
- Smart test data generators via logic programming
- Purely functional lazy non-deterministic programming
- Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL
- Source-Level Proof Reconstruction for Interactive Theorem Proving
- A Brief Overview of HOL4
- Code Generation via Higher-Order Rewrite Systems
- Asynchronous Proof Processing with Isabelle/Scala and Isabelle/jEdit
- Extending Sledgehammer with SMT Solvers
- Sort It Out with Monotonicity
- Sine Qua Non for Large Theory Reasoning
- Automated Reasoning
- Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder
- Fast LCF-Style Proof Reconstruction for Z3
- Monotonicity Inference for Higher-Order Formulas
- Sledgehammer: Judgement Day
- Kodkod: A Relational Model Finder
This page was built for publication: Automatic Proof and Disproof in Isabelle/HOL