Automatic proof and disproof in Isabelle/HOL
From MaRDI portal
Recommendations
Cites work
- A Brief Overview of HOL4
- Asynchronous proof processing with Isabelle/Scala and Isabelle/jEdit
- Automated Reasoning
- Code generation via higher-order rewrite systems
- Combining superposition, sorts and splitting
- Edinburgh LCF. A mechanized logic of computation
- Extending Sledgehammer with SMT solvers
- Fast LCF-Style Proof Reconstruction for Z3
- Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL
- Higher-order proof construction based on first-order narrowing
- scientific article; zbMATH DE number 1614711 (Why is no real title available?)
- scientific article; zbMATH DE number 1809861 (Why is no real title available?)
- scientific article; zbMATH DE number 5305114 (Why is no real title available?)
- scientific article; zbMATH DE number 1543300 (Why is no real title available?)
- scientific article; zbMATH DE number 234014 (Why is no real title available?)
- Isabelle/HOL. A proof assistant for higher-order logic
- Kodkod: A Relational Model Finder
- Lightweight relevance filtering for machine-generated resolution problems
- Monotonicity inference for higher-order formulas
- Nitpick: a counterexample generator for higher-order logic based on a relational model finder
- Purely functional lazy non-deterministic programming
- Set theory for verification. I: From foundations to functions
- Set theory for verification. II: Induction and recursion
- Sine qua non for large theory reasoning
- Sledgehammer: judgement day
- Smart test data generators via logic programming
- Sort it out with monotonicity. Translating between many-sorted and unsorted first-order logic
- Source-Level Proof Reconstruction for Interactive Theorem Proving
- Translating higher-order clauses to first-order clauses
Cited in
(55)- Isabelle/HOL
- Isabelle/HOL. A proof assistant for higher-order logic
- A verified SAT solver framework with learn, forget, restart, and incrementality
- FoCaLiZe and Dedukti to the rescue for proof interoperability
- Strategy analysis of non-consequence inference with Euler diagrams
- Goal-oriented conjecturing for Isabelle/HOL
- Left omega algebras and regular equations
- Unifying theories of reactive design contracts
- Formalization of Euler-Lagrange equation set based on variational calculus in HOL light
- Integration of formal proof into unified assurance cases with Isabelle/SACM
- Theorem proving as constraint solving with coherent logic
- From LCF to Isabelle/HOL
- Extending Sledgehammer with SMT solvers
- 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
- A proof strategy language and proof script generation for Isabelle/HOL
- From informal to formal proofs in Euclidean geometry
- Isabelle/UTP: a mechanised theory engineering framework
- A verified SAT solver framework with learn, forget, restart, and incrementality
- Automating free logic in Isabelle/HOL
- AUTO2, a saturation-based heuristic prover for higher-order logic
- Bounded model generation for Isabelle/HOL
- Mechanizing the metatheory of Sledgehammer
- Semi-intelligible Isar proofs from machine-generated proofs
- An Isabelle proof method language
- Teaching semantics with a proof assistant: no more LSD trip proofs
- Automated Reasoning in Higher-Order Regular Algebra
- Deriving comparators and show functions in Isabelle/HOL
- Unifying theories of programming in Isabelle
- Towards a UTP semantics for Modelica
- Automated Engineering of Relational and Algebraic Methods in Isabelle/HOL
- Unifying heterogeneous state-spaces with lenses
- Proving correctness of a KRK chess endgame strategy by using Isabelle/HOL and Z3
- Programming and automating mathematics in the Tarski-Kleene hierarchy
- Regular_Algebras
- αCheck: A mechanized metatheory model checker
- scientific article; zbMATH DE number 2090293 (Why is no real title available?)
- Programming and verifying a declarative first-order prover in Isabelle/HOL
- Extending Sledgehammer with SMT solvers
- Interactive theorem proving from the perspective of Isabelle/Isar
- Frontiers of Combining Systems
- Interactive simplifier tracing and debugging in Isabelle
- A vernacular for coherent logic
- Nitpick: a counterexample generator for higher-order logic based on a relational model finder
- Towards substructural property-based testing
- Hammering Floating-Point Arithmetic
- Linear resources in Isabelle/HOL
- Sledgehammering without ATPs (short paper)
- A computer-assisted proof of correctness of a marching cubes algorithm
- Optics
- Shallow Expressions
- Isabelle/UTP: Mechanised Theory Engineering for Unifying Theories of Programming
- Z Mathematical Toolkit in Isabelle/HOL
Describes a project that uses
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)
