Abstract
We consider reasoning and rewriting with set-relations: inclusion, non-empty intersection and singleton identity, each of which satisfies only two among the three properties of the equivalence relations. The paper presents a complete inference system which is a generalization of ordered paramodulation and superposition calculi. Notions of rewriting proof and confluent rule system are defined for such non-equivalence relations. Together with the notions of forcing and redundancy they are applied in the completeness proof. Ground completeness cannot be lifted to the non-ground case because substitution for variables is restricted to deterministic terms. To overcome the problems of restricted substitutivity and hidden (in relations) existential quantification, unification is defined as a three step process: substitution of determistic terms, introduction of bindings and “on-line” skolemisation. The inference rules based on this unification derive non-ground clauses even from the ground ones, thus making an application of a standard lifting lemma impossible. The completness theorem is proved directly without use of such a lemma.
Both authors gratefully acknowledge the financial support received from the Norwegian Research Council.
Preview
Unable to display preview. Download preview PDF.
References
M. Bezem. Completeness of Resolution Revisited. Theoretical Computer Science, 74, pp.27–237, (1990).
L. Bachmair, H. Ganzinger. Rewrite-Based Equational Theorem Proving with Selection and Simplification. Journal of Logic and Computation, 4(3), pp. 217–247 (1994).
L. Bachmair, H. Ganzinger. Rewrite Techniques for Transitive Relations. Proc. 9th IEEE Symposium on Logic in Computer Science, pp. 384–393. IEE Computer Society Press (1994).
L. Bachmair, H. Ganzinger. Ordered Chaining Calculi for First-Order Theories of Binary Relations. Technical Report MPI-I-95-2-009, Max-Planck-Institut f. Informatik, Saarbrücken, (1995).
L. Bachmair, H. Ganzinger, C. Lynch, W. Snyder. Basic paramodulation. Information and Computation, 121(2), pp. 172–192 (1995).
R. Berghammer, T. Gritzner, G. Schmidt. Prototyping relational specifications using higher-order objects. In Proc. Int. Workshop on Higher Order Algebra, Logic and Term Rewriting (HOA '93), Amsterdam, The Netherlands, Sept. 1993, LNCS, vol. 816, pp. 56–75 (1994).
M. Białasik, B. Konikowska, Reasoning with Nondeterministic Specifications, ICS PAS Report no. 793, Institute of Computer Science, Polish Academy of Sciences, (1995).
N. Dershowitz, J.-P. Jouannaud. Rewrite systems. In: J. van Leeuwen (ed.) Handbook of theoretical computer science, vol. B, chap. 6, pp.243–320. Amsterdam: Elsevier, (1990).
N. Dershowitz, Z. Manna. Proving termination with multiset orderings. Communications of the ACM, 22:8,pp.465–476, (1979).
A. Dovier, E. Omodeo, E. Pontelli, G.-F. Rossi. Embedding finite sets in a logic programming language. LNAI, vol. 660, pp.150–167, (1993).
W.H. Hesselink. A Mathematical Approach to Nondeterminism in Data Types. ACM Trans. on Programming Languages and Systems, 10, pp.87–117, (1988).
H. Hussmann. Nondeterministic algebraic specifications and nonconfluent term rewriting. Journal of Logic Programming, 12, pp.237–235, (1992).
H. Hussmann. Nondeterminism in Algebraic Specifications and Algebraic Programs. Birkhäuser Boston, (1993).
B. Jayaraman. Implementation of Subset-Equational Programs. Journal of Logic Programming, 12:4, pp.299–324, (1992).
S. Kaplan. Rewriting with a Nondeterministic Choice Operator. Theoretical Computer Science, 56:1, pp.37–57, (1988).
V. Kriaučiukas, S. Meldal, M. Walicki. Nondeterministic Algebraic Specifications in Relational Syntax, in Proc. of 7th Nordic Workshop on Programming Theory, Report No. 86, Programming Methodology Group, Göteborg University, (1995).
V. Kriaučiukas, M. Walicki. Reasoning and Rewriting with Set-Relations I: Ground-Completeness. In Proceedings of CSL'94, LNCS, vol. 933, pp. 264–278, (1995).
J. Levy, J. Agustí. Bi-rewriting, a term rewriting technique for monotonic order relations. In RTA'93, LNCS, vol. 690, pp.17–31, (1993).
P.D. Mosses. Unified algebras and institutions. In LICS'89, Proc. 4th Ann. Symp. on Logic in Computer Science, pp. 304–312, IEEE, (1989).
W. Snyder, C. Lynch. Goal directed strategies for paramodulation. In Proc. 4th Int. Conf, on Rewriting Techniques and Applications, LNCS, vol. 488, pp. 150–161, Berlin, (1991).
J. Pais, G.E. Peterson. Using Forcing to Prove Completeness of Resolution and Paramodulation. Journal of Symbolic Computation, 11:(1/2), pp.3–19, (1991).
J. Schwartz, R. Dewar, E. Schonberg, E. Dubinsky. Programming with sets, an introduction to SETL. Springer Verlag, New York, (1986).
M. Walicki. Algebraic Specifications of Nondeterminism. Ph.D. thesis, Institute of Informatics, University of Bergen, (1993).
M. Walicki, S. Meldal. Multialgebras, Power algebras and Complete Calculi of Identities and Inclusions. In Recent Trends in Data Type Specification, LNCS, vol. 906, pp. 453–468 (1995).
M. Walicki, S. Meldal. A Complete Calculus for Multialgebraic and Functional Semantics of Nondeterminism. ACM Trans. on Programming Languages and Systems, vol. 17, No. 2, pp. 366–393 (1995).
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kriaučiukas, V., Walicki, M. (1996). Rewriting and reasoning with set-relations II: The non-ground case completeness. In: Haveraaen, M., Owe, O., Dahl, OJ. (eds) Recent Trends in Data Type Specification. ADT COMPASS 1995 1995. Lecture Notes in Computer Science, vol 1130. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61629-2_50
Download citation
DOI: https://doi.org/10.1007/3-540-61629-2_50
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61629-0
Online ISBN: 978-3-540-70642-7
eBook Packages: Springer Book Archive