Superposition with Delayed Unification

DOI10.1007/978-3-031-38499-8_2MaRDI QIDQ6492727

Ahmed Bhayat, Johannes Schoisswohl, Michael G. Rawson

Publication date: 26 April 2024

Mathematics Subject Classification ID

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The higher-order prover \textsc{Leo}-II
• 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 \(\overline\lambda\)-calculus
• The higher-order prover Leo-III
• Higher-order unification revisited: Complete sets of transformations
• A combinator-based superposition calculus for higher-order logic
• Unification with abstraction and theory instantiation in saturation-based reasoning
• Fingerprint Indexing for Paramodulation and Rewriting
• AVATAR: The Architecture for First-Order Theorem Provers
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Goal directed strategies for paramodulation
• A comprehensive framework for saturation theorem proving
• Superposition with lambdas
• On restrictions of ordered paramodulation with simplification

This page was built for publication: Superposition with Delayed Unification