# Abduction in a Herbrand Constraint System

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:

1. Is my constraint system a Herbrand constraint system?
2. Are the results on Simple Constraint Abduction problem described in [M. Maher, Herbrand Constraint Abduction, LICS'05] applicable to my case?