This is a very simple truth-table generator for 3 and 4-valued logics that I made for solving homework one evening when I was bored. It also can be used to check entailments, as long as your formula doesn't have too many variables.

It uses lark-parser to parse the input formulas, which was very quick and easy to set up. After parsing the formula, the program will iterate over all possible assignments to the variables in the formula and recursively find the truth values of all connectives, and the entailment.

1. CPL - Classical propositional logic, the boolean logic we all know and love.
2. K3 - Kleen's 3-valued logic
3. B3 - Bochvar's internal 3-valued logic
4. LP - Priest's logic of paradox
5. L3 - Łukasiewicz's 3-valued logic
6. RM3 - R-mingle 3-valued logic
7. FDE - Belnap 4-valued logic, first degree entailment

• python3
• lark-parser

To install the lark-parser dependancy:

$ pip install lark-parser

To run the program:

$ python3 ttable.py

Checks if the entailment ¬p ∨ q ⊨ p → q holds in K3.

> ~p | q |=K3 p -> q

  (~p | q) |=K3 (p -> q)
..........................
   10 1 0   1    0 1  0
   10 1 i   1    0 1  i
   10 1 1   1    0 1  1
   ii i 0   1    i i  0
   ii i i   1    i i  i
   ii 1 1   1    i 1  1
   01 0 0   1    1 0  0
   01 i i   1    1 i  i
   01 1 1   1    1 1  1

entailment always holds