Strategic issues, problems and challenges in inductive theorem proving

MaRDI QIDQ2848043zbMATH OpenFDO

Authors Bernhard Gramlich

Publication date 25 September 2013

Full work available at URL http://www.sciencedirect.com/science/article/pii/S1571066105000940

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• The automation of proof by mathematical induction
• scientific article; zbMATH DE number 907678
• Some observations on the logical foundations of inductive theorem proving
• TIP: tons of inductive problems
• An Interactive Driver for Goal-directed Proof Strategies

Cited in

(4)

• TIP: tons of inductive problems
• Some observations on the logical foundations of inductive theorem proving
• A unified view of induction reasoning for first-order logic
• The failure of cut-elimination in cyclic proof for first-order logic with inductive definitions

Describes a project that uses

Uses Software

• NQTHM
• SPIKE

This page was built for publication: Strategic issues, problems and challenges in inductive theorem proving

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