×

\(E\)-unification with constants vs. general \(E\)-unification. (English) Zbl 1260.03019

Summary: We present a solution to Problem #66 from the RTA open problem list. The question is whether there exists an equational theory \(E\) such that \(E\)-unification with constants is decidable but general \(E\)-unification is undecidable. The answer is positive and we show such a theory. The problem has several equivalent formulations, therefore the solution has many consequences. Our result also shows, that there exist two theories \(E _1\) and \(E _2\) over disjoint signatures such that \(E _1\)-unification with constants and \(E _2\)-unification with constants are decidable, but \((E _1 \cup E _2)\)-unification with constants is undecidable.

MSC:

03B35 Mechanization of proofs and logical operations
68Q42 Grammars and rewriting systems
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Baader, F., Büttner, W.: Unification in commutative idempotent monoids. Theor. Comput. Sci. 56, 345–353 (1988) · Zbl 0658.68108 · doi:10.1016/0304-3975(88)90140-5
[2] Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press (1999) · Zbl 0948.68098
[3] Baader, F., Schulz, K.: Unification in the union of disjoint equational theories: combining decision procedures. In: 11th CADE. LNCS, vol. 607. Springer, Saratoga Springs, NY (1992) · Zbl 0925.03084
[4] Baader, F., Schulz, K.U.: Unification in the union of disjoint equational theories: combining decision procedures. J. Symbol. Comput. 21, 211–243 (1996) · Zbl 0851.68055 · doi:10.1006/jsco.1996.0009
[5] Baader, F., Snyder, W.: Unification theory. In: Robinson, A., Voronkov, A. (eds.) A Chapter in Handbook of Automated Reasoning. Elsevier/MIT Press (2001) · Zbl 1011.68126
[6] Bürckert H.-J., Herold A., Schmidt-Schauss, M.: On equational theories, unification and decidability. In: Proc. of the 2nd RTA. LNCS, vol. 256, pp. 204-215. Springer-Verlag (1987)
[7] Hopcroft, J.E., Motwani, R., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation, 2nd edn. Addison-Wesley (2001) · Zbl 0980.68066
[8] Kapur, D., Narendran, P.: Double-exponential complexity of computing a complete set of AC-unifiers. In: LICS, Santa Cruz, CA (1992) · Zbl 0781.68076
[9] Narendran, P., Otto, F.: Single versus simultaneous equational unification and equational unification for variable-permuting theories. J. Autom. Reason. 19, 87–115 (1997) · Zbl 0882.68079 · doi:10.1023/A:1005764526878
[10] 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
[11] The RTA List of Open Problems: http://rtaloop.pps.jussieu.fr/ . Accessed 15 September 2008
[12] Schmidt-Schauss, M.: Unification in a combination of arbitrary disjoint equational theories. J. Symbol. Comput. 8(1/2), 51–99 (1989) · Zbl 0691.03003 · doi:10.1016/S0747-7171(89)80022-7
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.