Automatic Proof and Disproof in Isabelle/HOL
- 1 January 2011
- book chapter
- conference paper
- Published by Springer Science and Business Media LLC in Lecture Notes in Computer Science
Abstract
No abstract availableKeywords
This publication has 31 references indexed in Scilit:
- Lightweight relevance filtering for machine-generated resolution problemsJournal of Applied Logic, 2009
- Higher-Order Proof Construction Based on First-Order NarrowingElectronic Notes in Theoretical Computer Science, 2008
- A Brief Overview of HOL4Lecture Notes in Computer Science, 2008
- Z3: An Efficient SMT SolverLecture Notes in Computer Science, 2008
- Translating Higher-Order Clauses to First-Order ClausesJournal of Automated Reasoning, 2007
- Source-Level Proof Reconstruction for Interactive Theorem ProvingLecture Notes in Computer Science, 2007
- System Description: E 0.81Lecture Notes in Computer Science, 2004
- Combining Superposition, Sorts and SplittingPublished by Elsevier BV ,2001
- Type classes and overloading in higher-order logicPublished by Springer Science and Business Media LLC ,1997
- Set theory for verification. II: Induction and recursionJournal of Automated Reasoning, 1995