Abstract
This paper looks at the addition of equality reasoning to systems that perform constrained resolution as defined within the substitutional framework. These systems reason with a constraint logic in which the constraints are interpreted relative to a constraint theory. First, a special case is considered when equality can be treated as a constraint. Then the general case is dealt with by developing and proving correct the rule of constrained paramodulation, which along with the rule of constrained resolution (and factoring) yields a refutationally complete set of inference rules for languages with equality. It is shown that if certain conditions are met, paramodulation into variables is not necessary and the functionally reflexive axioms need not be present. The modal case satisfies these conditions. If other weaker conditions are met, paramodulation into variables is necessary, but the functionally reflexive axioms are not needed. Some sorted logics satisfy these conditions. The analysis provides a means of extending restrictions on resolution and paramodulation (e.g. ordering restrictions) to constrained deduction, a relatively clean and simple mechanism for adding paramodulation to sorted logics and a proof of the conjectures of Walther and Schmidt-Schauss on the need for paramodulation into variables and the functionally reflexive axioms in the case of sorted logics.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Auffray, Yves and Enjalbert, Patrice 1989. Modal theorem proving: An equational viewpoint. In Proceedings of the Eleventh International Joint Conference on Artificial Intelligence, Detroit. 441–445.
Brand, D. 1975. Proving theorems with the modification method. Siam Journal of Computation 4(4):412–430.
Bürckert, Hans Jürgen 1990. A resolution principle for clauses with constraints. In Stickel, M. E., editor 1990, 10th International Conference on Automated Deduction, volume 449 of Lecture Notes in Artificial Intelligence. Springer-Verlag, Kaiserslautern, FRG. 178–192.
Chang, Chin-Liang and Lee, Richard Char-Tung 1973. Symbolic Logic and Mechanical Theorem Proving. Academic Press.
Frisch, Alan and Scherl, Richard 1991. A general framework for modal deduction. In Allen, J.A.; Fikes, R.; and Sandewall, E., editors 1991, Principles of Knowledge Representation and Reasoning: Proceedings of the Second International Conference, San Mateo, CA: Morgan Kaufmann. 196–207.
Frisch, Alan M. 1989. A general framework for sorted deduction: Fundamental results on hybrid reasoning. In Brachman, Ronald J.; Levesque, Hector J.; and Reiter, Raymond, editors 1989, Proceedings of the First International Conference on Principles of Knowledge Representation and Reasoning, Toronto. 126–136.
Frisch, Alan M. 1991. The substitutional framework for sorted deduction: Fundamental results on hybrid reasoning. Artificial Intelligence 49(1–3):161–198.
Frisch, Alan M. 1992. Deduction with constraints: The substitutional framework for hybrid reasoning.
Hsiang, Jieh and Rusinowitch, Michael 1991. Proving refutational completeness of theorem-proving strategies: The transfinite semantic tree method. Journal of the Association for Computing Machinery 38(3):559–587.
Kirchner, Claude; Kirchner, Hélène; and Rusinowitch, M. 1990. Deduction with symbolic constraints. Revue d'Intelligence Artificielle 4(3):9–52. Special issue on Automatic Deduction.
Loveland, Donald W. 1978. Automated Theorem Proving: A Logical Basis, volume 6 of Fundamental Studies in Computer Science. North-Holland Publishing Company, Amsterdam.
Moore, R.C. 1980. Reasoning about knowledge and action. Technical Note 191, SRI International.
Ohlbach, Hans Jürgen 1988. A resolution calculus for modal logic. In Lusk, E. and Overbeek, R., editors 1988, 9th International Conference on Automated Deduction, volume 310 of Lecture Notes in Computer Science. Springer-Verlag, Berlin. 500–516.
Peterson, Gerald E. 1983. A technique for establishing completeness results in theorem proving with equality. SIAM Journal of Computing 12(1):82–100.
Plotkin, Gordon 1972. Building in equational theories. Machine Intelligence 7:73–90.
Robinson, G. and Wos, L. 1969. Paramodulation and theorem proving in first-order theories with equality. In Meltzer, B. and Michie, D., editors 1969, Machine Intelligence 4. Edinburgh University Press, Edinburgh. 135–150. Reprinted in Automation of Reasoning 2 edited by Siekmann and Wrightson.
Scherl, Richard 1992. A Constraint Logic Approach To Automated Modal Deduction. Ph.D. Dissertation, University of Illinois.
Schmidt-Schauss, M. 1989. Computational Aspects of an Order-Sorted Logic with Term Declarations, volume 395 of Lecture Notes in Artificial Intelligence. Springer-Verlag, Berlin.
Walther, Christoph 1987. A Many-Sorted Calculus Based on Resolution and Paramodulation. Morgan Kaufman, Los Altos, CA.
Wos, L.T. and Robinson, G.A. 1973. Maximal models and refutation completeness: Semidecision procedures in automatic theorem proving. In Boone, W.; Cannonito, F.; and Lyndon, R., editors 1973, Word Problems: Decision Problems and the Burnside Problem in Group Theory. North Holland, New York, N.Y. 609–639. Reprinted in Automation of Reasoning 2, edited by Siekmann and Wrightson.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Scherl, R. (1994). Equality and constrained resolution. In: MacNish, C., Pearce, D., Pereira, L.M. (eds) Logics in Artificial Intelligence. JELIA 1994. Lecture Notes in Computer Science, vol 838. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0021971
Download citation
DOI: https://doi.org/10.1007/BFb0021971
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58332-5
Online ISBN: 978-3-540-48657-2
eBook Packages: Springer Book Archive