scientific article; zbMATH DE number 3986670

MaRDI QIDQ3750141zbMATH OpenFDO

Authors Dieter Hutter

Publication date 1986

zbMATH Keywords

symbolic evaluationInductive theorem proversresolution prover for simplifying formulas in a goal-directed way

Mathematics Subject Classification ID

Recommendations

• The automation of proof by mathematical induction
• Induction proofs with partial functions
• scientific article; zbMATH DE number 1614706
• Automatic inductive theorem proving using Prolog
• Combining induction and saturation-based theorem proving

Cited in

(2)

• Guiding induction proofs
• Proof normalization for resolution and paramodulation

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 Q3750141)