Constraint Logic Programming with Hereditary Harrop Formulas

Title: Constraint Logic Programming with Hereditary Harrop Formulas

Research Question: How can we combine the benefits of Constraint Logic Programming (CLP) and Hereditary Harrop Formulas (HH) to create a more expressive and efficient logic programming language?

Methodology: The researchers proposed a novel approach to combine the syntax and proof theory of HH with a given constraint system. They aimed to preserve the key property of HH as a logic programming language, namely the existence of uniform proofs, while enriching the expressivity and efficiency of the language. They also presented a goal solving procedure for this new language, ensuring its soundness and completeness.

Results: The researchers introduced a new language scheme called HH(X), with instances HH(C) for any constraint system C. They defined an amalgamated proof system that combined inference rules from intuitionistic sequent calculus with constraint entailment. This allowed them to create a more expressive and efficient logic programming language that incorporated the benefits of both CLP and HH.

Implications: The combination of CLP and HH has significant implications for the field of logic programming. It provides a more expressive and efficient language that can be used to solve complex combinatorial problems. The new language scheme HH(X) with instances HH(C) allows for a broad range of applications, as it is valid for any constraint system C. Furthermore, the soundness and completeness of the goal solving procedure ensures that the language can be used reliably for programming and problem-solving.

Link to Article: https://arxiv.org/abs/0404053v1 Authors: arXiv ID: 0404053v1