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?


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.