Oyster
From MaRDI portal
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
- Planning proofs of equations in CCS
- Extensions to a generalization critic for inductive proof
- Productive use of failure in inductive proof
- Termination of algorithms over non-freely generated data types
- Experiments with proof plans for induction
- Computer supported mathematics with 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
- IsaPlanner
- ALISA
- SPIKE
- Amphion
- fc2tools
- Tactician
- CLAM
- CyNTHIA
- InKa
- Lambda-Clam
- MKRP
- XBarnacle
- Prodigy
- Doris
- P.rex
- QuodLibet
- CoCLAM
- RRL
- Mollusc
- Plans and planning in mathematical proofs
- Termination of constructor systems
- scientific article; zbMATH DE number 622669 (Why is no real title available?)
- 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 tactics to reformulate formulae for resolution theorem proving
- scientific article; zbMATH DE number 4164172 (Why is no real title available?)
- Using a generalisation critic to find bisimulations for coinductive proofs
- Middle-out reasoning for synthesis and induction
This page was built for software: Oyster
