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
• PLANS AND PLANNING IN MATHEMATICAL PROOFS
• Mollusc a general proof-development shell for sequent-based logics
• 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
• KI 2004: Advances in Artificial Intelligence
• Computer-assisted human-oriented inductive theorem proving by descente infinie--a manifesto
• 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
• Termination of constructor systems
• Title not available (Why is that?)
• Mechanical verification on strategies
• 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
• Analogy in Automated Deduction: A Survey
• 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