Completeness in PVS of a nominal unification algorithm
type: Item
instance of: scholarly article
title: Completeness in PVS of a nominal unification algorithm
zbMATH Open document ID: 1394.68348
author: Mauricio Ayala-Rincón
author: Maribel Fernández
author: Ana Cristina Rocha-Oliveira
publication date: 2018-04-23T00:00:00Z
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 68Q42
zbMATH DE Number: 6862942
zbMATH Keywords: nominal terms
zbMATH Keywords: binders
zbMATH Keywords: \(\alpha\)-equivalence
zbMATH Keywords: nominal unification
zbMATH Keywords: PVS
Wikidata QID: Q113317684
describes a project that uses: LCF
describes a project that uses: Isabelle/HOL
describes a project that uses: PVS
describes a project that uses: Nominal Isabelle
MaRDI profile type: Publication
full work available at URL: j.entcs.2016.06.005
OpenAlex ID: W2472676800
cites work: Nominal reasoning techniques in Coq (extended abstract)
cites work: First-order unification in the PVS proof assistant
cites work: Unification via the \(\lambda s_e\)-style of explicit substitutions
cites work: Unifying Nominal Unification
cites work: The First-Order Nominal Link
cites work: Extracting the resolution algorithm from a completeness proof for the propositional calculus
cites work: Higher order unification via explicit substitutions
cites work: Nominal rewriting
cites work: Nominal Completion for Rewrite Systems with Binders
cites work: A formalization of the Knuth-Bendix(-Huet) critical pair theorem
cites work: A unification algorithm for typed \(\bar\lambda\)-calculus
cites work: (Nominal) Unification by Recursive Descent with Triangular Substitutions
cites work: An Efficient Nominal Unification Algorithm
cites work: Nominal Unification from a Higher-Order Perspective
cites work: Verifying the unification algorithm in LCF
cites work: Nominal unification
cites work: Nominal techniques in Isabelle/HOL
DOI: 10.1016/J.ENTCS.2016.06.005
description: scientific article; zbMATH DE number 6862942