scientific article; zbMATH DE number 1389654

MaRDI QIDQ4934147zbMATH OpenFDO

Authors Brigitte Pientka, Christoph Kreitz

Publication date 17 January 2000

zbMATH Keywords

logical proof searchrippling heuristics

Mathematics Subject Classification ID

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

Cited in

(15)

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

Describes a project that uses

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)