The Qu-Prolog unification algorithm: formalisation and correctness
From MaRDI portal
Recommendations
- Formal correctness of a quadratic unification algorithm
- On Unification of QBF Resolution-Based Calculi
- A unified proof system for QBF preprocessing
- Unification algorithms for eliminating and introducing quantifiers in natural deduction automated theorem proving
- Quantified logic programs, revisited
- A First Step Towards a Unified Proof Checker for QBF
- Synthesis of a unification algorithm in a logic programming calculus
- scientific article; zbMATH DE number 1223549
- Unification as a complexity measure for logic programming
Cites work
- scientific article; zbMATH DE number 3872640 (Why is no real title available?)
- scientific article; zbMATH DE number 1158760 (Why is no real title available?)
- scientific article; zbMATH DE number 3304881 (Why is no real title available?)
- scientific article; zbMATH DE number 3400430 (Why is no real title available?)
- A unification algorithm for typed \(\overline\lambda\)-calculus
- Substitution revisited
Cited in
(8)- Correctness of unification without occur check in prolog
- scientific article; zbMATH DE number 4043301 (Why is no real title available?)
- On Unification of QBF Resolution-Based Calculi
- Formal correctness of a quadratic unification algorithm
- Nominal unification
- Contextual equivalence for inductive definitions with binders in higher order typed functional programming
- Synthesis of a unification algorithm in a logic programming calculus
- Ergo 6: A Generic Proof Engine that Uses Prolog Proof Technology
This page was built for publication: The Qu-Prolog unification algorithm: formalisation and correctness
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1349886)
