Refining unification with abstraction

DOI10.29007/H65JMaRDI QIDQ7025228zbMATH OpenFDO

Authors Ahmed Bhayat, Konstantin Korovin, Laura Kovács, Johannes Schoisswohl

Publication date 19 February 2025

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

zbMATH Keywords

arithmeticautomated theorem provingunificationunification with abstraction

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• A combinator-based superposition calculus for higher-order logic
• A Machine-Oriented Logic Based on the Resolution Principle
• A technical note on AC-unification. The number of minimal unifiers of the equation \(\alpha x_ 1+ \cdots + \alpha x_ p \doteq _{AC} \beta y_ 1+ \cdots + \beta y_ q\)
• A unification algorithm for typed \(\bar\lambda\)-calculus
• Faster, higher, stronger: E 2.3
• scientific article; zbMATH DE number 1303342 (Why is no real title available?)
• Implementing Superposition in iProver (System Description)
• Making theory reasoning simpler
• Paramodulation-based theorem proving
• Resolution theorem proving
• Seventeen provers under the hammer
• Superposition with lambdas
• Unification with abstraction and theory instantiation in saturation-based reasoning

Cited in

(2)

• SMT and functional equation solving over the reals: challenges from the IMO
• A higher-order Vampire (short paper)

This page was built for publication: Refining unification with abstraction

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