swMATH19629MaRDI QIDQ31454FDOQ31454
Author name not available (Why is that?)
Official website: https://pdfs.semanticscholar.org/6cb8/ac778dfdd799dda3e8a0a9169431eef28062.pdf
Cited In (51)
- Rule-based induction
- An approach to automatic deductive synthesis of functional programs
- Proofs-as-programs as a framework for the design of an analogy-based ML editor
- On process equivalence = equation solving in CCS
- Rippling: A heuristic for guiding inductive proofs
- Analogy in automated deduction: a survey
- KI 2004: Advances in Artificial Intelligence
- Supporting the formal verification of mathematical texts
- Mechanizing Mathematical Reasoning
- Extensions to a generalization critic for inductive proof
- Planning proofs of equations in CCS
- Termination of algorithms over non-freely generated data types
- Productive use of failure in inductive proof
- Experiments with proof plans for induction
- Computer supported mathematics with \(\Omega\)MEGA
- TacticToe: learning to prove with tactics
- A calculus for and termination of rippling
- \textit{Mollusc}: a general proof-development shell for sequent-based logics
- Plans and planning in mathematical proofs
- Termination of constructor systems
- IsaPlanner
- ALISA
- SPIKE
- Amphion
- fc2tools
- Tactician
- Title not available (Why is that?)
- CLAM
- CyNTHIA
- InKa
- Lambda-Clam
- MKRP
- XBarnacle
- Prodigy
- Doris
- P.rex
- QuodLibet
- CoCLAM
- RRL
- Mollusc
- Mechanical verification on strategies
- Computer-assisted human-oriented inductive theorem proving by \textit{descente infinie} -- a manifesto
- Lemma discovery for induction. A survey
- Concept Formation via Proof Planning Failure
- Termination orderings for rippling
- Making a productive use of failure to generate witnesses for coinduction from divergent proof attempts
- Proving theorems by reuse
- Using a generalisation critic to find bisimulations for coinductive proofs
- Title not available (Why is that?)
- Using tactics to reformulate formulae for resolution theorem proving
- Middle-out reasoning for synthesis and induction
This page was built for software: Oyster
