Oyster

swMATH19629MaRDI QIDQ31454

No author found.

Related Items (32)

Rule-based induction ⋮ On process equivalence = equation solving in CCS ⋮ Termination of constructor systems ⋮ Mechanical verification on strategies ⋮ Computer supported mathematics with \(\Omega\)MEGA ⋮ Supporting the formal verification of mathematical texts ⋮ Productive use of failure in inductive proof ⋮ Middle-out reasoning for synthesis and induction ⋮ A calculus for and termination of rippling ⋮ Using tactics to reformulate formulae for resolution theorem proving ⋮ Concept Formation via Proof Planning Failure ⋮ An approach to automatic deductive synthesis of functional programs ⋮ Proving theorems by reuse ⋮ Mechanizing Mathematical Reasoning ⋮ Extensions to a generalization critic for inductive proof ⋮ Termination of algorithms over non-freely generated data types ⋮ Rippling: A heuristic for guiding inductive proofs ⋮ Computer-assisted human-oriented inductive theorem proving by descente infinie--a manifesto ⋮ Analogy in Automated Deduction: A Survey ⋮ Proofs-as-programs as a framework for the design of an analogy-based ML editor ⋮ TacticToe: learning to prove with tactics ⋮ KI 2004: Advances in Artificial Intelligence ⋮ Lemma discovery for induction. A survey ⋮ Termination orderings for rippling ⋮ Mollusc a general proof-development shell for sequent-based logics ⋮ Unnamed Item ⋮ Using a generalisation critic to find bisimulations for coinductive proofs ⋮ Unnamed Item ⋮ Planning proofs of equations in CCS ⋮ Making a productive use of failure to generate witnesses for coinduction from divergent proof attempts ⋮ Experiments with proof plans for induction ⋮ PLANS AND PLANNING IN MATHEMATICAL PROOFS

This page was built for software: Oyster