Completeness in PVS of a nominal unification algorithm
From MaRDI portal
Publication:1744405
DOI10.1016/j.entcs.2016.06.005zbMath1394.68348OpenAlexW2472676800WikidataQ113317684 ScholiaQ113317684MaRDI QIDQ1744405
Ana Cristina Rocha-Oliveira, Maribel Fernández, Mauricio Ayala-Rincón
Publication date: 23 April 2018
Full work available at URL: https://doi.org/10.1016/j.entcs.2016.06.005
Related Items (7)
Nominal Unification and Matching of Higher Order Expressions with Recursive Let ⋮ A Certified Functional Nominal C-Unification Algorithm ⋮ Nominal AC-matching ⋮ A formalisation of nominal \(\alpha\)-equivalence with A, C, and AC function symbols ⋮ A formalisation of nominal \(\alpha\)-equivalence with A and AC function symbols ⋮ A formalisation of nominal C-matching through unification with protected variables ⋮ Formalising nominal C-unification generalised with protected variables
Uses Software
Cites Work
- Unnamed Item
- A formalization of the Knuth-Bendix(-Huet) critical pair theorem
- Extracting the resolution algorithm from a completeness proof for the propositional calculus
- Nominal techniques in Isabelle/HOL
- Verifying the unification algorithm in LCF
- A unification algorithm for typed \(\bar\lambda\)-calculus
- Higher order unification via explicit substitutions
- Nominal unification
- Nominal rewriting
- Unification via the se-style of explicit substitutions
- Unifying Nominal Unification
- The First-Order Nominal Link
- Nominal Completion for Rewrite Systems with Binders
- First-order unification in the PVS proof assistant
- An Efficient Nominal Unification Algorithm
- (Nominal) Unification by Recursive Descent with Triangular Substitutions
- Nominal Unification from a Higher-Order Perspective
This page was built for publication: Completeness in PVS of a nominal unification algorithm
