chibi@unraed: software / formlogic $
What is formlogic?
formlogic is a Python3 library which currently supports:
 parsing formulae of propositional logic
 calculating and representing truth tables
 constructing semantic tableaux (truth trees) for sets of propositional formulae
formlogic comes with two useful tools based on the library:

trtr.py
: takes formulae and draws their truth tree. 
ttcalc.py
: takes formulae and draws their truth tables.
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.
Command:
./ttcalc.py 'p > q'
Output:
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.
Command:
./ttcalc.py n 3 '(p / q) & !(p & q)'
Output:
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
Download
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 Unixlike 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
FormulaNode
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:

formula
: the string representing the formula to be parsed. 
prop_letters
: a string whose characters are to be parsed as propositional atoms, e.g."pqrstuvwxyz"
. 
unary
: a list of strings, which can be one character or longer, which are to be parsed as unary connectives. A unary connective is assumed to prefix the subformula on which it operates. 
binary
: a list of strings, which can be one character or longer, which are to be parsed as binary connectives. A binary connective is assumed to appear between the subformulae on which it operates.
Truth tables in formlogic
Initialising a TruthTable
There are two steps to making a fullyfledged 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:

formula
: the formula, represented as aFormulaNode
object, whose truth table is being constructed. 
num_values
: the number of truth values in the underlying propositional logic. In the typical case of binary logic, this number is 2.
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:
tt.evaluate(connectives)
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
keyvalue pair for conjunction is: "&": min
, using
Python's builtin 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
:
tt.get_value_by_dict(assig_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})
Manyvalued 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.