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

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

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

CC BY-SA 3.0
2014-08-09T05:33:13.773Z
Interesting example. But in your example, I don't understand to the output corresponding to 0;1. How do we treat that case?
Daniel
CC BY-SA 3.0
2014-08-11T00:41:17.287Z
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?)
Daniel
CC BY-SA 3.0
2014-08-11T05:56:41.870Z
Basically how you formalize CWA suggested model? 
https://en.wikipedia.org/wiki/Closed_world_assumption
Daniel
CC BY-SA 3.0
2014-08-15T17:39:25.103Z
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.
Yuval Filmus
CC BY-SA 3.0
2014-08-15T17:43:16.567Z
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.
Yuval Filmus
CC BY-SA 3.0
2014-08-09T00:50:26.700Z
2014-08-09T00:50:26.700Z
Yuval Filmus
<p>This is not my area, so apologizes if I am asking nonsense! </p>

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

<p>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?)</p>

<p>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?)</p>

<p>Any idea or reference is appreciated. </p>

CC BY-SA 3.0
2014-08-08T08:33:39.560Z
Isn't this a special case of CSP: https://en.wikipedia.org/wiki/Constraint_satisfaction_problem
joro
CC BY-SA 3.0
2014-08-08T10:25:24.780Z
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).
Emil Jeřábek
CC BY-SA 3.0
2014-08-08T10:29:23.667Z
@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.
Emil Jeřábek
CC BY-SA 3.0
2014-08-08T21:54:36.003Z
@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.
Daniel
CC BY-SA 3.0
2014-08-11T22:20:42.627Z
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](https://dl.dropboxusercontent.com/u/9291912/papers/13-CMV-gencomp.pdf) paper.
J Marcos
CC BY-SA 3.0
2017-02-16T22:07:50.790Z
http://www.cse.chalmers.se/~danr/papers/intuit.pdf is a cool approach to using CEGAR (repeated calls of a SAT solver) for intuitionistic propositional logic, and something similar might be useful if you're looking for a practical approach
fread2281
<lo.logic><logic-programming>
Three-valued logic solver?
Daniel
# Three-valued logic solver?

(Asked by: username_0 on 2014-08-08)

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.

**Tags:** lo.logic, logic-programming
> **Comments:**
> **username_1**: Isn't this a special case of CSP: https://en.wikipedia.org/wiki/Constraint_satisfaction_problem  
> **username_2**: 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).  
> **username_2**: @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.  
> **username_0**: @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.  
> **username_3**: 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](https://dl.dropboxusercontent.com/u/9291912/papers/13-CMV-gencomp.pdf) paper.  
> **username_4**: http://www.cse.chalmers.se/~danr/papers/intuit.pdf is a cool approach to using CEGAR (repeated calls of a SAT solver) for intuitionistic propositional logic, and something similar might be useful if you're looking for a practical approach  

---

## 1 answers

### Answer by username_5 on 2014-08-09. Score: 5

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.

> **Comments:**
> **username_0**: Interesting example. But in your example, I don't understand to the output corresponding to 0;1. How do we treat that case?  
> **username_0**: 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?)  
> **username_0**: Basically how you formalize CWA suggested model?  https://en.wikipedia.org/wiki/Closed_world_assumption  
> **username_5**: 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.  
> **username_5**: 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.  

---

