swMATH2047MaRDI QIDQ14592FDOQ14592
Author name not available (Why is that?)
Official website: http://dream.inf.ed.ac.uk/projects/isaplanner/
Cited In (57)
- Roles of Math Search in Mathematics
- Conjecture synthesis for inductive theories
- The use of embeddings to provide a clean separation of term and annotation for higher order rippling
- IsaCoSy
- Title not available (Why is that?)
- Automated Deduction – CADE-20
- Discovering applications of higher order functions through proof planning
- Case-analysis for rippling and inductive proof
- A tactic language for declarative proofs
- Mining state-based models from proof corpora
- Theorem Proving in Higher Order Logics
- A proof-centric approach to mathematical assistants
- Supporting the formal verification of mathematical texts
- Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques
- TacticToe: learning to prove with tactics
- Artificial Intelligence and Symbolic Computation
- Symbolic automatic relations and their applications to SMT and CHC solving
- Integrating Maude into Hets
- IsaWin
- TAS
- HipSpec
- Zeno
- CRC 3
- HERMIT
- SicoTHEO
- HR
- Hipster
- Hat
- Tactician
- Cyclist
- QuickSpec
- CLAM
- InKa
- Lambda-Clam
- Oyster
- TIP
- XBarnacle
- MATHsAiD
- Multi
- QuodLibet
- VerifyThis
- XIsabelle
- Jape
- Automated cyclic entailment proofs in separation logic
- Proof planning with multiple strategies
- Lemma discovery for induction. A survey
- A Framework for Interactive Proof
- SAD as a mathematical assistant -- how should we go from here to there?
- Dynamic rippling, middle-out reasoning and lemma discovery
- A proof strategy language and proof script generation for Isabelle/HOL
- Proof automation for functional correctness in separation logic
- Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC
- On the comparison of proof planning systems: \(\lambda\)\textsc{clam}, \(\Omega\)\textsc{mega} and \textsc{IsaPlanner}
- Enhancing theorem prover interfaces with program slice information
- Hipster: integrating theory exploration in a proof assistant
- Automating Event-B invariant proofs by rippling and proof patching
- Removing algebraic data types from constrained Horn clauses using difference predicates
This page was built for software: IsaPlanner
