CLAM

swMATH19619MaRDI QIDQ31444FDOQ31444

Author name not available (Why is that?)

Cited In (40)

• 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
• On process equivalence = equation solving in CCS
• Rippling: A heuristic for guiding inductive proofs
• Automating the synthesis of decision procedures in a constructive metatheory
• KI 2004: Advances in Artificial Intelligence
• Computer-assisted human-oriented inductive theorem proving by descente infinie--a manifesto
• Title not available (Why is that?)
• Mechanizing Mathematical Reasoning
• An integrated approach to high integrity software verification
• Supporting the formal verification of mathematical texts
• Mechanizing Mathematical Reasoning
• Extensions to a generalization critic for inductive proof
• 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
• Title not available (Why is that?)
• Proof planning for strategy development
• Multilanguage hierarchical logics, or: How we can do without modal logics
• Termination of constructor systems
• Mechanical verification on strategies
• Reasoning About Incompletely Defined Programs
• Lemma discovery for induction. A survey
• A recursion planning analysis of inductive completion
• Analogy in inductive theorem proving
• Title not available (Why is that?)
• Termination orderings for rippling
• Making a productive use of failure to generate witnesses for coinduction from divergent proof attempts
• TAME: Using PVS strategies for special-purpose theorem proving
• 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
• Internal analogy in theorem proving

This page was built for software: CLAM