Higher order E-unification

DOI10.1007/3-540-52885-7_115MaRDI QIDQ6488561zbMATH OpenFDO

Authors Wayne Snyder

Publication date 28 April 2023

Full work available at URL https://doi.org/10.1007/3-540-52885-7_115

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40) Grammars and rewriting systems (68Q42)

Recommendations

• A combinatory logic approach to higher-order E-unification
• Modular higher-order E-unification
• scientific article; zbMATH DE number 1088023
• Higher-order unification revisited: Complete sets of transformations
• Higher-order unification via combinators

Cites work

• A Machine-Oriented Logic Based on the Resolution Principle
• A unification algorithm for typed \(\bar\lambda\)-calculus
• An Efficient Unification Algorithm
• Complete sets of transformations for general E-unification
• Complete sets of unifiers and matchers in equational theories
• Higher-order unification revisited: Complete sets of transformations
• scientific article; zbMATH DE number 3878393 (Why is no real title available?)
• scientific article; zbMATH DE number 3988745 (Why is no real title available?)
• scientific article; zbMATH DE number 3993540 (Why is no real title available?)
• scientific article; zbMATH DE number 3999882 (Why is no real title available?)
• scientific article; zbMATH DE number 3413831 (Why is no real title available?)
• Natural deduction as higher-order resolution
• Termination of rewriting
• Theorem Proving via General Matings
• Unification theory

Cited in

(24)

• A proof theory for general unification
• Higher order unification via explicit substitutions
• Comparing approaches to resolution based higher-order theorem proving
• Functions-as-constructors higher-order unification: extended pattern unification
• Higher-order unification via combinators
• Higher-order unification and matching
• scientific article; zbMATH DE number 4045129 (Why is no real title available?)
• scientific article; zbMATH DE number 1189062 (Why is no real title available?)
• scientific article; zbMATH DE number 1303338 (Why is no real title available?)
• scientific article; zbMATH DE number 1088023 (Why is no real title available?)
• scientific article; zbMATH DE number 1927411 (Why is no real title available?)
• scientific article; zbMATH DE number 1377612 (Why is no real title available?)
• Rewriting, and equational unification: the higher-order cases
• Goal directed strategies for paramodulation
• Modular higher-order E-unification
• Efficient second-order matching
• Modular AC unification of higher-order patterns
• Theory and practice of minimal modular higher-order \(E\)-unification
• Superposition with lambdas
• Superposition with lambdas
• E-unification for second-order abstract syntax
• A combinatory logic approach to higher-order E-unification
• Modular higher-order equational preunification
• One is all you need: associative second-order unification without first-order variables

This page was built for publication: Higher order E-unification

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