Let $C = m(P,X,Y) \leftarrow m(Q,X,Z), m(R,Z,Y)$. Is it possible to do the following substitution? $D = C\theta$ where $\theta = \{Q/R,R/Q\}$ s.t. $D = m(P,X,Y) \leftarrow m(R,X,Z),m(Q,Z,Y)$
FOL substitution - is it possible to substitute two variables with each other? e.g. $\theta=\{x/y,y/x\}$?
logic;first order logic;logic programming
Given the usual substitution function $[x/y]$ s.t. $M[x/y]$ is the result of substituting all free occurrences of '$y$' with '$x$' in $M$,your desired function can be defined as follows:$M [x//y] =_{df} M[x'/y][y/x][x/x']$ provided $x'$ doesn't occur in $M$.Example. Let $C = m(P,X,Y)m(Q,X,Z),m(R,Z,Y)$. Then:\begin{align*}D &= C~[Q~//~R]\\&= [m(P,X,Y)m(Q,X,Z),m(R,Z,Y)][Q'/R][R/Q][Q/Q'] \\&= [m(P,X,Y)m(Q,X,Z),m(Q',Z,Y)][R/Q][Q/Q']\\&= [m(P,X,Y)m(R,X,Z),m(Q',Z,Y)][Q/Q']\\&= m(P,X,Y)m(R,X,Z),m(Q,Z,Y)\end{align*}