0
$\begingroup$

I'm trying to model an undirected edge in a graph. If we have an edge $(a \to b)$ given in a database, the edge $(b \to a)$ is of course implied.

Given the predicate Has_Connection(a, b). It indicates nodes a and b having a connection.

I now want to make a new predicate (eg Has_Sym_Connection(a, b)) that defines that if we have a database with Has_Connection(a, b) in it, Has_Sym_Connection(b, a) is also true.

So far I tried the following:

Has_Symm_Connection(a, b) => Has_Connection(a, b) || Has_Connection(b, a)
Has_Symm_Connection(a, b) <=> Has_Connection(a, b) || Has_Connection(b, a)
Has_Symm_Connection(a, b) <= Has_Connection(a, b) || Has_Connection(b, a)

None of them seem to do the trick. Can someone point me towards the right direction?

An example of where it goes wrong. (Example is Linear Time Calculus)

Has_Connection = {(a, b), (b, c), (c, a)}; (A structure with initial values.)

What I'm modelling in the following is that, an entity its position changes when it moves to a connected node.

This works, but only in one direction, as specified in the structure above:

$\forall$ t, loc: C_Location(t, loc1) $\leftarrow$ Move_To(t, loc1) & $\exists$ loc2 : Location(t) = loc2 & (Has_Connection(loc2, loc).

This however, leads to an unsatisfiable problem with any of the above rules:

$\forall$ t, loc: C_Location(t, loc1) $\leftarrow$ Move_To(t, loc1) & $\exists$ loc2 : Location(t) = loc2 & Has_Symm_Connection(loc, loc2).

$\endgroup$
  • 1
    $\begingroup$ The middle one seems fine. $\endgroup$ – André Nicolas Nov 9 '15 at 23:05
  • $\begingroup$ @AndréNicolas Thanks for the answer, the problem I stumble upon is that it makes my model unsatisfiable when I try using the middle Has_Symm_Connection predicate. (Any of them actually). In my current model I simply use Has_Connection(a, b) to indicate I want a connection, if change this to (Has_Connection(a, b) || Has_Connection(b, a)) the unsat arises. Which is quite odd, as it I don't see why an OR would have that kind of influence.. $\endgroup$ – drx Nov 9 '15 at 23:11
  • $\begingroup$ What language are you using? Doesn't || denote 'or' rather than 'and' (&&). You want 'and' there . If it were 'or' the right hand side would be true when just a one-way connection existed. $\endgroup$ – Graham Kemp Nov 9 '15 at 23:18
  • $\begingroup$ Can you give an example of when it becomes unsatisfiable? The middle one looks fine to me. $\endgroup$ – Alt Nov 9 '15 at 23:20
1
$\begingroup$

Checking: $|\,|$ is the boolean 'or' in your programming language, whereas $\&\&$ is the Boolean 'and', correct?

$\begin{array}{c:c|c|c}\tiny\textsf{Has_Connection}(a,b) & \tiny\textsf{Has_Connection}(b, a) & \tiny\textsf{Has_Connection}(a,b)\,|\,|\,\textsf{Has_Connection}(b,a) & \tiny\textsf{Has_Sym_Connection}(a,b) & \tiny\textsf{Has_Connection}(a,b)\&\&\textsf{Has_Connection}(b,a) \\ \hline \color{blue}{T} & \color{blue}{T} & \color{blue}{T} & \color{blue}{T} & \color{blue}{T} \\ \color{blue}{T} & \color{red}{F} & \color{blue}{T} & \color{red}{F} & \color{red}{F} \\ \color{red}{F} & \color{blue}{T} & \color{blue}{T} & \color{red}{F} & \color{red}{F} \\ \color{red}{F} & \color{red}{F} & \color{red}{F} & \color{red}{F} & \color{red}{F} \end{array}$

So $\textsf{Has_Sym_Connection}(a,b) \implies \textsf{Has_Connection}(a,b)\,|\,|\,\textsf{Has_Connection}(b,a)$ is always satisfiable, but the other cases can be unsatisfied.

  • $\implies$ requires the consequent to be true whenever the antecedent is.
  • $\impliedby$ requires the antecedent to be true whenever the consequent is.
  • $\iff$ requires both the antecedent and consequent to be true whenever either is.
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.