Automatic proof and disproof in Isabelle/HOL
From MaRDI portal
Publication:3172879
DOI10.1007/978-3-642-24364-6_2zbMATH Open1348.68214OpenAlexW15103390MaRDI QIDQ3172879FDOQ3172879
Authors: Jasmin Christian Blanchette, Lukas Bulwahn, 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
Recommendations
Cites Work
- Title not available (Why is that?)
- A Brief Overview of HOL4
- Extending Sledgehammer with SMT Solvers
- Title not available (Why is that?)
- Nitpick: a counterexample generator for higher-order logic based on a relational model finder
- Kodkod: A Relational Model Finder
- Edinburgh LCF. A mechanized logic of computation
- Title not available (Why is that?)
- Automated Reasoning
- Isabelle/HOL. A proof assistant for higher-order logic
- Lightweight relevance filtering for machine-generated resolution problems
- Set theory for verification. I: From foundations to functions
- Translating higher-order clauses to first-order clauses
- Combining superposition, sorts and splitting
- Source-Level Proof Reconstruction for Interactive Theorem Proving
- Title not available (Why is that?)
- Sort It Out with Monotonicity
- Sine Qua Non for Large Theory Reasoning
- Fast LCF-Style Proof Reconstruction for Z3
- Sledgehammer: judgement day
- Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL
- Monotonicity inference for higher-order formulas
- Code generation via higher-order rewrite systems
- Set theory for verification. II: Induction and recursion
- Title not available (Why is that?)
- Purely functional lazy non-deterministic programming
- Asynchronous Proof Processing with Isabelle/Scala and Isabelle/jEdit
- Higher-order proof construction based on first-order narrowing
- Smart test data generators via logic programming
Cited In (33)
- Linear resources in Isabelle/HOL
- On the fine-structure of regular algebra
- Isabelle/UTP: A Mechanised Theory Engineering Framework
- Unifying theories of reactive design contracts
- Towards a UTP Semantics for Modelica
- Title not available (Why is that?)
- Unifying Heterogeneous State-Spaces with Lenses
- Isabelle/HOL. A proof assistant for higher-order logic
- From informal to formal proofs in Euclidean geometry
- Programming and automating mathematics in the Tarski-Kleene hierarchy
- Formalization of Euler-Lagrange equation set based on variational calculus in HOL light
- A verified SAT solver framework with learn, forget, restart, and incrementality
- Isabelle/HOL
- Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry
- Left omega algebras and regular equations
- A Vernacular for Coherent Logic
- αCheck: A mechanized metatheory model checker
- Interactive Simplifier Tracing and Debugging in Isabelle
- From LCF to Isabelle/HOL
- Automated Engineering of Relational and Algebraic Methods in Isabelle/HOL
- Integration of formal proof into unified assurance cases with Isabelle/SACM
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Premise selection for mathematics by corpus analysis and kernel methods
- Frontiers of Combining Systems
- Towards substructural property-based testing
- A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality
- Teaching Semantics with a Proof Assistant: No More LSD Trip Proofs
- Theorem proving as constraint solving with coherent logic
- FoCaLiZe and Dedukti to the rescue for proof interoperability
- Nitpick: a counterexample generator for higher-order logic based on a relational model finder
- Automated Reasoning in Higher-Order Regular Algebra
- Unifying Theories of Programming in Isabelle
- Strategy analysis of non-consequence inference with Euler diagrams
Uses Software
This page was built for publication: Automatic proof and disproof in Isabelle/HOL
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3172879)
