First-order unification in the PVS proof assistant

DOI10.1093/JIGPAL/JZU012MaRDI QIDQ4644611zbMATH OpenOpenAlexWikidataFDO

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

Publication date 8 January 2019

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

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

zbMATH Keywords

existence of first-order unifiersfirst-order unificationPVSspecification and formalizationverification and correction of algorithms

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Recommendations

• First-order unification by structural recursion
• First-order theorem proving: foreword
• A First Step Towards a Unified Proof Checker for QBF
• scientific article; zbMATH DE number 1070624
• scientific article; zbMATH DE number 4170865
• scientific article; zbMATH DE number 1377612
• scientific article; zbMATH DE number 7333179
• Unifying Theories in ProofPower-Z

Cited in

(3)

• Completeness in PVS of a nominal unification algorithm
• Confluence of orthogonal term rewriting systems in the prototype verification system
• First-order unification by structural recursion

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

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