Cited in
(66)- A calculus for and termination of rippling
- Proof planning for strategy development
- Automating the synthesis of decision procedures in a constructive metatheory
- scientific article; zbMATH DE number 1614721 (Why is no real title available?)
- Plans and planning in mathematical proofs
- Middle-out reasoning for synthesis and induction
- Analogy in inductive theorem proving
- Using tactics to reformulate formulae for resolution theorem proving
- Computer supported mathematics with \(\Omega\)MEGA
- Multilanguage hierarchical logics, or: How we can do without modal logics
- Extensions to a generalization critic for inductive proof
- An approach to automatic deductive synthesis of functional programs
- TacticToe: learning to prove with tactics
- Internal analogy in theorem proving
- Productive use of failure in inductive proof
- scientific article; zbMATH DE number 1696825 (Why is no real title available?)
- Making a productive use of failure to generate witnesses for coinduction from divergent proof attempts
- TAME: Using PVS strategies for special-purpose theorem proving
- Termination orderings for rippling
- IsaPlanner
- scientific article; zbMATH DE number 1341612 (Why is no real title available?)
- ALISA
- SCR
- An integrated approach to high integrity software verification
- SPIKE
- Amphion
- Tactician
- Supporting the formal verification of mathematical texts
- OMEGA
- InKa
- Lambda-Clam
- MKRP
- Oyster
- XBarnacle
- Prodigy
- Bliksem
- Doris
- KOMET
- MATHsAiD
- Medmaker
- P.rex
- PROTEIN
- GETFOL
- QuodLibet
- CoCLAM
- RRL
- TAME
- Mollusc
- Mechanizing Mathematical Reasoning
- \textit{Mollusc}: a general proof-development shell for sequent-based logics
- A recursion planning analysis of inductive completion
- KI 2004: Advances in Artificial Intelligence
- Computer-assisted human-oriented inductive theorem proving by \textit{descente infinie} -- a manifesto
- Termination of constructor systems
- Experiments with proof plans for induction
- Proving theorems by reuse
- Using a generalisation critic to find bisimulations for coinductive proofs
- Analogy in automated deduction: a survey
- Mechanical verification on strategies
- Reasoning About Incompletely Defined Programs
- Mechanizing Mathematical Reasoning
- Rippling: A heuristic for guiding inductive proofs
- Termination of algorithms over non-freely generated data types
- scientific article; zbMATH DE number 4164172 (Why is no real title available?)
- On process equivalence = equation solving in CCS
- Lemma discovery for induction. A survey
This page was built for software: CLAM
