Término reescritura; Calcular pares críticos

Intenté resolver el siguiente ejercicio, pero me quedé estancado mientras trataba de encontrar todos los pares críticos .

Tengo las siguientes preguntas:

1. ¿Cómo sé qué par crítico produjo una nueva regla?
2. ¿Cómo sé que encontré todos los pares críticos?

Deje $\Sigma= \left \{ \circ, i, e \right \}$ donde $\circ$ es binario, $i$ es unario y $e$ es una constante.

$$E=\left \{ \begin{gather} ( x \circ y ) \circ z \approx x \circ\left ( y \circ z \right ) \\ x \circ e \approx x \\ x \circ i(x) \approx e \end{gather} \right\}$$

Mi trabajo hasta ahora:

1. $x\circ e >_{\textsf{lpo}} x$   (LPO 1)   $x$ es una variable
   
   $x\circ i(x)>_{\textsf{lpo}} e$   (LPO 2b) no hay términos en el lado derecho
   
   $(x\circ y)\circ z\approx x\circ(y\circ z)$
   
   $s=\circ(\underset{\large s_1}{\circ(x,y)},\underset{\large s_2}{\strut z})\qquad t=\circ (\underset{\large t_1}{x\strut}, \underset{\large t_2}{\circ(y,z)})$     (LPO 2c)
   
   

   • compruebe que $s>t_j$ , $j=\overline{1,m}$
     
     $s>_{\textsf{lpo}}t_1$     (LPO 1)
     
     para demostrar que $s>_{\textsf{lpo}}t_2$ (LPO 2c) probamos que $$s>_{\textsf{lpo}} y \;\;\text{(LPO 1)};\qquad s>_{\textsf{lpo}}z \;\;\text{(LPO 1)};\qquad \circ(x,y)>y\;\;\text{(LPO 1)}$$
   • encuentre tal que s i > lpo t i i = 1 ∘ ( x , y ) > lpo$i$$s_i>_{\textsf{lpo}}t_i$     $i=1$ $$\circ(x,y)>_{\textsf{lpo}}x\;\;\text{(LPO 1)}$$

   $(x\circ y)\circ z>_{\textsf{lpo}} x\circ (y\circ z)$
   
   

2. a. x 1 ∘ $(x\circ y)\circ z\;\rightarrow\; x\circ (y\circ z)$
   
   x ∘ $x_1\circ e\;\rightarrow\; x_1$
   
   θ { $x\circ y \mathrel{\,=?\,} x_1\circ e$
   
   ( x 1 ∘ e ) ∘ $\theta\{x \;\leftarrow \;x_1;\; y\;\leftarrow \;e\}$ si. ( x ∘ y ) ∘

   $$\require{AMScd} \require{cancel} \begin{CD} (x_1\circ e)\circ z @>>> \cancel{x_1}\circ z\\ @VVV @VVV\\ \cancel{x_1}\circ(e\circ z) @>>> e\circ z\approx z \end{CD}\qquad\text{left identity?}$$
   e ∘ x $(x\circ y)\circ z\;\rightarrow\; x\circ (y\circ z)$
   
   x ∘ $e\circ x_1\;\rightarrow\; x_1$
   
   θ { $x\circ y \mathrel{\,=?\,} e\circ x_1$
   
   ( e ∘ x 1 ) ∘ $\theta\{x \;\leftarrow \;e;\; y\;\leftarrow \;x_1\}$ C. (x∘y)∘ $$\begin{CD} (e\circ x_1)\circ z @>>> x_1\circ z\\ @VVV @VVV\\ e\circ(x_1\circ z) @>>> ? \end{CD}$$
   x 1 ∘ i ( x 1$(x\circ y)\circ z\;\rightarrow\; x\circ (y\circ z)$
   
   x ∘ $x_1\circ i(x_1)\;\rightarrow\; e$
   
   $x\circ y \mathrel{\,=?\,} x_1\circ i(x_1)$
   
   $\theta\{x \;\leftarrow \;x_1;\; y\;\leftarrow \;i(x_1)\}$ $$\begin{CD} (x_1\circ i(x_1))\circ z @>>> e\circ z\\ @VVV @VVV\\ x_1\circ(i(x_1)\circ z) @>>> ? \end{CD}$$
   

Como documento de soporte tengo "Reescritura de términos y todo eso" de Franz Baader y Tobias Nipkow.

( imagen original aquí )

EDITAR1

Después de buscar los pares críticos, tengo el siguiente conjunto de reglas (suponiendo que 2.a es corect):

$$E=\left \{ \begin{gather} ( x \circ y ) \circ z \approx x \circ\left ( y \circ z \right ) \\ x \circ e \approx x \\ x \circ i(x) \approx e \\ x \circ (i(x) \circ y) \approx y \\ x \circ ( y \circ i(x \circ y) ) \approx e \\ e \circ x \approx x \\ e \circ (x \circ y) \approx x \circ y \end{gather} \right\}$$

$x\circ(e\circ z) \approx x\circ z$$0*x \approx 0*y$$x\approx y$(lo que significaría que solo tiene un modelo trivial). Ningún procedimiento de reescritura de sonido, incluido el de Huet, debería permitir esta reducción.

$x\circ e$$x\circ i(x)$$(x\circ y)\circ z$$\circ$

• $x\circ(y\circ e)\leftarrow (x\circ y)\circ e\to x\circ y$$x\circ y\approx x\circ y$
• $x\circ(y\circ i(x\circ y))\leftarrow(x\circ y)\circ i(x\circ y)\to e$$x\circ(y\circ i(x\circ y))\to e$$\circ\triangleright e$$\triangleright$$x\circ i(x)\approx e$

Para el procedimiento básico de finalización:

1. $x\circ(i(x)\circ z)\to e\circ z$$(x\circ y)\circ z$$x_1\circ y_1$$(x\circ y)\circ(z\circ z_1)\leftarrow((x\circ y)\circ z)\circ z_1\to(x\circ(y\circ z))\circ z_1$$x\circ(y\circ(z\circ z_1))\approx x\circ(y\circ(z\circ z_1))$
2. $l\to r$$l_1\to r_1,\dots,l_n\to r_n$$l$$l_i$$l$

Este procedimiento se puede mejorar bastante. En particular, puede usar nuevas reglas para simplificar las viejas (y posiblemente descartarlas si se vuelven triviales, lo que significa que están incluidas en la nueva regla), y una buena heurística para elegir el próximo par crítico para examinar puede reducir drásticamente cantidad de reglas