Connection-driven inductive theorem proving

DOI10.1023/A:1013874024997MaRDI QIDQ5955618zbMATH OpenOpenAlexFDO

Authors Christoph Kreitz, Brigitte Pientka

Publication date 16 September 2002

Published in Studia Logica (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1023/a:1013874024997

zbMATH Keywords

inductionripplingprogram synthesisinductive theorem provingmatrix-based theorem proving

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mechanization of proofs and logical operations (03B35)

Recommendations

• scientific article; zbMATH DE number 1612558
• scientific article; zbMATH DE number 1748580
• scientific article; zbMATH DE number 1389654
• Rippling: A heuristic for guiding inductive proofs
• Extensions to the rippling-out tactic for guiding inductive proofs

Cited in

(9)

• Inductive theorem proving based on tree grammars
• Focused Inductive Theorem Proving
• FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover
• scientific article; zbMATH DE number 1765687 (Why is no real title available?)
• scientific article; zbMATH DE number 1612558 (Why is no real title available?)
• scientific article; zbMATH DE number 1748580 (Why is no real title available?)
• Connection calculus theorem proving with multiple built-in theories
• scientific article; zbMATH DE number 1389654 (Why is no real title available?)
• scientific article; zbMATH DE number 549993 (Why is no real title available?)

This page was built for publication: Connection-driven inductive theorem proving

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