Superposition with Delayed Unification

DOI10.1007/978-3-031-38499-8_2MaRDI QIDQ6492727zbMATH OpenFDO

Authors Ahmed Bhayat, Johannes Schoisswohl, Michael G. Rawson

Publication date 26 April 2024

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-38499-8_2

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 comprehensive framework for saturation theorem proving
• 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 -calculus
• AVATAR: The Architecture for First-Order Theorem Provers
• Fingerprint indexing for paramodulation and rewriting
• Goal directed strategies for paramodulation
• Higher-order unification revisited: Complete sets of transformations
• scientific article; zbMATH DE number 1809862 (Why is no real title available?)
• scientific article; zbMATH DE number 1303344 (Why is no real title available?)
• scientific article; zbMATH DE number 1348470 (Why is no real title available?)
• On restrictions of ordered paramodulation with simplification
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Superposition for lambda-free higher-order logic
• Superposition with lambdas
• The higher-order prover \textsc{Leo}-II
• The higher-order prover Leo-III
• The state of CASC
• Unification theory
• Unification with abstraction and theory instantiation in saturation-based reasoning

Cited in

(4)

• A modular formalization of superposition in Isabelle/HOL
• Partial redundancy in saturation
• Reducibility constraints in superposition
• An empirical assessment of progress in automated theorem proving

This page was built for publication: Superposition with Delayed Unification

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