Abstract
In this paper we present the CPUHR-tableau calculus, a modification of positive unit hyperresolution (PURR) tableaux, the calculus underlying the model generator and theorem prover Satchmo. In addition to clausal first order logic, CPUHR tableaux are able to manipulate existentially quantified variables without Skolemization, and they allow to attach constraints to these variables as in constraint logic programming. This extension allows to handle efficiently many realistic model generation problems that cannot be handled by model generators for clausal theories such as PURR tableaux. In this paper we deal with CPUHR tableaux only for formulas without function symbols other than constants.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
F. Bry and R. Manthey. Checking consistency of database constraints: A logical basis. In 12th Int. Conf. on Very Large Data Bases (VLDB), Kyoto, Japan, 1986.
F. Bry and A. Yahya. Minimal model generation with positive unit hyper-resolution tableaux. In 5th Workshop on Theorem Proving with Tableaux and Related Methods, Springer LNAI, 1996.
F. Bry. Proving finite satisfiability of deductive databases. In Proc. of the Conference Logic and Computer Science, Karlsruhe, Germany, 1987. Springer-Verlag.
R. Caferra and N. Peltier. Model building and interactive theory discovery. In 4th Workshop on Theorem Proving with Analytic Tableaux and Related Methods 95, Springer LNAI 918, pages 154–168, 1995.
R. Caferra and N. Zabel. Extending resolution for model construction. In Logics in AL European Workshop JELIA '90, Springer LNAI 478, pages 153–169, 1991.
M. Denecker and D. De Schreye. On the duality of abduction and model generation in a framework for model generation with equality. Journal of Theoretical Computer Science, 1994.
T. Frühwirth. Constraint handling rules. In A. Podelski, editor, Constraint Programming: Basics and Trends, LNCS 910. Springer-Verlag, 1995.
J. Hintikka. Model minimization — an alternative to circumscription. Journal of Automated Reasoning, 4(1):1–14, Mar. 1988.
H. Kirchner. On the use of constraints in automated deduction. In A. Podelski, editor, Constraint Programming: Basics and Trends, LNCS 910. Springer, 1995. (Châtillon-sur-Seine Spring School, France, May 1994).
J. Lobo, J. Minker, and A. Rajasekar. Foundations of Disjunctive Logic Programming. MIT Press, 1992.
R. Manthey and F. Bry. SATCHMO: A theorem prover implemented in Prolog. In 9th Int. Conf. on Automated Deduction (CADE), Springer LNCS 310, pages 415–434, 1988.
H. Schütz and T. Geisler. Efficient model generation through compilation. In M. McRobbie and J. Slaney, editors, Proceedings of the 18th International Conference on Automated Deduction, number 1104 in Lecture Notes in Artificial Intelligence, pages 433–447. Springer-Verlag, 1996.
R. Smullyan. First-Order Logic. Springer-Verlag, 1968.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Abdennadher, S., Schütz, H. (1997). Model generation with existentially quantified variables and constraints. In: Hanus, M., Heering, J., Meinke, K. (eds) Algebraic and Logic Programming. ALP HOA 1997 1997. Lecture Notes in Computer Science, vol 1298. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0027015
Download citation
DOI: https://doi.org/10.1007/BFb0027015
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63459-1
Online ISBN: 978-3-540-69555-4
eBook Packages: Springer Book Archive