More SPASS with Isabelle

DOI10.1007/978-3-642-32347-8_24zbMath1360.68742OpenAlexW1481699975MaRDI QIDQ2914754

Daniel Wand, Christoph Weidenbach, Jasmin Christian Blanchette, Andrei Popescu

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

Related Items

Semi-intelligible Isar proofs from machine-generated proofs, A learning-based fact selector for Isabelle/HOL, Encoding Monomorphic and Polymorphic Types, Superposition for Bounded Domains, Automating free logic in HOL, with an experimental application in category theory, Theorem proving as constraint solving with coherent logic, Extending Sledgehammer with SMT solvers, Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)

Uses Software

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