chibi@unraed: software / formlogic $

What is formlogic?

formlogic is a Python3 library which currently supports:

formlogic comes with two useful tools based on the library:

Example: ttcalc

If you follow the download instructions below, you can start to see the capabilities of formlogic by playing around with the tools built on it.

By default, conjunction is represented by & (ampersand), disjunction by / (forward slash), implication by > (greater than) and negation by ! (exclamation mark). Start by calculating some familiar truth tables.


./ttcalc.py 'p > q'


p q | (p>q)
0 0 | 1
0 1 | 1
1 0 | 0
1 1 | 1

formlogic supports any finite number of truth values in truth tables. The number of truth values is specified via the -n option.


./ttcalc.py -n 3 '(p / q) & !(p & q)'


p q | ((p/q)&!(p&q))
0 0 | 0
0 1 | 1
0 2 | 2
1 0 | 1
1 1 | 1
1 2 | 1
2 0 | 2
2 1 | 1
2 2 | 0


Copy the source code into a directory called formlogic:

git clone http://unraed.uk/repos/formlogic.git formlogic

If you want to use the library, all the code will now be within the directory formlogic/formlogic/.

If you want to run the tools mentioned above, it is helpful to make them executable first. On Unix-like systems, this can be done by running the following commands in the terminal:

cd formlogic
chmod +x trtr.py
chmod +x ttcalc.py

Formulae in formlogic


Formulae in formlogic can be stored as FormulaNode objects. A FormulaNode is essentially a node on a binary tree. If a node has children, it is a connective, and the subtree or subtrees under it are the formula or formulae on which the connective operates. If a node does not have any children, it is a propositional atom.

Parsing formulae

parse_prop_formula(formula, prop_letters, unary, binary)

The function parse_prop_formula parses strings which represent propositional formulae and (if no errors are encountered) returns a FormulaNode object.

Its arguments are:

Truth tables in formlogic

Initialising a TruthTable

There are two steps to making a fully-fledged truth table in formlogic. The first is to make an instance of the class TruthTable:

tt = TruthTable(formula, num_values)

The two required arguments are:

Evaluating a TruthTable

After creating a TruthTable, it is blank in the sense that none of its rows has a value. To fill up the table, call the method evaluate on the table:


The single required argument, connectives, must be a dictionary. The keys of the dictionaries are strings which represent the unary and binary connectives present in the TruthTable's formula. The values of the dictionaries are functions. The function takes one argument if the connective it defines is unary, and two arguments if the connective it defines is binary. The function must return, for each possible set of truth values given to it, the truth value of the connective operating on those values.

This is less difficult than it sounds. For example, if conjunction is symbolised as &, the key-value pair for conjunction is: "&": min, using Python's built-in function for getting the lesser of two integers. This works because when truth values are numbers, the conjunction of two values is equivalent to the lesser of the pair.

Accessing information in a TruthTable

When the two steps above have been performed, your truth table is ready to go. The safest way to retrieve the value of the table for a specific assignment to its propositional atoms is get_value_by_dict:


assig_dict is a dictionary which represents an assignment of truth values to the propositional atoms in tt's formula. Each key is a propositional atom (as a string) appearing in tt's formula. Each key's value is the truth value which is assigned to the atom in question.

For example:

tt.get_value_by_dict({"p": 0, "q": 1})

Many-valued logics

formlogic is able to handle (and construct) truth tables with any finite number of truth values.

If there are n truth values, they are represented in formlogic as the integers 0, 1, ..., n - 1. In binary logic, this results in the familiar 0 (falsity) and 1 (truth). However, in logics with more truth values, 1 will represent an intermediate truth value, rather than 'truth'. Instead, n - 1 is normally taken to represent 'truth', i.e. what 1 represents in binary logic.