2
$\begingroup$

This is not my area, so apologizes if I am asking nonsense!

I know that there are very good solver/theorem provers for solving 1st order logic.

Now I have a problem, using 3-valued logic, but I am not sure if there are some practical ways of solving 3-valued logic (or converting it to a bigger 2-valued logic problem?)

EDIT1: Is it possible to translated (~reduce?) any 3-valued logic to 2-valued logic? Can this be generalized to K-valued logic, where K is any arbitrary integer? (What about the case when K is infinity?)

Any idea or reference is appreciated.

Improve this question
$\endgroup$
6
  • $\begingroup$ Isn't this a special case of CSP: en.wikipedia.org/wiki/Constraint_satisfaction_problem $\endgroup$
    – joro
    Aug 8, 2014 at 8:33
  • 3
    $\begingroup$ There is more than one system of 3-valued logic, but all of them have straightforward translations to 2-valued logic, replacing each atomic formula with a pair of formulas (that can be seen as implementing the original formula and its negation, in case the logic has Kleene negation). $\endgroup$
    – Emil Jeřábek
    Aug 8, 2014 at 10:25
  • 1
    $\begingroup$ @joro: 3-valued propositional logic is CSP. 3-valued first-order logic obviously isn't, as it is just as undecidable as in the 2-valued case. $\endgroup$
    – Emil Jeřábek
    Aug 8, 2014 at 10:29
  • $\begingroup$ @EmilJeřábek thanks for the explanation. Could you point me to some of the translations to the 2-valued logic? I updated the question with some relevant details. $\endgroup$
    – Daniel
    Aug 8, 2014 at 21:54
  • $\begingroup$ A finite-valued logic may be algorithmically translated into a 2-valued setting as soon as its language is sufficiently expressive (negation might help on that). Such expressiveness condition may be checked by way of a fixed-point construction, and failure in expressivity may be fixed by appropriate conservative extensions. The resulting 2-valued semantics is based on a generalized notion of compositionality, and is amenable to fully automated implementations. One detailed reference for the above is this paper. $\endgroup$
    – J Marcos
    Aug 11, 2014 at 22:20

1 Answer 1

Reset to default
5
$\begingroup$

Let's assume that your three-valued logic consists of the truth values Yes, No and "unknown". We can think of these truth values as the sets $\{\top\}, \{\bot\}, \{\top,\bot\}$, and then the logical operations result in all possible values. For example, Yes and Unknown is Unknown while No and Unknown is No.

A trick known as "double rail logic" uses two binary variables to represent each truth value: Yes is 1,1; No is 0,0; and Unknown is 1;0. The connectives And and Or are implemented using two matching gates, and Not by two negation gates followed by a swap.

More generally, $k$-valued logic can be implemented by encoding each truth value using $\lceil\log_2 k\rceil$ bits. The logical operations are implemented using constant-size Boolean circuits. The advantage of the encoding above is that the circuits are very simple, in particular they read each input only once.

Improve this answer
$\endgroup$
5
  • 1
    $\begingroup$ Interesting example. But in your example, I don't understand to the output corresponding to 0;1. How do we treat that case? $\endgroup$
    – Daniel
    Aug 9, 2014 at 5:33
  • $\begingroup$ Let me clarify. By this conversion, the resulting thing semi-decidable (right?), i.e. for any algorithm and given logical 3-valued logical statement, it can evaluate it for us, only when it is {T}, not the other two cases. How do you handle this? (i.e. how do you do resolution for this?) $\endgroup$
    – Daniel
    Aug 11, 2014 at 0:41
  • $\begingroup$ Basically how you formalize CWA suggested model? en.wikipedia.org/wiki/Closed_world_assumption $\endgroup$
    – Daniel
    Aug 11, 2014 at 5:56
  • $\begingroup$ We have embedded your three-valued logic into ordinary Boolean logic, do now you can use whatever algorithm you want that can handle Boolean logic. For example, there is an algorithm for the stable marriage problem which is based on three-valued logic. Using this conversion, you can implement it with Boolean variables. $\endgroup$
    – Yuval Filmus
    Aug 15, 2014 at 17:39
  • 1
    $\begingroup$ If you have other logic in mind, say one corresponding to CWA, you need to specify then first. I can't read your mind. Whatever the logic is, if it has reasonable semantics then the same encoding idea would work. $\endgroup$
    – Yuval Filmus
    Aug 15, 2014 at 17:43

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.

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