IsaPlanner - MaRDI portal

swMATH2047MaRDI QIDQ14592FDOQ14592

Author name not available (Why is that?)

Cited In (31)

Mining State-Based Models from Proof Corpora
Case-Analysis for Rippling and Inductive Proof
Roles of Math Search in Mathematics
A Tactic Language for Declarative Proofs
Dynamic Rippling, Middle-Out Reasoning and Lemma Discovery
Conjecture synthesis for inductive theories
The use of embeddings to provide a clean separation of term and annotation for higher order rippling
Title not available (Why is that?)
Automated Deduction – CADE-20
Discovering applications of higher order functions through proof planning
Automated Cyclic Entailment Proofs in Separation Logic
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
Hipster: Integrating Theory Exploration in a Proof Assistant
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?
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
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