Formal correctness of a quadratic unification algorithm

DOI10.1007/S10817-006-9030-5MaRDI QIDQ877825zbMATH OpenOpenAlexFDO

Authors José Luis Ruiz-Reina, Francisco Jesús Martín-Mateos, Jose Antonio Alonso, María José Hidalgo

Publication date 3 May 2007

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://idus.us.es/handle//11441/86262

Mathematics Subject Classification ID

Graph theory (including graph drawing) in computer science (68R10)

Recommendations

• The Qu-Prolog unification algorithm: formalisation and correctness
• scientific article; zbMATH DE number 1841814
• scientific article; zbMATH DE number 4023248
• On Unification of QBF Resolution-Based Calculi
• scientific article; zbMATH DE number 4076602
• A unified proof system for QBF preprocessing
• Coinductive Correctness of Homographic and Quadratic Algorithms for Exact Real Numbers
• Formalizing termination proofs under polynomial quasi-interpretations
• A First Step Towards a Unified Proof Checker for QBF
• scientific article; zbMATH DE number 2080213

Cites work

• scientific article; zbMATH DE number 3827203 (Why is no real title available?)
• scientific article; zbMATH DE number 46981 (Why is no real title available?)
• Formal proofs about rewriting using ACL2
• Term Rewriting and All That
• Unification theory

Cited in

(5)

• Verification of the Completeness of Unification Algorithms à la Robinson
• Verifying the unification algorithm in LCF
• The Qu-Prolog unification algorithm: formalisation and correctness
• Formalization of the resolution calculus for first-order logic
• Logic Based Program Synthesis and Transformation

Describes a project that uses

Uses Software

• ACL2
• LISP

This page was built for publication: Formal correctness of a quadratic unification algorithm

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