swMATH19619MaRDI QIDQ31444FDOQ31444
Author name not available (Why is that?)
Official website: http://rd.springer.com/chapter/10.1007%2F3-540-52885-7_123?LI=true
Cited In (64)
- An approach to automatic deductive synthesis of functional programs
- On process equivalence = equation solving in CCS
- Rippling: A heuristic for guiding inductive proofs
- Analogy in automated deduction: a survey
- Automating the synthesis of decision procedures in a constructive metatheory
- KI 2004: Advances in Artificial Intelligence
- 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?)
- \textit{Mollusc}: a general proof-development shell for sequent-based logics
- Proof planning for strategy development
- Plans and planning in mathematical proofs
- Multilanguage hierarchical logics, or: How we can do without modal logics
- Termination of constructor systems
- SCR
- SPIKE
- Amphion
- Tactician
- OMEGA
- InKa
- Lambda-Clam
- MKRP
- Oyster
- XBarnacle
- Prodigy
- Bliksem
- Doris
- KOMET
- MATHsAiD
- Medmaker
- P.rex
- PROTEIN
- GETFOL
- QuodLibet
- CoCLAM
- RRL
- TAME
- Mollusc
- Mechanical verification on strategies
- Computer-assisted human-oriented inductive theorem proving by \textit{descente infinie} -- a manifesto
- 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
- 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
