Skip to main content
SpringerLink
Log in

A resolution principle for clauses with constraints

  • Conference paper
  • First Online:
10th International Conference on Automated Deduction (CADE 1990)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 449))

Included in the following conference series:

Abstract

We introduce a general scheme for handling clauses whose variables are constrained by an underlying constraint theory. In general, constraints can be seen as quantifier restrictions as they filter out the values that can be assigned to the variables of a clause (or an arbitrary formulae with restricted universal or existential quantifier) in any of the models of the constraint theory. We present a resolution principle for clauses with constraints, where unification is replaced by testing constraints for satisfiability over the constraint theory. We show that this constrained resolution is sound and complete in that a set of clauses with constraints is unsatisfiable over the constraint theory iff we can deduce a constrained empty clause for each model of the constraint theory, such that the empty clauses constraint is satisfiable in that model. We show also that we cannot require a better result in general, but we discuss certain tractable cases, where we need at most finitely many such empty clauses or even better only one of them as it is known in classical resolution, sorted resolution or resolution with theory unification.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  • K.H. Bläsius, H.-J. Bürckert (eds.). Deduction Systems in Artificial Intelligence. Horwood, Chichester, 1989

    Google Scholar 

  • R.J. Brachman, J.G. Schmolze. An Overview of the KL-ONE Knowledge Representation System. Cognitive Science 9(2), 171–216, 1985.

    Google Scholar 

  • W. Buntine, H.-J. Bürckert. On Solving Equations and Disequations. SEKI-Report SR-89-03, Universität Kaiserslautern, 1989

    Google Scholar 

  • H.-J. Bürckert. Lazy Theory Unification in Prolog: An Extension of the Warren Abstract Machine. Proc. of German Workshop on Artificial Intelligence, Springer Informatik-Fachberichte 124, 277–288, 1986

    Google Scholar 

  • H.-J. Bürckert. Solving Disequations in Equational Theories. Proc. of Conf. on Automated Deduction, Springer LNCS 310, 517–526, 1988

    Google Scholar 

  • H.-J. Bürckert. A Resolution Principle for a Logic with Restricted Quantifiers. Dissertation, in prep., 1990

    Google Scholar 

  • C.-L. Chang, R.C.-T. Lee. Symbolic Logic and Mechanical Theorem Proving. Academic Press, 1973

    Google Scholar 

  • A. Colmerauer. Equations and Inequations on Finite and Infinite Trees. Proc. of Conf. on Fifth Generation Computer Systems, 85–99, 1984

    Google Scholar 

  • M. Dincbas, P. van Hentenryck, H. Simonis, A. Aggoun, T. Graf, F. Berthin. The Constraint Logic Programming Language CHIP. Proc. of Conf. on Fifth Generation Computer Systems, 1988

    Google Scholar 

  • A. Frisch. A General Framework for Sorted Deduction: Fundamenrtal Results on Hybrid Reasoning. Conf. on Principles of Knowledge Representation and Reasoning, 126–136, 1989

    Google Scholar 

  • J. Gallier, S. Raatz. SLD-Resolution Methods for Horn Clauses with Equality Based on E-Unification. Proc. of Symp. on Logic Programming, 1986

    Google Scholar 

  • J. Gallier. Logic for Computer Science: Foundations of Automatic Theorem Proving. Harper and Row, 1986

    Google Scholar 

  • M.R. Genesereth, N.J. Nilsson. Logical Foundations of Artificial Intelligence. Morgan Kaufmann, 1987

    Google Scholar 

  • J.A. Goguen, J. Meseguer. Equalities, Types, Modules, and Generics for Logic Programming. J. of Logic Programming 1, 179–210, 1984

    Google Scholar 

  • M. Höhfeld, G. Smolka. Definite Relations over Constraint Languages. LILOG-Report 53, IBM Deutschland, 1988

    Google Scholar 

  • G. Huet. Constrained Resolution — A Complete Method for Higher Order Logic. Ph.D. Thesis, Case Western University, 1972

    Google Scholar 

  • J. Jaffar, J.-L. Lassez. Constrained Logic Programming. Proc. of ACM Symp. on Principles of Programming Languages, 111–119, 1987

    Google Scholar 

  • J. Jaffar, J.-L. Lassez, M. Maher. Logic Programming Scheme. In: Logic Programming: Functions, Relations, Equations (eds. D. De Groot, G. Lindstrom), Prentice Hall, 1986

    Google Scholar 

  • C. Kirchner (ed.). Special Issue on Unification. J. of Symbolic Computation, 1989

    Google Scholar 

  • R. Kowalski. Logic for Problem Solving. North-Holland, 1979

    Google Scholar 

  • J.W. Lloyd. Foundations of Logic Programming. Springer, 1987

    Google Scholar 

  • D.W. Loveland. Automated Theorem Proving: A Logical Basis. North-Holland, 1978

    Google Scholar 

  • B. Nebel. Reasoning and Revision in Hybrid Representation Systems. Dissertation, Universität Saarbrücken, 1989

    Google Scholar 

  • A. Oberschelp. Untersuchungen zur mehrsortigen Quantorenlogik (in German). Mathematische Annalen 145, 297–333, 1962

    Google Scholar 

  • H.J. Ohlbach. The Semantic Clause Graph Procedure — A First Overview. Proc. of German Workshop on Artificial Intelligence, Springer Informatik-Fachberichte 124, 218–229, 1986

    Google Scholar 

  • G. Plotkin. Building in Equational Theories. Machine Intelligence 7, 1972

    Google Scholar 

  • J.A. Robinson. A Machine Oriented Logic Based on the Resolution Principle. Journal of the ACM 12(1), 1965

    Google Scholar 

  • M. Schmidt-Schauß. Computational Aspects of an Order-Sorted Logic with Term Declarations. Springer LNAI 395, 1989

    Google Scholar 

  • J.R. Shoenfield. Mathematical Logic. Addison Wesley, 1967

    Google Scholar 

  • J.H. Siekmann. Unification Theory — A Survey. In: Special Issue on Unification (ed. C. Kirchner), J. of Symbolic Computation, 1989

    Google Scholar 

  • G. Smolka. Logic Programming over Polymorphically Order-Sorted Types. Dissertation, Universität Kaiserslautern, 1989

    Google Scholar 

  • G. Smolka, W. Nutt, J.A. Goguen, J. Meseguer. Order-Sorted Equational Computation. In: Resolution of Equations in Algebraic Structures (eds. H. Ait-Kaci, M. Nivat). Prentice Hall, 1989

    Google Scholar 

  • M.E. Stickel. Automated Deduction by Theory Resolution. J. of Automated Reasoning 1(4), 1985

    Google Scholar 

  • C. Walther. A Many-Sorted Calculus Based on Resolution and Paramodulation. Pitman & Morgan Kaufmann Publishers, Research Notes in Artificial Intelligence, 1987

    Google Scholar 

  • L. Wos, G. Robinson. Paramodulation and the Set of Support. Proc. of Symp. on Automated Demonstration, Springer, 1970

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. DFKI, Project Group AKA-WINO, Postfach 2080, D-6750, Kaiserslautern, FR Germany

    Hans-Jürgen Bürckert

Authors
  1. Hans-Jürgen Bürckert
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Mark E. Stickel

Rights and permissions

Reprints and permissions

Copyright information

© 1990 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Bürckert, HJ. (1990). A resolution principle for clauses with constraints. In: Stickel, M.E. (eds) 10th International Conference on Automated Deduction. CADE 1990. Lecture Notes in Computer Science, vol 449. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-52885-7_87

Download citation

  • DOI: https://doi.org/10.1007/3-540-52885-7_87

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-52885-2

  • Online ISBN: 978-3-540-47171-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation