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?
