IsaPlanner: A Prototype Proof Planner in Isabelle
- 1 January 2003
- 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 10 references indexed in Scilit:
- Ordinal Arithmetic: A Case Study for Rippling in a Higher Order DomainLecture Notes in Computer Science, 2001
- Logic Program Synthesis in a Higher-Order SettingLecture Notes in Computer Science, 2000
- Isar — A Generic Interpretative Approach to Readable Formal Proof DocumentsLecture Notes in Computer Science, 1999
- System description: Proof planning in higher-order logic with λClamLecture Notes in Computer Science, 1998
- An interface between CLAM and HOLPublished by Springer Science and Business Media LLC ,1998
- Derivation and use of induction schemes in higher-order logicPublished by Springer Science and Business Media LLC ,1997
- Productive use of failure in inductive proofJournal of Automated Reasoning, 1996
- Experiments in automating hardware verification using inductive proof planningPublished by Springer Science and Business Media LLC ,1996
- IsabellePublished by Springer Science and Business Media LLC ,1994
- Experiments with proof plans for inductionJournal of Automated Reasoning, 1991