First-order unification in the PVS proof assistant

DOI10.1093/jigpal/jzu012zbMath1407.68430OpenAlexW1973876376WikidataQ58001385 ScholiaQ58001385MaRDI QIDQ4644611

Andréia Borges Avelar, Flávio L. C. de Moura, Mauricio Ayala-Rincón, André Luiz Galdino

Publication date: 8 January 2019

Published in: Logic Journal of IGPL (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1093/jigpal/jzu012

zbMATH Keywords

PVSfirst-order unificationexistence of first-order unifiersspecification and formalizationverification and correction of algorithms

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items (2)

Confluence of orthogonal term rewriting systems in the prototype verification system ⋮ Completeness in PVS of a nominal unification algorithm

This page was built for publication: First-order unification in the PVS proof assistant