Model generation and existentially quantified variables and constraints

DOI10.1007/BFB0027015MaRDI QIDQ4364380zbMATH OpenFDO

Authors Slim Abdennadher, Heribert Schütz

Publication date 14 June 1998

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/BFB0027015

zbMATH Keywords

constraintsCPUHR tableau calculusHerbrand model generationmodel generator Satchmomodification of PUHR

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Logic programming (68N17) Database theory (68P15)

Review text

Using the idea of Herbrand model generation for construction of interpretations that satisfy a given theory, the Satchmo system was early developed to check the consistency of integrity constraints in relational databases. If Satchmo can generate a Herbrand model for the constraints, then the constraints are consistent and they be satisfied by some database instance. There are systems, e.g. PUHR (positive unit hyper-resolution) tableau calculus, which underlie the model generator Satchmo). In this paper, CPUHR tableau calculus is proposed as a modification of PUHR tableau at constraints. The fundamental advantage of the CPUHR system is the ability to manipulate existentially quantified variables without Skolemization, in order to attach constraints to the variable as in logic programming. Some soundness and completeness properties of the CPUHR tableau calculus with respect to model generation are presented. This approach can be seen as an extension of disjunctive logic programming with forward chaining by constraints. For the entire collection see [Zbl 0871.00033].

Recommendations

• Positive unit hyperresolution tableaux and their application to minimal model generation
• Minimal model generation with positive unit hyper-resolution tableaux
• Efficient model generation through compilation.
• SHR tableaux -- a framework for automated model generation
• scientific article; zbMATH DE number 1841823

Cited in

(2)

• Blocking and Other Enhancements for Bottom-Up Model Generation Methods
• A Transformation-Based Approach to View Updating in Stratifiable Deductive Databases

This page was built for publication: Model generation and existentially quantified variables and constraints

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