scientific article; zbMATH DE number 1389654

zbMATH Open0951.68145MaRDI QIDQ4934147FDOQ4934147

Authors: Brigitte Pientka, Christoph Kreitz 

Publication date: 17 January 2000

Title of this publication is not available (Why is that?)

Recommendations

• Connection-driven inductive theorem proving
• Rippling: A heuristic for guiding inductive proofs
• scientific article; zbMATH DE number 3880144
• Extensions to the rippling-out tactic for guiding inductive proofs
• The automation of proof by mathematical induction

zbMATH Keywords

logical proof searchrippling heuristics

Mathematics Subject Classification ID

Cited In (15)

• Improving automation for higher-order proof steps
• An approach to automatic deductive synthesis of functional programs
• Automating Induction with an SMT Solver
• Automatic inductive theorem proving using Prolog
• Title not available (Why is that?)
• Automating Inductive Proofs Using Theory Exploration
• Title not available (Why is that?)
• Automated Certification of Implicit Induction Proofs
• Automata-driven automated induction
• Title not available (Why is that?)
• Title not available (Why is that?)
• Automating Side Conditions in Formalized Partial Functions
• Dynamic rippling, middle-out reasoning and lemma discovery
• Connection-driven inductive theorem proving
• Inductive theorem proving for design specifications

Uses Software

• Nuprl

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4934147)