Pages that link to "Item:Q685548"

The following pages link to Rippling: A heuristic for guiding inductive proofs (Q685548):

Displaying 31 items.

• The use of embeddings to provide a clean separation of term and annotation for higher order rippling (Q540694) (← links)
• Using induction and rewriting to verify and complete parameterized specifications (Q672051) (← links)
• On process equivalence = equation solving in CCS (Q839034) (← links)
• An integrated approach to high integrity software verification (Q861714) (← links)
• Supporting the formal verification of mathematical texts (Q865656) (← links)
• Deaccumulation techniques for improving provability (Q882487) (← links)
• Rule-based induction (Q1334895) (← links)
• A recursion planning analysis of inductive completion (Q1353935) (← links)
• Constraint solving for proof planning (Q1774557) (← links)
• Sound generalizations in mathematical induction (Q1882908) (← links)
• Productive use of failure in inductive proof (Q1915134) (← links)
• Middle-out reasoning for synthesis and induction (Q1915136) (← links)
• A calculus for and termination of rippling (Q1915137) (← links)
• Proving theorems by reuse (Q1978233) (← links)
• Induction and Skolemization in saturation theorem proving (Q2084957) (← links)
• An approach to automatic deductive synthesis of functional programs (Q2457802) (← links)
• A Pragmatic Approach to Reuse in Tactical Theorem Proving (Q2841242) (← links)
• A Formalisation of Weak Normalisation (with Respect to Permutations) of Sequent Calculus Proofs (Q4506460) (← links)
• Extensions to a generalization critic for inductive proof (Q4647499) (← links)
• Patching faulty conjectures (Q4647501) (← links)
• Internal analogy in theorem proving (Q4647502) (← links)
• Termination of algorithms over non-freely generated data types (Q4647505) (← links)
• INKA: The next generation (Q4647524) (← links)
• Lemma discovery in automating induction (Q4647546) (← links)
• A case study in the mechanical verification of fault tolerance (Q4783363) (← links)
• A divergence critic (Q5210759) (← links)
• Lazy generation of induction hypotheses (Q5210761) (← links)
• Mechanizable inductive proofs for a class of ∀ ∃ formulas (Q5210766) (← links)
• Termination orderings for rippling (Q5210791) (← links)
• A colored version of the λ-calculus (Q5234713) (← links)
• Verifying Procedural Programs via Constrained Rewriting Induction (Q5278212) (← links)