More SPASS with Isabelle
From MaRDI portal
Recommendations
- Nonfree datatypes in Isabelle/HOL. Animating a many-sorted metatheory
- Light-weight containers for Isabelle: efficient, extensible, nestable
- More Church-Rosser proofs (in Isabelle/HOL)
- More Church-Rosser proofs (in Isabelle/HOL)
- Foundations of Software Science and Computation Structures
- More on bisimulations for higher order \(\pi\)-calculus
- Interactive simplifier tracing and debugging in Isabelle
- Beautiful formalizations in Isabelle/Naproche
- Term rewriting and beyond -- theorem proving in Isabelle
- scientific article; zbMATH DE number 1722714
Cited in
(17)- LEO-II and Satallax on the Sledgehammer test bench
- Theorem proving as constraint solving with coherent logic
- Automating free logic in HOL, with an experimental application in category theory
- Extending Sledgehammer with SMT solvers
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Mechanizing the metatheory of Sledgehammer
- Semi-intelligible Isar proofs from machine-generated proofs
- Encoding monomorphic and polymorphic types
- A learning-based fact selector for Isabelle/HOL
- Superposition for bounded domains
- Extending Sledgehammer with SMT solvers
- Sledgehammer: judgement day
- Exploiting instantiations from paramodulation proofs in Isabelle/HOL
- Sledgehammering without ATPs (short paper)
- Gödel's God in Isabelle/HOL
- Faithful Logic Embeddings in HOL — Deep and Shallow (Isabelle/HOL dataset)
- Exploring Simplified Variants of Gödel’s Ontological Argument in Isabelle/HOL
Describes a project that uses
Uses Software
This page was built for publication: More SPASS with Isabelle
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2914754)
