A small program that generates truth tables from arguments in sentential logic.

truth_tables.py

#!/usr/bin/env python3
#
# Copyright (c) 2018 Christian Calderon
#
# Permission is hereby granted, free of charge, to any person obtaining a copy
# of this software and associated documentation files (the "Software"), to deal
# in the Software without restriction, including without limitation the rights
# to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
# copies of the Software, and to permit persons to whom the Software is
# furnished to do so, subject to the following conditions:
#
# The above copyright notice and this permission notice shall be included in all
# copies or substantial portions of the Software.
#
# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
# FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
# SOFTWARE.
import string
import sys
from typing import List
import argparse

BI = '↔'
IMP = '→'
WDG = '∨'
AMP = '&'
TURN = '⊢'
TILD = '~'
LPAREN = '('
RPAREN = ')'
VALID_LETTERS = set(string.ascii_uppercase)
VALID_BINOPS = set(BI+IMP+WDG+AMP)
VALID_CHARS = set('~()').union(VALID_LETTERS).union(VALID_BINOPS)
BINOP_TABLE = {
    BI: 'is',
    IMP: 'imp',
    AMP: 'and',
    WDG: 'or',
}


def parse(premise: str, verbose=False):
    """Parses a premise into a tree that can be turned into python code."""
    if verbose:
        print(premise)
    if not len(premise):
        raise ValueError('Empty premise not allowed')

    # start with base case
    if premise in VALID_LETTERS:
        return ('val', premise)

    # next case, find the main operator
    # check for tilde first, then binary operators

    if premise[0] == TILD:
        return ('not', parse(premise[1:], verbose))

    if premise[0] == LPAREN:
        missing_paren = 1
        i = 1
        max_i = len(premise)
        while i < max_i and missing_paren:
            char = premise[i]
            if char == LPAREN:
                missing_paren += 1
            elif char == RPAREN:
                missing_paren -= 1

            i += 1

        if missing_paren:
            #  mismatched parenthesis
            raise ValueError(f'Mismatched parenthesis: {premise}')

        if i == max_i:
            # just remove the parenthesis and keep parsing
            return parse(premise[1:-1], verbose)

        # in the final case, this is a binary operator
        # with parenthesis around the left hand side.
        # if not then error
        if i > max_i - 2:
            raise ValueError(
                f'Binary operator without right hand side: {premise}')

        # i should be the operator
        py_op = BINOP_TABLE.get(premise[i], None)

        if py_op is None:
            raise ValueError(f'Unknown binary operator: {premise}')

        return (py_op,
                parse(premise[1:i-1], verbose),
                parse(premise[i+1:], verbose))

    if premise[0] in VALID_LETTERS:
        # premise[1] must be the operator.
        # everything after is parsed recursively.
        if premise[1] not in VALID_BINOPS:
            raise ValueError(f'Unknown binary operator: {premise}')

        if len(premise) < 3:
            raise ValueError(f'Malformed premise: {premise}')

        py_op = BINOP_TABLE[premise[1]]

        return (py_op,
                ('val', premise[0]),
                parse(premise[2:], verbose))


def serialize(ptree):
    """Serializes a parsed premise into Python code."""

    if ptree[0] == 'val':
        return ptree[1]

    if ptree[0] == 'not':
        return '(not {})'.format(serialize(ptree[1]))

    if ptree[0] == 'imp':
        return 'imp({}, {})'.format(serialize(ptree[1]), serialize(ptree[2]))

    if ptree[0] in ('and', 'or', 'is'):
        return '({} {} {})'.format(serialize(ptree[1]), ptree[0], serialize(ptree[2]))

    raise ValueError(f'Invalid ptree: {ptree}')


def preproccess(argument):
    """Replaces common symbol synonyms with the ones expected by the parser."""
    replacements = (
        ('<->', BI),
        ('->', IMP),
        ('v', WDG),
        ('t', TURN),
        ('//', TURN),
        ('/', ','),
        (' ', '')
    )
    for substring, cannon in replacements:
        argument = argument.replace(substring, cannon)
    return argument


def truth_table(argument):
    """Makes the truth table for an argument in sentential logic."""
    argument = preproccess(argument).split(',')
    if TURN not in argument[-1]:
        raise ValueError('Missing conclusion: {}'.format(argument))
    else:
        start = argument[-1].find(TURN)
        argument[-1], conclusion = argument[-1][:start], argument[-1][start:]
        argument.append(conclusion)

    letters_used = list(VALID_LETTERS.intersection(''.join(argument)))
    letters_used.sort()
    L = len(letters_used)
    rows = [letters_used + argument]
    expressions = [serialize(parse(premise)) for premise in argument[:-1]]
    expressions.append(serialize(parse(argument[-1][1:])))

    # Function for logical implication
    def _imp(a, b):
        return b if a else True

    for i in range(2**len(letters_used)):
        letter_assignment = {}
        row = []
        for j, l in enumerate(letters_used):
            letter_assignment[l] = (i & (1 << (L - j - 1))) >> (L - j - 1)
            row.append('T' if letter_assignment[l] else 'F')

        for e in expressions:
            row.append('T' if eval(e, {'imp': _imp}, letter_assignment) else 'F')
        rows.append(row)

    return {'rows': rows,
            'atoms': letters_used,
            'size': (len(rows), len(rows[0]))}


def is_valid(truth_table):
    rows, size = truth_table['rows'], truth_table['size']
    len_atoms = len(truth_table['atoms'])
    for i in range(1, size[0]):
        if rows[i][-1] == 'F':
            if all(p=='T' for p in rows[i][len_atoms:-1]):
                return False

    return True


def pprint(truth_table):
    widths = map(len, truth_table['rows'][0])
    row_format = '|'.join('{{:^{}}}'.format(l+2) for l in widths)
    for row in truth_table['rows']:
        pretty_row = row_format.format(*row)
        print(pretty_row)
        print('-'*len(pretty_row))

    if is_valid(truth_table):
        print('Valid.')
    else:
        print('Invalid!')


def main() -> int:
    parser = argparse.ArgumentParser(
        description='Prints truth tables for a given argument and checks validity'
    )
    parser.add_argument('--demo',
                        action='store_true',
                        default=False,
                        help='Demonstrates how to use this'
    )
    parser.add_argument('--argument',
                        help='The argument you want to analyze.',
                        default=None)

    args = parser.parse_args()

    if not args.demo and args.argument is None:
        parser.print_usage()
        return 2
    elif args.demo and args.argument is None:
        argument = 'A->(BvC), C->(D&E), ~B tA->~E'
        print('Demo:')
        print(sys.argv[0], '--argument', repr(argument))
    elif args.argument:
        argument = args.argument

    pprint(truth_table(argument))
    return 0


if __name__ == '__main__':
    sys.exit(main())