IsaPlanner
IsaPlanner is a generic framework for proof planning in the interactive theorem prover Isabelle. It facilitates the encoding of reasoning techniques, which can be used to conjecture and prove theorems automatically. The system provides an interactive tracing tool that allows you to interact the proof planning attempt. (see the screenshot of IsaPlanner being used with Isabelle and Proof General) It is based on the Isabelle theorem prover and the Isar language. The main proof technique written in IsaPlanner is an inductive theorem prover based on Rippling. This is applicable within Isabelle”s Higher Order Logic, and can easily be adapted to Isabelle”s other logics.
Keywords for this software
References in zbMATH (referenced in 29 articles , 1 standard article )
Showing results 1 to 20 of 29.
Sorted by year (- Drămnesc, Isabela; Jebelean, Tudor; Stratulat, Sorin: Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques (2019)
- Johansson, Moa: Lemma discovery for induction. A survey (2019)
- Lin, Yuhui; Bundy, Alan; Grov, Gudmund; Maclean, Ewen: Automating Event-B invariant proofs by rippling and proof patching (2019)
- Nagashima, Yutaka; Kumar, Ramana: A proof strategy language and proof script generation for Isabelle/HOL (2017)
- Lin, Yuhui; Grov, Gudmund; Arthan, Rob: Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC (2016)
- Maclean, Ewen; Ireland, Andrew; Grov, Gudmund: Proof automation for functional correctness in separation logic (2016)
- Gransden, Thomas; Walkinshaw, Neil; Raman, Rajeev: Mining state-based models from proof corpora (2014)
- Johansson, Moa; Rosén, Dan; Smallbone, Nicholas; Claessen, Koen: Hipster: integrating theory exploration in a proof assistant (2014)
- Brotherston, James; Distefano, Dino; Petersen, Rasmus Lerchedahl: Automated cyclic entailment proofs in separation logic (2011)
- Codescu, Mihai; Mossakowski, Till; Riesco, Adrián; Maeder, Christian: Integrating Maude into Hets (2011)
- Dennis, Louise Abigail; Green, Ian; Smaill, Alan: The use of embeddings to provide a clean separation of term and annotation for higher order rippling (2011)
- Johansson, Moa; Dixon, Lucas; Bundy, Alan: Conjecture synthesis for inductive theories (2011)
- Autexier, Serge; Dietrich, Dominik: A tactic language for declarative proofs (2010)
- Johansson, Moa; Dixon, Lucas; Bundy, Alan: Case-analysis for rippling and inductive proof (2010)
- Johansson, Moa; Dixon, Lucas; Bundy, Alan: Dynamic rippling, middle-out reasoning and lemma discovery (2010)
- Melis, Erica; Meier, Andreas; Siekmann, Jörg: Proof planning with multiple strategies (2008)
- Aspinall, David; Lüth, Christoph; Winterstein, Daniel: A framework for interactive proof (2007)
- Dennis, Louise A.: Enhancing theorem prover interfaces with program slice information (2007)
- Dennis, Louise A.; Jamnik, Mateja; Pollet, Martin: On the comparison of proof planning systems: (\lambda)\textscclam, (\Omega)\textscmegaand \textscIsaPlanner (2006)
- Dixon, Lucas; Fleuriot, Jacques: A proof-centric approach to mathematical assistants (2006)
Further publications can be found at: http://dream.inf.ed.ac.uk/publications/