IsaPlanner
From MaRDI portal
Software:14592
No author found.
Related Items (31)
Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques ⋮ Symbolic automatic relations and their applications to SMT and CHC solving ⋮ Proof planning with multiple strategies ⋮ A proof-centric approach to mathematical assistants ⋮ SAD as a mathematical assistant -- how should we go from here to there? ⋮ Supporting the formal verification of mathematical texts ⋮ A proof strategy language and proof script generation for Isabelle/HOL ⋮ Unnamed Item ⋮ Conjecture synthesis for inductive theories ⋮ Automated Deduction – CADE-20 ⋮ Automating Event-B invariant proofs by rippling and proof patching ⋮ Unnamed Item ⋮ The use of embeddings to provide a clean separation of term and annotation for higher order rippling ⋮ Proof automation for functional correctness in separation logic ⋮ A Framework for Interactive Proof ⋮ A Tactic Language for Declarative Proofs ⋮ Case-Analysis for Rippling and Inductive Proof ⋮ Roles of Math Search in Mathematics ⋮ Dynamic Rippling, Middle-Out Reasoning and Lemma Discovery ⋮ TacticToe: learning to prove with tactics ⋮ Automated Cyclic Entailment Proofs in Separation Logic ⋮ Integrating Maude into Hets ⋮ Lemma discovery for induction. A survey ⋮ Artificial Intelligence and Symbolic Computation ⋮ Theorem Proving in Higher Order Logics ⋮ Hipster: Integrating Theory Exploration in a Proof Assistant ⋮ Mining State-Based Models from Proof Corpora ⋮ Discovering applications of higher order functions through proof planning ⋮ Removing algebraic data types from constrained Horn clauses using difference predicates ⋮ Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC ⋮ Enhancing Theorem Prover Interfaces with Program Slice Information
This page was built for software: IsaPlanner
