More SPASS with Isabelle
From MaRDI portal
Publication:2914754
DOI10.1007/978-3-642-32347-8_24zbMATH Open1360.68742OpenAlexW1481699975MaRDI QIDQ2914754FDOQ2914754
Authors: Jasmin Christian Blanchette, Andrei Popescu, Daniel Wand, Christoph Weidenbach 
Publication date: 20 September 2012
Published in: Interactive Theorem Proving (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-32347-8_24
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 (12)
- Extending Sledgehammer with SMT solvers
- Semi-intelligible Isar proofs from machine-generated proofs
- Superposition for bounded domains
- Encoding monomorphic and polymorphic types
- Mechanizing the metatheory of Sledgehammer
- A learning-based fact selector for Isabelle/HOL
- Sledgehammer: judgement day
- Extending Sledgehammer with SMT solvers
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Theorem proving as constraint solving with coherent logic
- Automating free logic in HOL, with an experimental application in category theory
- LEO-II and Satallax on the Sledgehammer test bench
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)
