Truth-Table-Generator

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.

Suported Logics

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

Dependancies

• python3
• lark-parser

Instructions

To install the lark-parser dependancy:

$ pip install lark-parser

To run the program:

$ python3 ttable.py

Syntax Reference

operator
~p	not p
p & q	p and q
p | q	p or q
p -> q	p implies q
p <-> q	p is equivalent to q
atom
p	any sequence of lowercase characters is a variable
1 or T	true
0 or F	false
I or U	unspecified for 3-valued logic
B	both true and false for 4 valued logic
N	neither true nor false for 4 valued logic
entailment
p |= q	p entails q in classic propositional logic (CPL)
p |=L q	p entails q in logic "L" (see above)
|= p	p is a tautology in classical propositional logic
|=L p	p is a tautology in logic "L" (see above)

Example

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