×

Order-sorted rewriting and congruence closure. (English) Zbl 1475.68142

Jacobs, Bart (ed.) et al., Foundations of software science and computation structures. 19th international conference, FOSSACS 2016, held as part of the European joint conferences on theory and practice of software, ETAPS 2016, Eindhoven, The Netherlands, April 2–8, 2016. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 9634, 493-509 (2016).
Summary: Order-sorted type systems supporting inheritance hierarchies and subtype polymorphism are used in theorem proving, AI, and declarative programming. The satisfiability problems for the theories of: (i) order-sorted uninterpreted function symbols, and (ii) of such symbols modulo a subset \(\varDelta\) of associative-commutative ones are reduced to the unsorted versions of such problems at no extra computational cost. New results on order-sorted rewriting are needed to achieve this reduction.
For the entire collection see [Zbl 1333.68011].

MSC:

68Q42 Grammars and rewriting systems

Software:

CafeOBJ; Maude
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Ackermann, W.: Solvable Cases of the Decision Problem. North-Holland Publishing Company, Amsterdam (1954) · Zbl 0056.24505
[2] Bachmair, L., Tiwari, A., Vigneron, L.: Abstract congruence closure. J. Autom. Reasoning 31(2), 129–168 (2003) · Zbl 1040.03006 · doi:10.1023/B:JARS.0000009518.26415.49
[3] Bouhoula, A., Jouannaud, J.P., Meseguer, J.: Specification and proof in membership equational logic. Theoret. Comput. Sci. 236, 35–132 (2000) · Zbl 0938.68057 · doi:10.1016/S0304-3975(99)00206-6
[4] Clavel, M., Durán, F., Eker, S., Meseguer, J., Lincoln, P., Martí-Oliet, N., Talcott, C.: All About Maude. LNCS, vol. 4350. Springer, Heidelberg (2007) · Zbl 1115.68046
[5] Conchon, S., Contejean, E., Iguernelala, M.: Canonized rewriting and ground AC completion modulo Shostak theories : design and implementation. Logical Methods Comput. Sci. 8(3), 1–29 (2012) · Zbl 1253.68291 · doi:10.2168/LMCS-8(3:16)2012
[6] Dershowitz, N., Jouannaud, J.P.: Rewrite systems. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B, pp. 243–320. North-Holland Publishing Company, Amsterdam (1990) · Zbl 0900.68283
[7] Downey, P.J., Sethi, R., Tarjan, R.E.: Variations on the common subexpressions problem. J. ACM 27(4), 758–771 (1980) · Zbl 0458.68026 · doi:10.1145/322217.322228
[8] Frisch, A.M.: The substitutional framework for sorted deduction: fundamental results on hybrid reasoning. Artif. Intell. 49(1–3), 161–198 (1991) · Zbl 0736.68071 · doi:10.1016/0004-3702(91)90009-9
[9] Futatsugi, K., Diaconescu, R.: CafeOBJ Report. World Scientific, Singapore (1998) · Zbl 0962.68115
[10] Futatsugi, K., Goguen, J., Jouannaud, J.P., Meseguer, J.: Principles of OBJ2. In: Proceedings of POPL 1985, pp. 52–66. ACM (1985) · doi:10.1145/318593.318610
[11] Gallier, J., Isakowitz, T.: Order-sorted congruence closure. Technical report CIS-686, UPenn (1988). http://repository.upenn.edu/cis_reports/686
[12] Gallier, J.H., Narendran, P., Plaisted, D.A., Raatz, S., Snyder, W.: An algorithm for finding canonical sets of ground rewrite rules in polynomial time. J. ACM 40(1), 1–16 (1993) · Zbl 0779.68050 · doi:10.1145/138027.138032
[13] Gnaedig, I., Kirchner, C., Kirchner, H.: Equational completion in order-sorted algebras. Theoret. Comput. Sci. 72(2–3), 169–202 (1990) · Zbl 0698.68028 · doi:10.1016/0304-3975(90)90034-F
[14] Goguen, J., Jouannaud, J.P., Meseguer, J.: Operational semantics of order-sorted algebra. In: Brauer, W. (ed.) Automata, Languages and Programming. LNCS, vol. 194, pp. 221–231. Springer, Heidelberg (1985) · Zbl 0591.68041 · doi:10.1007/BFb0015747
[15] Goguen, J., Meseguer, J.: Order-sorted algebra I. Theoret. Comput. Sci. 105, 217–273 (1992) · Zbl 0778.68056 · doi:10.1016/0304-3975(92)90302-V
[16] Kapur, D.: Shostak’s congruence closure as completion. In: Comon, H. (ed.) RTA 1997. LNCS, vol. 1232, pp. 23–37. Springer, Heidelberg (1997) · Zbl 1379.68196 · doi:10.1007/3-540-62950-5_59
[17] Kirchner, C., Kirchner, H., Meseguer, J.: Operational semantics of OBJ3. In: Lepistö, T., Salomaa, A. (eds.) Automata, Languages and Programming. LNCS, vol. 317, pp. 287–301. Springer, Heidelberg (1988) · Zbl 0649.68028 · doi:10.1007/3-540-19488-6_123
[18] Knuth, D., Bendix, P.: Simple word problems in universal algebra. In: Leech, J. (ed.) Computational Problems in Abstract Algebra. Pergamon Press, Oxford (1970) · Zbl 0188.04902
[19] Marché, C.: On ground AC-completion. In: Book, R.V. (ed.) RTA 1991. LNCS, vol. 488, pp. 411–422. Springer, Heidelberg (1991) · doi:10.1007/3-540-53904-2_114
[20] Meseguer, J.: Order-sorted rewriting and congruence closure. Technical report, C.S. Department, University of Illinois at Urbana-Champaign, June 2015. http://hdl.handle.net/2142/78008 · Zbl 1475.68142
[21] Meseguer, J.: Membership algebra as a logical framework for equational specification. In: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol. 1376, pp. 18–61. Springer, Heidelberg (1998) · Zbl 0903.08009 · doi:10.1007/3-540-64299-4_26
[22] Narendran, P., Rusinowitch, M.: Any ground associative-commutative theory has a finite canonical system. In: Book, R.V. (ed.) RTA 1991. LNCS, vol. 488, pp. 423–434. Springer, Heidelberg (1991) · Zbl 0878.68076 · doi:10.1007/3-540-53904-2_115
[23] Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst. 1(2), 245–257 (1979) · Zbl 0452.68013 · doi:10.1145/357073.357079
[24] Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. J. ACM 27(2), 356–364 (1980) · Zbl 0441.68111 · doi:10.1145/322186.322198
[25] Oppen, D.C.: Complexity, convexity and combinations of theories. Theoret. Comput. Sci. 12, 291–302 (1980) · Zbl 0437.03007 · doi:10.1016/0304-3975(80)90059-6
[26] Schmidt-Schauss, M.: Computational Aspects of Order-Sorted Logic with Term Declarations. LNCS (LNAI), vol. 395. Springer, Heidelberg (1989) · Zbl 0689.68001 · doi:10.1007/BFb0024065
[27] Shostak, R.E.: An algorithm for reasoning about equality. Commun. ACM 21(7), 583–585 (1978) · Zbl 0378.68044 · doi:10.1145/359545.359570
[28] Shostak, R.E.: Deciding combinations of theories. J. ACM 31(1), 1–12 (1984) · Zbl 0629.68089 · doi:10.1145/2422.322411
[29] Smolka, G., Aït-Kaci, H.: Inheritance hierarchies: semantics and unification. J. Symb. Comput. 7(3/4), 343–370 (1989) · Zbl 0678.68009 · doi:10.1016/S0747-7171(89)80016-1
[30] Tinelli, C., Zarba, C.G.: Combining decision procedures for sorted theories. In: Alferes, J.J., Leite, J. (eds.) JELIA 2004. LNCS (LNAI), vol. 3229, pp. 641–653. Springer, Heidelberg (2004) · Zbl 1111.68691 · doi:10.1007/978-3-540-30227-8_53
[31] Tiwari, A.: Combining equational reasoning. In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS, vol. 5749, pp. 68–83. Springer, Heidelberg (2009) · Zbl 1193.68239 · doi:10.1007/978-3-642-04222-5_4
[32] Walther, C.: A mechanical solution of Schubert’s steamroller by many-sorted resolution. Artif. Intell. 26(2), 217–224 (1985) · Zbl 0569.68076 · doi:10.1016/0004-3702(85)90029-3
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.