On Extending Bounded Proofs to Inductive Proofs

DOI10.1007/978-3-642-02658-4_23MaRDI QIDQ3636868zbMATH OpenOpenAlexFDO

Authors Oded Fuhrmann, Shlomo Hoory

Publication date 30 June 2009

Published in Computer Aided Verification (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-02658-4_23

zbMATH Keywords

extending proofsformal verificationproof simplificationresolution proofs

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Bounded model checking and induction: From refutation to verification (extended abstract, Category A)
• scientific article; zbMATH DE number 1670785
• Combining induction and saturation-based theorem proving
• Extended Resolution Proofs for Conjoining BDDs
• scientific article; zbMATH DE number 938516

Cited in

(4)

• On the proof-theoretic strength of monotone induction in explicit mathematics
• Well-behaved principles alternative to bounded induction
• On Inductive and Coinductive Proofs via Unfold/Fold Transformations
• The bounded proof property via step algebras and step frames

This page was built for publication: On Extending Bounded Proofs to Inductive Proofs

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