A certified functional nominal C-unification algorithm

DOI10.1007/978-3-030-45260-5_8MaRDI QIDQ5097631zbMATH OpenOpenAlexFDO

Authors Mauricio Ayala-Rincón, Maribel Fernández, G. F. Silva, Daniele Nantes-Sobrinho

Publication date 25 August 2022

Published in Logic-Based Program Synthesis and Transformation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-030-45260-5_8

zbMATH Keywords

nominal C-unificationnominal termsverification of functional specifications

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Nominal C-unification
• Completeness in PVS of a nominal unification algorithm
• A polynomial nominal unification algorithm
• Formalising nominal C-unification generalised with protected variables
• An efficient nominal unification algorithm

Cites work

• (Nominal) unification by recursive descent with triangular substitutions
• A formalisation of nominal \(\alpha\)-equivalence with A and AC function symbols
• A formalisation of nominal \(\alpha\)-equivalence with A, C, and AC function symbols
• A polynomial nominal unification algorithm
• An efficient nominal unification algorithm
• Complete axiomatizations of some quotient term algebras
• Completeness in PVS of a nominal unification algorithm
• Fixed-point constraints for nominal equational unification
• Logic Programming
• Nominal anti-unification
• Nominal C-unification
• Nominal narrowing
• Nominal rewriting
• Nominal sets. Names and symmetry in computer science
• Nominal techniques in Isabelle/HOL
• Nominal unification
• Nominal unification of higher order expressions with recursive let
• Term Rewriting and All That
• Unification theory

Cited in

(8)

• Nominal C-unification
• Completeness in PVS of a nominal unification algorithm
• A formalisation of nominal C-matching through unification with protected variables
• A formalisation of nominal \(\alpha\)-equivalence with A, C, and AC function symbols
• Formalising nominal C-unification generalised with protected variables
• Rewriting with generalized nominal unification
• Nominal AC-matching
• Unranked Nominal Unification

This page was built for publication: A certified functional nominal C-unification algorithm

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