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