The following pages link to IsaPlanner (Q14592):
Displaying 31 items.
- Conjecture synthesis for inductive theories (Q438543) (← links)
- The use of embeddings to provide a clean separation of term and annotation for higher order rippling (Q540694) (← links)
- Automating Event-B invariant proofs by rippling and proof patching (Q667526) (← links)
- A proof-centric approach to mathematical assistants (Q865648) (← links)
- SAD as a mathematical assistant -- how should we go from here to there? (Q865654) (← links)
- Supporting the formal verification of mathematical texts (Q865656) (← links)
- Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques (Q1640636) (← links)
- TacticToe: learning to prove with tactics (Q2031416) (← links)
- Removing algebraic data types from constrained Horn clauses using difference predicates (Q2096439) (← links)
- Symbolic automatic relations and their applications to SMT and CHC solving (Q2145347) (← links)
- Lemma discovery for induction. A survey (Q2287904) (← links)
- Proof planning with multiple strategies (Q2389631) (← links)
- A proof strategy language and proof script generation for Isabelle/HOL (Q2405272) (← links)
- Discovering applications of higher order functions through proof planning (Q2576573) (← links)
- (Q2767093) (← links)
- On the comparison of proof planning systems: \(\lambda\)\textsc{clam}, \(\Omega\)\textsc{mega} and \textsc{IsaPlanner} (Q2852043) (← links)
- Enhancing theorem prover interfaces with program slice information (Q2867933) (← links)
- Dynamic Rippling, Middle-Out Reasoning and Lemma Discovery (Q3058453) (← links)
- Integrating Maude into Hets (Q3067467) (← links)
- Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC (Q5195279) (← links)
- Automated Cyclic Entailment Proofs in Separation Logic (Q5200020) (← links)
- Automated Deduction – CADE-20 (Q5394617) (← links)
- A Framework for Interactive Proof (Q5428268) (← links)
- Theorem Proving in Higher Order Logics (Q5464664) (← links)
- Artificial Intelligence and Symbolic Computation (Q5464716) (← links)
- Hipster: Integrating Theory Exploration in a Proof Assistant (Q5495917) (← links)
- Mining State-Based Models from Proof Corpora (Q5495930) (← links)
- Proof automation for functional correctness in separation logic (Q5739977) (← links)
- A Tactic Language for Declarative Proofs (Q5747644) (← links)
- Case-Analysis for Rippling and Inductive Proof (Q5747656) (← links)
- Roles of Math Search in Mathematics (Q5756768) (← links)
