More SPASS with Isabelle

DOI10.1007/978-3-642-32347-8_24MaRDI QIDQ2914754zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

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
• A learning-based fact selector for Isabelle/HOL
• Mechanizing the metatheory of Sledgehammer
• Encoding monomorphic and polymorphic types
• 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

Describes a project that uses

Uses Software

• OMEGA
• seL4
• Ivy
• Gandalf
• VCC
• Sledgehammer
• z3
• Mizar
• TPTP
• SPASS
• Isabelle/HOL
• Coq

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)