Tableaux¶

Base Classes¶

class logics.classes.propositional.proof_theories.TableauxNode(content, index=None, justification=None, parent=None, children=None)¶

Class for a tableaux node.

Subclasses NodeMixin from the anytree package. Since a node can have children, it can also be taken to represent a tree (an entire tableaux), see below for some examples.

Parameters:

content (logics.classes.propositional.Formula) – The formula of the node
index (int, optional) – An optional index for tableaux that have indexed nodes
justification (str, optional) – If the node is non-root, this parameter should contain the name of the rule by which it was obtained
parent (logics.classes.propositional.proof_theories.TableauxNode, optional) – The parent node. The root node of a tableaux has None as parent (the default value).
children (list of logics.classes.propositional.proof_theories.TableauxNode, optional) – A list of the children node. Also optional. If child nodes are specified with the parent attribute, there is no need to provide this (see the example below).

Examples

Using the anytree package gives us a lot of base functionality. For example:

>>> from logics.utils.parsers import classical_parser
>>> from logics.classes.propositional.proof_theories import TableauxNode
>>> n1 = TableauxNode(content=classical_parser.parse('~~~~p'))
>>> n2 = TableauxNode(content=classical_parser.parse('~~p'), justification='R~~', parent=n1)
>>> n3 = TableauxNode(content=classical_parser.parse('p'), justification='R~~', parent=n2)
>>> n1.is_root
True
>>> n3.is_leaf
True
>>> n1.children  # returns (n2,)
(['~', ['~', ['p']]] (R~~),)
>>> n1.descendants  # returns (n2, n3)
(['~', ['~', ['p']]] (R~~), ['p'] (R~~))
>>> n3.root  # returns n1
['~', ['~', ['~', ['~', ['p']]]]]
>>> n1.leaves  # returns (n3,)
(['p'] (R~~),)
>>> n3.path  # returns (n1, n2, n3)
(['~', ['~', ['~', ['~', ['p']]]]], ['~', ['~', ['p']]] (R~~), ['p'] (R~~))
>>> n3.depth
2
>>> n1.height
2

Notes

The logics’ extension of the anytree node class also includes some methods for pretty printing tableaux as trees, see below.

separator = '==>'¶

The NodeMixin class extends any Python class to a tree node.

The only tree relevant information is the parent attribute. If None the NodeMixin is root node. If set to another node, the NodeMixin becomes the child of it.

The children attribute can be used likewise. If None the NodeMixin has no children. The children attribute can be set to any iterable of NodeMixin instances. These instances become children of the node.

>>> from anytree import NodeMixin, RenderTree
>>> class MyBaseClass(object):  # Just an example of a base class
...     foo = 4
>>> class MyClass(MyBaseClass, NodeMixin):  # Add Node feature
...     def __init__(self, name, length, width, parent=None, children=None):
...         super(MyClass, self).__init__()
...         self.name = name
...         self.length = length
...         self.width = width
...         self.parent = parent
...         if children:
...             self.children = children

Construction via parent:

>>> my0 = MyClass('my0', 0, 0)
>>> my1 = MyClass('my1', 1, 0, parent=my0)
>>> my2 = MyClass('my2', 0, 2, parent=my0)

>>> for pre, _, node in RenderTree(my0):
...     treestr = u"%s%s" % (pre, node.name)
...     print(treestr.ljust(8), node.length, node.width)
my0      0 0
├── my1  1 0
└── my2  0 2

Construction via children:

>>> my0 = MyClass('my0', 0, 0, children=[
...     MyClass('my1', 1, 0),
...     MyClass('my2', 0, 2),
... ]

>>> for pre, _, node in RenderTree(my0):
...     treestr = u"%s%s" % (pre, node.name)
...     print(treestr.ljust(8), node.length, node.width)
my0      0 0
├── my1  1 0
└── my2  0 2

Both approaches can be mixed:

>>> my0 = MyClass('my0', 0, 0, children=[
...     MyClass('my1', 1, 0),
... ]
>>> my2 = MyClass('my2', 0, 2, parent=my0)

>>> for pre, _, node in RenderTree(my0):
...     treestr = u"%s%s" % (pre, node.name)
...     print(treestr.ljust(8), node.length, node.width)
my0      0 0
├── my1  1 0
└── my2  0 2

is_instance_of(node, language, subst_dict=None, return_subst_dict=False)¶

Determines whether a node is as instance of another (schematic) node.

A TableauxNode (self) is considered an instance of another TableauxNode (node) iff:

The content of self is an instance of the content of node
The index and justification of self are equal to the index and justification of node, or are None in node

Parameters:

node (logics.classes.propositional.proof_theories.TableauxNode) – The (schematic) TableauxNode of which we want to know if it is instance
language (logics.classes.propositional.Language or logics.classes.propositional.InfiniteLanguage) – Instance of Language or InfiniteLanguage
subst_dict (dict, optional) – A susbstitution dict of the form {'A': someformula, 'B': someformula}
return_subst_dict (bool, optional) – If True will additionally return a substitution dict.

Examples

>>> from logics.utils.parsers import classical_parser
>>> from logics.instances.propositional.languages import classical_language
>>> from logics.classes.propositional.proof_theories import TableauxNode
>>> n1 = TableauxNode(content=classical_parser.parse('~A'))
>>> n2 = TableauxNode(content=classical_parser.parse('~~p'))
>>> n2.is_instance_of(n1, classical_language)
True
>>> n2.is_instance_of(n1, classical_language, subst_dict={'A': classical_parser.parse('q')})
False
>>> n2.is_instance_of(n1, classical_language, return_subst_dict=True)
(True, {'A': ['~', ['p']]})
>>> n3 = TableauxNode(content=classical_parser.parse('~~p'), justification='R~~')
>>> n3.is_instance_of(n1, classical_language)  # justification is None in n1
True
>>> n4 = TableauxNode(content=classical_parser.parse('A'), justification='R~~')
>>> n2.is_instance_of(n4, classical_language)  # Justification is None in n2 but not in n4
False

Notes

subst_dict and return_subst_dict are similar to the Formula homonymous methods.

instantiate(language, subst_dict, instantiate_children=True, first_iteration=True)¶

Given a TableauxNode with a schematic formula as content and a substitution dict, returns the schema instantiated with the dict.

Will return a different TableauxNode object, and not modify the original. If the node given is not the root node will construct a new tree with the node given as root. The children will also be new nodes.

Parameters:

language (logics.classes.propositional.Language or logics.classes.propositional.InfiniteLanguage) – Instance of Language or InfiniteLanguage
subst_dict (dict) – The susbstitution dict must have form {'A': someformula, 'B': someformula}
instantiate_children (bool, optional) – If True (default behavior), will also instantiate the children with the same substitution dict. Else, will leave them as is.
first_iteration (bool, optional) – For recursion purposes, should not be altered.

Returns:

A different formula instance from the original

Return type:

logics.classes.propositional.proof_theories.TableauxNode

Raises:

ValueError – if some schematic propositional within the formula has no substitution assigned in the dictionary

Examples

>>> from logics.utils.parsers import classical_parser
>>> from logics.instances.propositional.languages import classical_language
>>> from logics.classes.propositional.proof_theories import TableauxNode
>>> schema_parent = TableauxNode(content=classical_parser.parse('C'))
>>> schema = TableauxNode(content=classical_parser.parse('A ∨ B'), parent=schema_parent)
>>> schema_child = TableauxNode(content=classical_parser.parse('B'), parent=schema)
>>> instance1 = schema.instantiate(classical_language,
...                                {'A': classical_parser.parse('p'), 'B': classical_parser.parse('q')},
...                                instantiate_children=True)
>>> instance1
['∨', ['p'], ['q']]
>>> instance1.parent is None  # the resulting node is the root of the new instance tree
True
>>> instance1.children
(['q'],)
>>> instance2 = schema.instantiate(classical_language,
...                                {'A': classical_parser.parse('p'), 'B': classical_parser.parse('q')},
...                                instantiate_children=False)
>>> instance2
['∨', ['p'], ['q']]
>>> instance2.children
(['B'],)

property child_index¶

Returns the index of the node among the parent’s children. E.g. if the node is the second sibling, returns 1. For the root it will return 0

Examples

>>> from logics.classes.propositional.proof_theories import TableauxNode
>>> from logics.utils.parsers import classical_parser
>>> n1 = TableauxNode(content=classical_parser.parse('~(A ∧ B)'))
>>> n2 = TableauxNode(content=classical_parser.parse('~A'), justification='R∧', parent=n1)
>>> n3 = TableauxNode(content=classical_parser.parse('~B'), justification='R∧', parent=n1)
>>> n1.print_tree(classical_parser)  # For illustration purposes
~(A ∧ B)
├── ~A (R∧)
└── ~B (R∧)
>>> n2.child_index
0
>>> n3.child_index
1
>>> n1.child_index  # root node
0

print_path(parser=None)¶

Will print a node and its ancestors in a pretty format

If a parser is given as argument, returns the content unparsed

Examples

>>> from logics.utils.parsers import classical_parser
>>> from logics.classes.propositional.proof_theories import TableauxNode
>>> n1 = TableauxNode(content=classical_parser.parse('~~~~p'))
>>> n2 = TableauxNode(content=classical_parser.parse('~~p'), justification='R~~', parent=n1)
>>> n3 = TableauxNode(content=classical_parser.parse('p'), justification='R~~', parent=n2)
>>> n3.print_path()
['~', ['~', ['~', ['~', ['p']]]]] ==> ['~', ['~', ['p']]] (R~~) ==> ['p'] (R~~)
>>> n3.print_path(classical_parser)
~~~~p ==> ~~p (R~~) ==> p (R~~)

print_tree(parser=None)¶

Will print a node and its descendants in a pretty, tree-like, format

If a parser is given as argument, returns the content unparsed

Examples

>>> from logics.utils.parsers import classical_parser
>>> from logics.classes.propositional.proof_theories import TableauxNode
>>> n1 = TableauxNode(content=classical_parser.parse('~~~~p'))
>>> n2 = TableauxNode(content=classical_parser.parse('~~p'), justification='R~~', parent=n1)
>>> n3 = TableauxNode(content=classical_parser.parse('p'), justification='R~~', parent=n2)
>>> n1.print_tree()
['~', ['~', ['~', ['~', ['p']]]]], 0
└── ['~', ['~', ['p']]], 0 (R~~)
    └── ['p'], 0 (R~~)
>>> from logics.utils.parsers import classical_parser
>>> n1.print_tree(classical_parser)
~~~~p, 0
└── ~~p, 0 (R~~)
    └── p, 0 (R~~)

Tableaux System¶

class logics.classes.propositional.proof_theories.TableauxSystem(language, rules, closure_rules, solver=None)¶

Class for tableaux systems.

Parameters:

language (logics.classes.propositional.Language or logics.classes.propositional.InfiniteLanguage) – Instance of Language or InfiniteLanguage
rules (dict (str: logics.classes.propositional.proof_theories.TableauxNode)) – The keys are strings (the name of the rule) and the values are TableauxNode (w/schematic content and children)
closure_rules (list) – Each element of the list is a len2-list of (schematic) TableauxNode, e.g. [[TableauxNode(A), TableauxNode(~A)]] says that a node will be considered closed if A and ~A are found in its path.
solver – Any object with a solve method (which takes an inference and a tableaux system). None by default.

fast_node_is_closed_enabled¶

Class attribute. If True, will consider a node closed if and only if it finds A, i and ~A, i in its path. Will not look at the closure rules, but rather follow this hardcoded rule. Is faster but less general than using closure rules.

Type:: bool

Examples

Defining an example (toy) system with only conjunction and negation rules, and non-indexed nodes:

>>> from logics.utils.parsers import classical_parser
>>> from logics.instances.propositional.languages import classical_language
>>> from logics.classes.propositional.proof_theories import TableauxNode, TableauxSystem

We first define some rules:

>>> double_negation_rule = TableauxNode(content=classical_parser.parse('~~A'))
>>> TableauxNode(content=classical_parser.parse('A'), justification='R~~', parent=double_negation_rule)
>>> double_negation_rule.print_tree(classical_parser)  # For illustration purposes
~~A
└── A (R~~)
>>> conjunction_rule = TableauxNode(content=classical_parser.parse('A ∧ B'))
>>> conj_child1 = TableauxNode(content=classical_parser.parse('A'), justification='R∧', parent=conjunction_rule)
>>> TableauxNode(content=classical_parser.parse('B'), justification='R∧', parent=conj_child1)
>>> conjunction_rule.print_tree(classical_parser)  # For illustration purposes
(A ∧ B)
└── A (R∧)
    └── B (R∧)
>>> neg_conjunction_rule = TableauxNode(content=classical_parser.parse('~(A ∧ B)'))
>>> TableauxNode(content=classical_parser.parse('~A'), justification='R~∧', parent=neg_conjunction_rule)
>>> TableauxNode(content=classical_parser.parse('~B'), justification='R~∧', parent=neg_conjunction_rule)
>>> neg_conjunction_rule.print_tree(classical_parser)  # For illustration purposes
~(A ∧ B)
├── ~A (R~∧)
└── ~B (R~∧)

Now we can define the system:

>>> system_rules = {
...     'R~~': double_negation_rule,
...     'R∧': conjunction_rule,
...     'R~∧': neg_conjunction_rule}
>>> closure_rules = [
...     [TableauxNode(content=classical_parser.parse('~A')), TableauxNode(content=classical_parser.parse('A'))]
... ]  # This is actually not necessary since fast_node_is_closed_enabled is True by default
>>> toy_tableaux_system = TableauxSystem(language=classical_language,
...                                      rules=system_rules,
...                                      closure_rules= closure_rules)

Notes

There are predefined instances of this class for known systems, see below.
If some rule contains two versions (e.g. A ∧ B ⇛ A ⇛ B and A ∧ B ⇛ B ⇛ A), you can name them R∧_1 and R∧_2 the rules dict, but put only R∧ in the justification of the children for both. See the test for is_correct_tree in the tests module for an example.

node_is_closed(node)¶

Checks whether a node is closed, by looking at its ancestors

A node is considered closed when an instance of a closure rule occurs in its path (see also the fast_node_is_closed_enabled class attribute).

Examples

>>> from logics.utils.parsers import classical_parser
>>> from logics.classes.propositional.proof_theories import TableauxNode
>>> from logics.instances.propositional.tableaux import classical_tableaux_system
>>> n1 = TableauxNode(content=classical_parser.parse('~~~~p'))
>>> n2 = TableauxNode(content=classical_parser.parse('~p'), parent=n1)
>>> n3 = TableauxNode(content=classical_parser.parse('~~p'), justification='R~~', parent=n2)
>>> n1.print_tree(classical_parser)  # For illustration purposes
(~~~p)
└── ~p
    └── ~~p (R~~)
>>> classical_tableaux_system.node_is_closed(n2)
False
>>> classical_tableaux_system.node_is_closed(n3)
True

tree_is_closed(node)¶

Same as above, but checks if all descendant branches (including the current node) are closed

Will consider the node given as the root of the tableaux (i.e. will not look at its ancestors).

Examples

>>> from logics.utils.parsers import classical_parser
>>> from logics.classes.propositional.proof_theories import TableauxNode
>>> from logics.instances.propositional.tableaux import classical_tableaux_system
>>> n1 = TableauxNode(content=classical_parser.parse('~~p ∧ q'))
>>> n2 = TableauxNode(content=classical_parser.parse('~p'), parent=n1)
>>> n3 = TableauxNode(content=classical_parser.parse('q'), justification='R∧', parent=n2)
>>> n4 = TableauxNode(content=classical_parser.parse('p'), justification='R~~', parent=n3)
>>> n1.print_tree(classical_parser)  # For illustration purposes
(~~p ∧ q)
└── ~p
    └── q (R∧)
        └── p (R~~)
>>> classical_tableaux_system.tree_is_closed(n1)
True
>>> classical_tableaux_system.tree_is_closed(n3)
False

get_counterexamples(tree, exit_on_first=False)¶

Given a tree, returns a valuation that constitutes a counterexample to it.

The valuation is returned as a dict, where the keys are propositional letters (strings) and the values are truth values. E.g. {'p': '1', 'q': '0'}. If exit_on_first is false, will return a list of such dicts. If the tree is closed, returns None.

Note that the dicts only contains the valuations of the atomics needed to produce a counterexample. If some propositional letter present in the inference does not appear on the open branch, this will not assign it any value.

Parameters:

tree (logics.classes.propositional.proof_theories.TableauxNode) – The root of the tree we want to look at
exit_on_first (bool, optional) – Whether it returns a single counterexample (if True) or many

Examples

>>> from logics.utils.parsers import classical_parser
>>> from logics.classes.propositional.proof_theories import TableauxNode
>>> from logics.instances.propositional.tableaux import classical_tableaux_system
>>> n1 = TableauxNode(content=classical_parser.parse('p ∧ q'))
>>> n2 = TableauxNode(content=classical_parser.parse('~p'), parent=n1)
>>> n3 = TableauxNode(content=classical_parser.parse('q'), justification='R∧', parent=n2)
>>> n4 = TableauxNode(content=classical_parser.parse('p'), justification='R~~', parent=n2)
>>> n1.print_tree(classical_parser)  # For illustration purposes
p ∧ q
└── ~p
    ├── q (R∧)
    └── p (R~~)
>>> classical_tableaux_system.get_counterexample(n1, exit_on_first=True)
{'p': '0', 'q': '1'}
>>> classical_tableaux_system.get_counterexample(n1)  # exit_on_first is False by default
[{'p': '0', 'q': '1'}]

Notes

Make sure the node you are passing as tree has no parents, otherwise you might get incorrect results

rule_is_applicable(node, rule_name, return_subst_dict=False)¶

Given a node and a rule name, determines if the rule can be applied to the node.

If the rule has more than one premise, the node must be an instance of the last premise of the rule, and instances of the rest of the premises should be present above in the tree.

Parameters:

node (logics.classes.propositional.proof_theories.TableauxNode) – The node we want to look at
rule_name (str) – The name of the rule. Should be present as key in TableauxSystem rules parameter
return_subst_dict (bool) – If True will additionally return a substitution dict.

Examples

>>> from logics.utils.parsers import classical_parser
>>> from logics.classes.propositional.proof_theories import TableauxNode
>>> from logics.instances.propositional.tableaux import classical_tableaux_system
>>> n1 = TableauxNode(content=classical_parser.parse('~~p ∧ q'))
>>> classical_tableaux_system.rule_is_applicable(n1, 'R~~')
False
>>> classical_tableaux_system.rule_is_applicable(n1, 'R∧')
True
>>> classical_tableaux_system.rule_is_applicable(n1, 'R∧', return_subst_dict=True)
(True, {'A': ['~', ['~', ['p']]], 'B': ['q']})
True

is_correct_tree(tree, inference=None, return_error_list=False, exit_on_first_error=False, parser=None)¶

Checks if a given tableaux (a node and its descendants) is correctly derived, given the rules of the system.

Parameters:

tree (logics.classes.propositional.proof_theories.TableauxNode) – A TableauxNode, posssibly with children.
inference (logics.classes.propositional.Inference or None, optional) – If None, will just check correct application of the rules. If an inference, will check that the steps with no justification are either premises or the negation of the conclusion (this behavior can be overriden for other systems, see the source code).
return_error_list (bool, optional) – If False, will just return True or False (exits when it finds an error, more efficient) If True, will return (True, a list of logics.classes.errors.CorrectionError)
exit_on_first_error (bool, optional) – If return_error_list and this are both true, it will return a list with a single error instead of many. More efficient, since it makes early exits.
parser (logics.utils.parsers.standard_parser.StandardParser, optional) – If present, will return the error list with unparsed instead of parsed formulae. Can be of another class that implements unparse for Formula. Can be the classical_parser (see below in the Examples) or some other parser defined by the user.

Examples

>>> from logics.utils.parsers import classical_parser
>>> from logics.classes.propositional.proof_theories import TableauxNode
>>> from logics.instances.propositional.tableaux import classical_tableaux_system

A correct derivation of ~~p ∧ q / p:

>>> n1 = TableauxNode(content=classical_parser.parse('~~p ∧ q'))
>>> n2 = TableauxNode(content=classical_parser.parse('~p'), parent=n1)
>>> n3 = TableauxNode(content=classical_parser.parse('~~p'), justification='R∧', parent=n2)
>>> n4 = TableauxNode(content=classical_parser.parse('q'), justification='R∧', parent=n3)
>>> n5 = TableauxNode(content=classical_parser.parse('p'), justification='R~~', parent=n4)
>>> n1.print_tree(classical_parser)  # For illustration purposes
(~~p ∧ q)
└── ~p
    └── q (R∧)
        └── p (R~~)
>>> classical_tableaux_system.is_correct_tree(n1)
True
>>> classical_tableaux_system.is_correct_tree(n1, inference=classical_parser.parse('~~p ∧ q / p'))
True
>>> classical_tableaux_system.is_correct_tree(n1, inference=classical_parser.parse('~~p ∧ q / ~p'))
False
>>> classical_tableaux_system.is_correct_tree(n1, inference=classical_parser.parse('~~p ∧ q / ~p'),
...                                           return_error_list=True)
(False, [(): Conclusion ['~', ['p']] is not present in the tree, (0, 0): Node ['~', ['p']] is an incorrect premise node])
>>> from logics.utils.parsers import classical_parser
>>> classical_tableaux_system.is_correct_tree(n1, inference=classical_parser.parse('~~p ∧ q / ~p'),
...                                           return_error_list=True, parser=classical_parser)
(False, [(): Conclusion ~p is not present in the tree, (0, 0): Node ~p is an incorrect premise node])

Notes

All premise nodes (including negations of conclusions) must come at the beginning of the tableaux, before any other rules are applied and before branching. Otherwise the tableaux will be marked as incorrect.

solve_tree(inference)¶

Takes an inference and returns its tree-derivation

For this to work, the parameter solver must be assigned.

Examples

>>> from logics.utils.parsers import classical_parser
>>> from logics.instances.propositional.tableaux import classical_tableaux_system
>>> tree = classical_tableaux_system.solve_tree(classical_parser.parse("~(p ∧ q) / ~p ∨ ~q"))
>>> tree.print_tree(classical_parser)
~(p ∧ q)
└── ~(~p ∨ ~q)
    ├── ~p (R~∧)
    │   └── ~~p (R~∨)
    │       └── ~~q (R~∨)
    └── ~q (R~∧)
        └── ~~p (R~∨)
            └── ~~q (R~∨)

is_valid(inference)¶

Takes an inference and determines wheter it is valid

For this to work, the parameter solver must be assigned.

Examples

>>> from logics.utils.parsers import classical_parser
>>> from logics.instances.propositional.tableaux import classical_tableaux_system
>>> classical_tableaux_system.is_valid(classical_parser.parse("~(p ∧ q) / ~p ∨ ~q"))
True
>>> classical_tableaux_system.is_valid(classical_parser.parse("p / q"))
False

class logics.classes.propositional.proof_theories.tableaux.ManyValuedTableauxSystem(language, rules, closure_rules, solver=None)¶

Class for many-valued tableaux systems.

Basically the same as the above, only overrides what it considers a correct non-justified node, since the initial nodes have form premise, 1 or conclusion, 0. Note that A, 0 and ~A, 1 are different claims in this kind of system.

Examples

>>> from logics.utils.parsers import classical_parser
>>> from logics.classes.propositional.proof_theories import TableauxNode
>>> from logics.instances.propositional.tableaux import FDE_tableaux_system
>>> inference = classical_parser.parse("~~p ∧ q / p")

Incorrectly initializing the tableaux:

>>> n1 = TableauxNode(content=classical_parser.parse('~~p ∧ q'), index=1)
>>> n2 = TableauxNode(content=classical_parser.parse('~p'), index=1, parent=n1)
>>> n3 = TableauxNode(content=classical_parser.parse('~~p'), index=1, justification="R∧1", parent=n2)
>>> n4 = TableauxNode(content=classical_parser.parse('q'), index=1, justification="R∧1", parent=n3)
>>> n5 = TableauxNode(content=classical_parser.parse('p'), index=1, justification="R~~1", parent=n4)
>>> n1.print_tree(classical_parser)  # For illustration purposes
(~~p ∧ q), 1
└── ~p, 1
    └── ~~p, 1 (R∧1)
        └── q, 1 (R∧1)
            └── p, 1 (R~~1)
>>> FDE_tableaux_system.is_correct_tree(n1, inference=inference)
False
>>> FDE_tableaux_system.is_correct_tree(n1, inference=inference, return_error_list=True)
(False, ["Node ['~', ['p']], 1 is an incorrect premise node", "Nodes {['~', ['p']], 1} are not accounted for in the derivation"])

To initialize it correctly we must do the following:

>>> n1 = TableauxNode(content=classical_parser.parse('~~p ∧ q'), index=1)
>>> n2 = TableauxNode(content=classical_parser.parse('p'), index=0, parent=n1)  # <-- This changed
>>> n3 = TableauxNode(content=classical_parser.parse('~~p'), index=1, justification="R∧1", parent=n2)
>>> n4 = TableauxNode(content=classical_parser.parse('q'), index=1, justification="R∧1", parent=n3)
>>> n5 = TableauxNode(content=classical_parser.parse('p'), index=1, justification="R~~1", parent=n4)
>>> n1.print_tree(classical_parser)  # For illustration purposes
(~~p ∧ q), 1
└── p, 0
    └── ~~p, 1 (R∧1)
        └── q, 1 (R∧1)
            └── p, 1 (R~~1)
>>> FDE_tableaux_system.is_correct_tree(n1, inference=inference)
True
>>> # Also considers it closed bc of how the closure rules are given to the instance, see below
>>> FDE_tableaux_system.tree_is_closed(n1)
True

Note that the get_counterexamples method takes two extra parameters, gap_value and glut_value (both of which default to None, but can be set to strings). For example:

>>> from logics.instances.propositional.tableaux import classical_indexed_tableaux_system,
>>> from logics.instances.propositional.tableaux import K3_tableaux_system, LP_tableaux_system
>>> n1 = TableauxNode(content=classical_parser('~p'), index=1)
>>> n2 = TableauxNode(content=classical_parser('~q'), index=1, parent=n1)
>>> n3 = TableauxNode(content=classical_parser('p'), index=1, parent=n2)
>>> n1.print_tree(classical_parser)  # For illustration purposes
~p, 1
└── ~q, 1
    └── p, 1
>>> classical_indexed_tableaux_system.get_counterexamples(n1)  # Only looks at atomics
[{'p': '1'}]
>>> K3_tableaux_system.get_counterexamples(n1, gap_value='i') is None  # in k3 this is closed
True
>>> LP_tableaux_system.get_counterexamples(n1, glut_value='i')
[{'p': 'i', 'q': '0'}]
>>> FDE_tableaux_system.get_counterexamples(n1, gap_value='n', glut_value='b')
[{'p': 'b', 'q': '0'}]

class logics.classes.propositional.proof_theories.tableaux.IndexedTableauxSystem(language, rules, closure_rules, solver=None)¶

Class for propositional indexed tableaux.

Initializes nodes as the ManyValuedTableauxSystem, and has [(A, 1), (A, 0)] as a hardcoded closure rule.

Instances¶

logics.instances.propositional.tableaux.classical_tableaux_system¶

Has the following rules:

classical_double_negation_rule = TableauxNode(content=Formula(['~', ['~', ['A']]]))
TableauxNode(content=Formula(['A']), justification='R~~', parent=classical_double_negation_rule)
'''
['~', ['~', ['A']]]
└── ['A'] (R~~)
'''

classical_conjunction_rule = TableauxNode(content=Formula(['∧', ['A'], ['B']]))
ccr2 = TableauxNode(content=Formula(['A']), justification='R∧', parent=classical_conjunction_rule)
TableauxNode(content=Formula(['B']), justification='R∧', parent=ccr2)
'''
['∧', ['A'], ['B']]
└── ['A'] (R∧)
    └── ['B'] (R∧)
'''

classical_neg_conjunction_rule = TableauxNode(content=Formula(['~', ['∧', ['A'], ['B']]]))
TableauxNode(content=Formula(['~', ['A']]), justification='R~∧', parent=classical_neg_conjunction_rule)
TableauxNode(content=Formula(['~', ['B']]), justification='R~∧', parent=classical_neg_conjunction_rule)
'''
['~', ['∧', ['A'], ['B']]]
├── ['~', ['A']] (R~∧)
└── ['~', ['B']] (R~∧)
'''

classical_disjunction_rule = TableauxNode(content=Formula(['∨', ['A'], ['B']]))
TableauxNode(content=Formula(['A']), justification='R∨', parent=classical_disjunction_rule)
TableauxNode(content=Formula(['B']), justification='R∨', parent=classical_disjunction_rule)
'''
['∨', ['A'], ['B']]
├── ['A'] (R∨)
└── ['B'] (R∨)
'''

classical_neg_disjunction_rule = TableauxNode(content=Formula(['~', ['∨', ['A'], ['B']]]))
cndr2 = TableauxNode(content=Formula(['~', ['A']]), justification='R~∨', parent=classical_neg_disjunction_rule)
TableauxNode(content=Formula(['~', ['B']]), justification='R~∨', parent=cndr2)
'''
['~', ['∨', ['A'], ['B']]]
└── ['~', ['A']] (R~∨)
    └── ['~', ['B']] (R~∨)
'''

classical_conditional_rule = TableauxNode(content=Formula(['→', ['A'], ['B']]))
TableauxNode(content=Formula(['~', ['A']]), justification='R→', parent=classical_conditional_rule)
TableauxNode(content=Formula(['B']), justification='R→', parent=classical_conditional_rule)
'''
['→', ['A'], ['B']]
├── ['~', ['A']] (R→)
└── ['B'] (R→)
'''

classical_neg_conditional_rule = TableauxNode(content=Formula(['~', ['→', ['A'], ['B']]]))
cncr2 = TableauxNode(content=Formula(['A']), justification='R~→', parent=classical_neg_conditional_rule)
TableauxNode(content=Formula(['~', ['B']]), justification='R~→', parent=cncr2)
'''
['~', ['→', ['A'], ['B']]]
└── ['A'] (R~→)
    └── ['~', ['B']] (R~→)
'''

classical_biconditional_rule = TableauxNode(content=Formula(['↔', ['A'], ['B']]))
cbr2 = TableauxNode(content=Formula(['A']), justification='R↔', parent=classical_biconditional_rule)
TableauxNode(content=Formula(['B']), justification='R↔', parent=cbr2)
cbr3 = TableauxNode(content=Formula(['~', ['A']]), justification='R↔', parent=classical_biconditional_rule)
TableauxNode(content=Formula(['~', ['B']]), justification='R↔', parent=cbr3)
'''
['↔', ['A'], ['B']]
├── ['A'] (R↔)
│   └── ['B'] (R↔)
└── ['~', ['A']] (R↔)
    └── ['~', ['B']] (R↔)
'''

classical_neg_biconditional_rule = TableauxNode(content=Formula(['~', ['↔', ['A'], ['B']]]))
cnbr2 = TableauxNode(content=Formula(['~', ['A']]), justification='R~↔', parent=classical_neg_biconditional_rule)
TableauxNode(content=Formula(['B']), justification='R~↔', parent=cnbr2)
cnbr3 = TableauxNode(content=Formula(['A']), justification='R~↔', parent=classical_neg_biconditional_rule)
TableauxNode(content=Formula(['~', ['B']]), justification='R~↔', parent=cnbr3)
'''
['~', ['↔', ['A'], ['B']]]
├── ['~', ['A']] (R~↔)
│   └── ['B'] (R~↔)
└── ['A'] (R~↔)

Closes a branch when both A and ~A occur in it (for some formula A)

logics.instances.propositional.tableaux.classical_indexed_tableaux_system¶

Indexed presentation of classical logic. Has the following rules:

idx_classical_negation1 = TableauxNode(content=Formula(['~', ['A']]), index=1)
TableauxNode(content=Formula(['A']), index=0, justification='R~1', parent=idx_classical_negation1)
'''
['~', ['A']], 1
└── ['A'], 0 (R~1)
'''

idx_classical_negation0 = TableauxNode(content=Formula(['~', ['A']]), index=0)
TableauxNode(content=Formula(['A']), index=1, justification='R~0', parent=idx_classical_negation0)
'''
['~', ['A']], 0
└── ['A'], 1 (R~0)
'''

idx_classical_conjunction1 = TableauxNode(content=Formula(['∧', ['A'], ['B']]), index=1)
idx_cr2 = TableauxNode(content=Formula(['A']), index=1, justification='R∧1', parent=idx_classical_conjunction1)
TableauxNode(content=Formula(['B']), index=1, justification='R∧1', parent=idx_cr2)
'''
['∧', ['A'], ['B']], 1
└── ['A'], 1 (R∧1)
    └── ['B'], 1 (R∧1)
'''

idx_classical_conjunction0 = TableauxNode(content=Formula(['∧', ['A'], ['B']]), index=0)
TableauxNode(content=Formula(['A']), index=0, justification='R∧0', parent=idx_classical_conjunction0)
TableauxNode(content=Formula(['B']), index=0, justification='R∧0', parent=idx_classical_conjunction0)
'''
['∧', ['A'], ['B']], 0
├── ['A'], 0 (R∧0)
└── ['B'], 0 (R∧0)
'''

idx_classical_disjunction1 = TableauxNode(content=Formula(['∨', ['A'], ['B']]), index=1)
TableauxNode(content=Formula(['A']), index=1, justification='R∨1', parent=idx_classical_disjunction1)
TableauxNode(content=Formula(['B']), index=1, justification='R∨1', parent=idx_classical_disjunction1)
'''
['∨', ['A'], ['B']], 1
├── ['A'], 1 (R∨1)
└── ['B'], 1 (R∨1)
'''

idx_classical_disjunction0 = TableauxNode(content=Formula(['∨', ['A'], ['B']]), index=0)
idx_dr2 = TableauxNode(content=Formula(['A']), index=0, justification='R∨0', parent=idx_classical_disjunction0)
TableauxNode(content=Formula(['B']), index=0, justification='R∨0', parent=idx_dr2)
'''
['∨', ['A'], ['B']], 0
└── ['A'], 0 (R∨0)
    └── ['B'], 0 (R∨0)
'''

idx_classical_conditional1 = TableauxNode(content=Formula(['→', ['A'], ['B']]), index=1)
TableauxNode(content=Formula(['A']), index=0, justification='R→1', parent=idx_classical_conditional1)
TableauxNode(content=Formula(['B']), index=1, justification='R→1', parent=idx_classical_conditional1)
'''
['→', ['A'], ['B']], 1
├── ['A'], 0 (R→1)
└── ['B'], 1 (R→1)
'''

idx_classical_conditional0 = TableauxNode(content=Formula(['→', ['A'], ['B']]), index=0)
idx_cr2 = TableauxNode(content=Formula(['A']), index=1, justification='R→0', parent=idx_classical_conditional0)
TableauxNode(content=Formula(['B']), index=0, justification='R→0', parent=idx_cr2)
'''
['→', ['A'], ['B']], 0
└── ['A'], 1 (R→0)
    └── ['B'], 0 (R→0)
'''

idx_classical_biconditional1 = TableauxNode(content=Formula(['↔', ['A'], ['B']]), index=1)
idx_cbr2 = TableauxNode(content=Formula(['A']), index=1, justification='R↔1', parent=idx_classical_biconditional1)
TableauxNode(content=Formula(['B']), index=1, justification='R↔1', parent=idx_cbr2)
idx_cbr3 = TableauxNode(content=Formula(['A']), index=0, justification='R↔1', parent=idx_classical_biconditional1)
TableauxNode(content=Formula(['B']), index=0, justification='R↔1', parent=idx_cbr3)
'''
['↔', ['A'], ['B']], 1
├── ['A'], 1 (R↔1)
│   └── ['B'], 1 (R↔1)
└── ['A'], 0 (R↔1)
    └── ['B'], 0 (R↔1)
'''

idx_classical_biconditional0 = TableauxNode(content=Formula(['↔', ['A'], ['B']]), index=0)
idx_cbr4 = TableauxNode(content=Formula(['A']), index=1, justification='R↔0', parent=idx_classical_biconditional0)
TableauxNode(content=Formula(['B']), index=0, justification='R↔0', parent=idx_cbr4)
idx_cbr5 = TableauxNode(content=Formula(['A']), index=0, justification='R↔0', parent=idx_classical_biconditional0)
TableauxNode(content=Formula(['B']), index=1, justification='R↔0', parent=idx_cbr5)
'''
['↔', ['A'], ['B']], 0
├── ['A'], 1 (R↔0)
│   └── ['B'], 0 (R↔0)
└── ['A'], 0 (R↔0)
    └── ['B'], 1 (R↔0)
'''

Closes a branch when both A, 1 and A, 0 occur in it (for some formula A)

logics.instances.propositional.tableaux.FDE_tableaux_system¶

logics.instances.propositional.tableaux.LP_tableaux_system¶

logics.instances.propositional.tableaux.K3_tableaux_system¶

All three systems share the following rules (note there is no conditional nor biconditional):

FDE_double_negation_rule1 = TableauxNode(content=Formula(['~', ['~', ['A']]]), index=1)
TableauxNode(content=Formula(['A']), index=1, justification='R~~1', parent=FDE_double_negation_rule1)
'''
['~', ['~', ['A']]], 1
└── ['A'], 1 (R~~1)
'''

FDE_double_negation_rule0 = TableauxNode(content=Formula(['~', ['~', ['A']]]), index=0)
TableauxNode(content=Formula(['A']), index=0, justification='R~~0', parent=FDE_double_negation_rule0)
'''
['~', ['~', ['A']]], 0
└── ['A'], 0 (R~~0)
'''

FDE_conjunction_rule1 = TableauxNode(content=Formula(['∧', ['A'], ['B']]), index=1)
FDEcr1 = TableauxNode(content=Formula(['A']), index=1, justification='R∧1', parent=FDE_conjunction_rule1)
TableauxNode(content=Formula(['B']), index=1, justification='R∧1', parent=FDEcr1)
'''
['∧', ['A'], ['B']], 1
└── ['A'], 1 (R∧1)
    └── ['B'], 1 (R∧1)
'''

FDE_conjunction_rule0 = TableauxNode(content=Formula(['∧', ['A'], ['B']]), index=0)
TableauxNode(content=Formula(['A']), index=0, justification='R∧0', parent=FDE_conjunction_rule0)
TableauxNode(content=Formula(['B']), index=0, justification='R∧0', parent=FDE_conjunction_rule0)
'''
['∧', ['A'], ['B']], 0
├── ['A'], 0 (R∨0)
└── ['B'], 0 (R∨0)
'''

FDE_neg_conjunction_rule1 = TableauxNode(content=Formula(['~', ['∧', ['A'], ['B']]]), index=1)
TableauxNode(content=Formula(['∨', ['~', ['A']], ['~', ['B']]]), index=1, justification='R~∧1',
             parent=FDE_neg_conjunction_rule1)
'''
['~', ['∧', ['A'], ['B']]], 1
└── ['∨', ['~', ['A']], ['~', ['B']]], 1 (R~∧1)
'''

FDE_neg_conjunction_rule0 = TableauxNode(content=Formula(['~', ['∧', ['A'], ['B']]]), index=0)
TableauxNode(content=Formula(['∨', ['~', ['A']], ['~', ['B']]]), index=0, justification='R~∧0',
             parent=FDE_neg_conjunction_rule0)
'''
['~', ['∧', ['A'], ['B']]], 0
└── ['∨', ['~', ['A']], ['~', ['B']]], 0 (R~∧0)
'''

FDE_disjunction_rule1 = TableauxNode(content=Formula(['∨', ['A'], ['B']]), index=1)
TableauxNode(content=Formula(['A']), index=1, justification='R∨1', parent=FDE_disjunction_rule1)
TableauxNode(content=Formula(['B']), index=1, justification='R∨1', parent=FDE_disjunction_rule1)
'''
['∨', ['A'], ['B']], 1
├── ['A'], 1 (R∨1)
└── ['B'], 1 (R∨1)
'''

FDE_disjunction_rule0 = TableauxNode(content=Formula(['∨', ['A'], ['B']]), index=0)
FDEdr1 = TableauxNode(content=Formula(['A']), index=0, justification='R∨0', parent=FDE_disjunction_rule0)
TableauxNode(content=Formula(['B']), index=0, justification='R∨0', parent=FDEdr1)
'''
['∨', ['A'], ['B']], 0
└── ['A'], 0 (R∨0)
    └── ['B'], 0 (R∨0)
'''

FDE_neg_disjunction_rule1 = TableauxNode(content=Formula(['~', ['∨', ['A'], ['B']]]), index=1)
TableauxNode(content=Formula(['∧', ['~', ['A']], ['~', ['B']]]), index=1, justification='R~∨1',
             parent=FDE_neg_disjunction_rule1)
'''
['~', ['∨', ['A'], ['B']]], 1
└── ['∧', ['~', ['A']], ['~', ['B']]], 1 (R~∨1)
'''

FDE_neg_disjunction_rule0 = TableauxNode(content=Formula(['~', ['∨', ['A'], ['B']]]), index=0)
TableauxNode(content=Formula(['∧', ['~', ['A']], ['~', ['B']]]), index=0, justification='R~∨0',
             parent=FDE_neg_disjunction_rule0)
'''
['~', ['∨', ['A'], ['B']]], 0
└── ['∧', ['~', ['A']], ['~', ['B']]], 0 (R~∨0)
'''

They only differ in their closure rules:

FDE_closure_rules = [
    [TableauxNode(content=Formula(['A']), index=0),
     TableauxNode(content=Formula(['A']), index=1)]
]
K3_closure_rules = FDE_closure_rules + \
                   [[TableauxNode(content=Formula(['A']), index=1),
                     TableauxNode(content=Formula(['~', ['A']]), index=1)]]
LP_closure_rules = FDE_closure_rules + \
                   [[TableauxNode(content=Formula(['A']), index=0),
                     TableauxNode(content=Formula(['~', ['A']]), index=0)]]

Tableaux Solver¶

class logics.utils.solvers.tableaux.TableauxSolver¶

Solver for tableaux systems

Will build a tree for an (either valid or invalid) inference. When a branch is closed, does not continue adding nodes to it. Does not have the rules hardcoded. The solve method takes a tableaux system as parameter, and the tableaux solver will derive with the rules of the system you give it.

beggining_premise_index¶

Class attribute representing the index that the premises have at the beggining of the derivation. None by default.

Type:: int or None

beggining_conclusion_index¶

Class attribute representing the index that the conclusion has at the beggining of the derivation. None by default.

Type:: int or None

solve(inference, tableaux_system, beggining_index=None, max_depth=100)¶

Builds a tableaux for an inference, given a tableaux system with which to operate.

Parameters:

inference (logics.classes.propositional.Inference) – The Inference to build a tableaux for
tableaux_system (logics.classes.propositional.proof_theories.TableauxSystem) – A TableauxSystem or any class that inherits from it.
beggining_index (list or set, optional) – For systems that require you to specify a label at the beginning of the proof (e.g. for metainferential tableaux it can be things like {‘1’}, {‘1’, ‘i’}, [{‘1’, ‘i’}, {‘1’}], [[{‘1’, ‘i’}, {‘1’}], [{‘1’}, {‘1’, ‘i’}]] for S, T, TS, TS/ST, respectively)
max_depth (int, optional) – The maximum depth that a tableaux can have. Default is 100. Set it to None if you want infinity.

Examples

>>> from logics.utils.parsers import classical_parser
>>> from logics.utils.solvers.tableaux import standard_tableaux_solver  # <-- The default instance of the solver
>>> from logics.instances.propositional.tableaux import classical_tableaux_system
>>> tree = standard_tableaux_solver.solve(classical_parser.parse("~(p ∨ q) / ~p ∧ ~q"), classical_tableaux_system)
>>> tree.print_tree(classical_parser)
~(p ∨ q)
└── ~(~p ∧ ~q)
    └── ~p (R~∨)
        └── ~q (R~∨)
            ├── ~~p (R~∧)
            └── ~~q (R~∧)
>>> tree = standard_tableaux_solver.solve(classical_parser.parse("p ↔ ~(q → r) / ~~p ∨ q"), classical_tableaux_system)
>>> tree.print_tree(classical_parser)
(p ↔ ~(q → r))
└── ~(~~p ∨ q)
    ├── p (R↔)
    │   └── ~(q → r) (R↔)
    │       └── ~~~p (R~∨)
    │           └── ~q (R~∨)
    │               └── q (R~→)
    │                   └── ~r (R~→)
    └── ~p (R↔)
        └── ~~(q → r) (R↔)
            └── ~~~p (R~∨)
                └── ~q (R~∨)
                    └── (q → r) (R~~)
                        └── ~p (R~~)
                            ├── ~q (R→)
                            └── r (R→)

class logics.utils.solvers.tableaux.IndexedTableauxSolver¶

Class for classical indexed and many-valued tableaux systems

Basically the same as the above solver, only changes the way in which the tableaux is initialized (does not negate the conclusion, beggining_premise_index is 1, beggining_conclusion_index is 0)

Examples

>>> from logics.utils.parsers import classical_parser
>>> from logics.utils.solvers.tableaux import indexed_tableaux_solver  # <-- The default instance of the solver
>>> from logics.instances.propositional.tableaux import LP_tableaux_system
>>> tree = indexed_tableaux_solver.solve(classical_parser.parse("~(p ∨ q) / ~~p ∧ ~~q"), LP_tableaux_system)
>>> tree.print_tree(classical_parser)
~(p ∨ q), 1
└── (~~p ∧ ~~q), 0
    └── (~p ∧ ~q), 1 (R~∨1)
        ├── ~~p, 0 (R∧0)
        │   └── ~p, 1 (R∧1)
        │       └── ~q, 1 (R∧1)
        │           └── p, 0 (R~~0)
        └── ~~q, 0 (R∧0)
            └── ~p, 1 (R∧1)
                └── ~q, 1 (R∧1)
                    └── q, 0 (R~~0)

Constructive Tree System¶

class logics.classes.propositional.proof_theories.tableaux.ConstructiveTreeSystem(language, solver=None)¶

Constructive tree system for a given language

Only takes a language (make sure it is an instance of InfiniteLanguage) and, optionally, a solver. Will automatically build the tableaux rules from the given language.

Examples

>>> from logics.utils.parsers import classical_parser
>>> from logics.instances.propositional.languages import classical_infinite_language
>>> from logics.utils.solvers.tableaux import constructive_tree_solver
>>> from logics.classes.propositional.proof_theories.tableaux import ConstructiveTreeSystem
>>> classical_ct_system = ConstructiveTreeSystem(classical_infinite_language, solver=constructive_tree_solver)

The rules are automatically built:

>>> classical_ct_system.rules['R~'].print_tree(classical_parser)
~A1
└── A1 (R~)
>>> classical_ct_system.rules['R∧'].print_tree(classical_parser)
A1 ∧ A2
├── A1 (R∧)
└── A2 (R∧)

The solver works as expected:

>>> tree = classical_ct_system.solve_tree(classical_parser.parse('p and not q'))
>>> tree.print_tree(classical_parser)
p ∧ ~q
├── p (R∧)
└── ~q (R∧)
    └── q (R~)
>>> tree = classical_ct_system.solve_tree(classical_parser.parse('(p iff ~r) and ~~q'))
>>> tree.print_tree(classical_parser)
(p ↔ ~r) ∧ ~~q
├── p ↔ ~r (R∧)
│   ├── p (R↔)
│   └── ~r (R↔)
│       └── r (R~)
└── ~~q (R∧)
    └── ~q (R~)

node_is_closed(node)¶

In a constructive tree system a node is considered closed iff its content is an atomic wff

Examples

>>> from logics.utils.parsers import classical_parser
>>> from logics.instances.propositional.tableaux import classical_constructive_tree_system  # Identical to the above
>>> tree = classical_constructive_tree_system.solve_tree(classical_parser.parse('~p'))
>>> classical_constructive_tree_system.node_is_closed(tree.children[0])
True
>>> classical_constructive_tree_system.tree_is_closed(tree)
True

is_well_formed(formula)¶

Determines through tableaux methods if a formula is well-formed (if its constructive tree is closed)

This method is actually an alias of is_valid

Examples

>>> from logics.classes.propositional import Formula
>>> from logics.instances.propositional.tableaux import classical_constructive_tree_system
>>> classical_constructive_tree_system.is_well_formed(Formula(['~', ['~', ['p']]]))
True
>>> classical_constructive_tree_system.is_well_formed(Formula(['~', '~', ['p']]))
False