Oyster

swMATH19629MaRDI QIDQ31454FDOQ31454

Author name not available (Why is that?)

Cited In (32)

• 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
• Title not available (Why is that?)
• 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