Completeness in PVS of a nominal unification algorithm

DOI10.1016/J.ENTCS.2016.06.005MaRDI QIDQ1744405zbMATH OpenOpenAlexWikidataFDO

Authors Mauricio Ayala-Rincón, Maribel Fernández, Ana Cristina Rocha-Oliveira

Publication date 23 April 2018

Full work available at URL https://doi.org/10.1016/j.entcs.2016.06.005

zbMATH Keywords

\(\alpha\)-equivalencebindersnominal termsnominal unificationPVS

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Grammars and rewriting systems (68Q42)

Recommendations

• A certified functional nominal C-unification algorithm
• Nominal C-unification
• Nominal unification
• Computer Science Logic
• Nominal unification with atom-variables

Cites work

• (Nominal) unification by recursive descent with triangular substitutions
• A formalization of the Knuth-Bendix(-Huet) critical pair theorem
• A unification algorithm for typed \(\bar\lambda\)-calculus
• An efficient nominal unification algorithm
• Extracting the resolution algorithm from a completeness proof for the propositional calculus
• First-order unification in the PVS proof assistant
• Higher order unification via explicit substitutions
• Nominal completion for rewrite systems with binders
• Nominal reasoning techniques in Coq (extended abstract)
• Nominal rewriting
• Nominal techniques in Isabelle/HOL
• Nominal unification
• The First-Order Nominal Link
• Unification via the s_e-style of explicit substitutions
• Unifying nominal unification
• Verifying the unification algorithm in LCF

Cited in

(16)

• Nominal essential intersection types
• A formalisation of nominal \(\alpha\)-equivalence with A and AC function symbols
• Understanding PPA-completeness
• A formalisation of nominal C-matching through unification with protected variables
• A formalisation of nominal \(\alpha\)-equivalence with A, C, and AC function symbols
• Nominal completion for rewrite systems with binders
• scientific article; zbMATH DE number 4053008 (Why is no real title available?)
• Verification of the Completeness of Unification Algorithms à la Robinson
• Formalising nominal C-unification generalised with protected variables
• Nominal Unification and Matching of Higher Order Expressions with Recursive Let
• A certified functional nominal C-unification algorithm
• Understanding PPA-completeness
• Nominal AC-matching
• Unranked Nominal Unification
• Nominal equational rewriting and narrowing
• Certified first-order AC-unification and applications.

Describes a project that uses

Uses Software

• LCF
• Isabelle/HOL
• PVS
• Nominal Isabelle

This page was built for publication: Completeness in PVS of a nominal unification algorithm

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