Abstract
In this paper we study the subsumption inference rule in the context of distributed deduction. It is well known that the unrestricted application of subsumption may destroy the fairness and thus the completeness of a deduction strategy. Solutions to this problem in sequential theorem proving are known. We observe that in distributed automated deduction, subsumption may also thwartmonotonicity, a dual property of soundness, in addition to completeness. Not only do the solutions for the sequential case not apply, even proper subsumption may destroy monotonicity in the distributed case.
We present these problems and propose a general solution that treats subsumption as a composition of a replacement inference rule,replacement subsumption, and a deletion inference rule,variant subsumption. (Proper subsumption, in this case, becomes a derived inference rule.) We define a newdistributed subsumption inference rule, which has all the desirable properties: it allows subsumption, including subsumption of variants, in a distributed derivation, while preserving fairness and monotonicity. It also works in both sequential and distributed environments.
We conclude the paper with some discussion of the different behavior of subsumption in different architectures.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
Anantharaman, S. and Hsiang, J., Automated proofs of the Moufang identities in alternative rings,J. Automated Reasoning 6(1) (1990) 76–109.
Bachmair, L. and Ganzinger, H., Completion of first-order clauses with equality by strict superposition, in M. Okada and S. Kaplan (eds.),Proc. Second International Workshop on Conditional and Typed Term Rewriting Systems, Montreal, Canada, June 1990, Lecture Notes in Computer Science 516, Springer-Verlag, New York, 1991, pp. 162–180.
Bonacina, M. P., Distributed automated deduction, PhD thesis, Department of Computer Science, State University of New York at Stony Brook, December 1992.
Bonacina, M. P. and Hsiang, J., Distributed Deduction by Clause-Diffusion: The Aquarius Prover, in A. Miola (ed.),Proceedings of the Third International Symposium on Design and Implementation of Symbolic Computation Systems, Gmunden, Austria, September 1993, Lecture Notes in Computer Science 722, Springer-Verlag, New York, 1993, pp. 272–287.
Dershowitz, N. and Jouannaud, J.-P., Rewrite systems, Chapter 15, Volume B,Handbook of Theoretical Computer Science, North-Holland, Amsterdam, 1989.
Hsiang, J. and Rusinowitch, M., On word problems in equational theories, in Th. Ottman (ed.),Proceedings of the Fourteenth International Conference on Automata, Languages and Programming, Karlsruhe, Germany, July 1987, Lecture Notes in Computer Science 267, Springer-Verlag, New York, 1987, pp. 54–71.
Kapur, D. and Zhang, H., RRL: A rewrite rule laboratory, in E. Lusk and R. Overbeek (eds.),Proceedings of the Ninth International Conference on Automated Deduction, Argonne, Illinois, May 1988, Lecture Notes in Computer Science 310, Springer-Verlag, New York, 1988, pp. 768–770.
Kowalski, R., Studies in the completeness and efficiency of theorem proving by resolution, PhD thesis, University of Edinburgh, 1970.
Loveland, D. W.,Automated Theorem Proving: A Logical Basis, North-Holland, Amsterdam, 1978.
McCune, W. W., OTTER 2.0 Users Guide, Technical Report ANL-90/9, Argonne National Laboratory, Argonne, Illinois, March 1990.
Robinson, J. A., A machine-oriented logic based on the resolution principle,J. ACM 12 (1965) 23–41.
Rusinowitch, M., Theorem-proving with resolution and superposition,J. Symbolic Computation 11(1–2) (1991), 21–50.
Wos, L., Overbeek, R. and Lusk, E., Subsumption, a sometimes undervalued procedure, in J.-L. Lassez and G. Plotkin (eds.),Computational Logic, MIT Press, Cambridge, Mass., 1991, pp. 3–41.
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Bonacina, M.P., Hsiang, J. On subsumption in distributed derivations. J Autom Reasoning 12, 225–240 (1994). https://doi.org/10.1007/BF00881888
Received:
Issue Date:
DOI: https://doi.org/10.1007/BF00881888