Rewriting and inductive reasoning

DOI10.29007/VBFPMaRDI QIDQ7025184zbMATH OpenFDO

Authors Márton Hajdu, Laura Kovács, Michael G. Rawson

Publication date 19 February 2025

Full work available at URL https://doi.org/10.29007/VBFP

zbMATH Keywords

inductionrewritingsaturationsuperposition

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Cites work

• Automating Inductive Proofs Using Theory Exploration
• Combining induction and saturation-based theorem proving
• Combining superposition and induction: a practical realization
• Conjecture synthesis for inductive theories
• Efficient encodings of first-order Horn formulas in equational logic
• Getting saturated with induction
• Ground joinability and connectedness in the superposition calculus
• scientific article; zbMATH DE number 193479 (Why is no real title available?)
• scientific article; zbMATH DE number 1552532 (Why is no real title available?)
• Implicit induction in conditional theories
• Induction in saturation-based proof search
• Induction with generalization in superposition reasoning
• Integer induction in saturation
• Isabelle/HOL. A proof assistant for higher-order logic
• Paramodulation-based theorem proving
• Rippling: A heuristic for guiding inductive proofs
• Seventeen provers under the hammer
• Subsumption demodulation in first-order theorem proving
• Superposition with structural induction
• TIP: tons of inductive problems

This page was built for publication: Rewriting and inductive reasoning

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