# Three-valued logic solver?

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.

• Isn't this a special case of CSP: en.wikipedia.org/wiki/Constraint_satisfaction_problem
– joro
Aug 8 '14 at 8:33
• 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). Aug 8 '14 at 10:25
• @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. Aug 8 '14 at 10:29
• @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. Aug 8 '14 at 21:54
• 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. Aug 11 '14 at 22:20

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.
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.