I have a simple constraint system with a finite set $C$ of constant symbols, an infinite set $V$ of variables, and two relation symbols - $R_1$, a preorder, and $R_2$, an equivalence relation. Furthermore, $R_1$ and $R_2$ are related in the following way:$\forall x,y. R_1(x,y) \wedge R_1(y,x) \Rightarrow R_2(x,y)$The language of constraints ($\phi$) is as following:$x,y \in C \cup V$$\phi \in R_1(x,y) ~|~ R_2(x,y) ~|~ \phi \wedge \phi ~|~ true $I need to perform abduction in this constraint system. Specifically, for any given mutually consistent pair of constraints $\phi_{cx}$ and $\phi_{cs}$, I need to find a maximally weak (in an intuitive sense) constraint $\varphi$ such that $\phi_{cx} \wedge \varphi \Rightarrow \phi_{cs}$. I have following questions:Is my constraint system a Herbrand constraint system?Are the results on Simple Constraint Abduction problem described in [M. Maher, Herbrand Constraint Abduction, LICS'05] applicable to my case?
Abduction in a Herbrand Constraint System
lo.logic;type inference;logic programming