Metainferential Tableaux¶
Classes for metainferential tableaux, of the kind described in (citation needed)
Base Classes¶
- class logics.classes.propositional.proof_theories.metainferential_tableaux.MetainferentialTableauxStandard(content, bar=False)¶
Class for a standard in metainferential tableaux (the second member of each node)
- Parameters:
content (list or set or string) – Basic (level-0) indices are sets (e.g.
{'1', 'i'}
), higher level standards are 2-lists of lower level ones, (e.g.[{'1', 'i'}, {'1'}]
-aka TS). The formulation of a system’s rules can include variables as standards (e.g.'X'
). See MetainferentialTableauxStandard.standard_variablesbar (bool, optional) – Whether the index has a bar on top or not. Defaults to
False
.
Notes
Note that the __init__ method of will automatically turn sets and lists within a standard into standard. Thus, you can write
MetainferentialTableauxStandard([{'1'}, {'1'}])
instead ofMetainferentialTableauxStandard([MetainferentialTableauxStandard({'1'}), MetainferentialTableauxStandard({'1'})])
Examples
>>> from logics.classes.propositional.proof_theories.metainferential_tableaux import MetainferentialTableauxStandard >>> standard = MetainferentialTableauxStandard([[{'1', 'i'}, {'1'}], [{'1', 'i'}, {'1'}]], bar=True) >>> isinstance(standard, MetainferentialTableauxStandard) True >>> isinstance(standard.content[0], MetainferentialTableauxStandard) True >>> standard.content[0].bar # bar status is not inherited to content sub-standards False
- property level¶
Returns the level of a standard
Examples
>>> from logics.classes.propositional.proof_theories.metainferential_tableaux import MetainferentialTableauxStandard >>> standard = MetainferentialTableauxStandard([[{'1', 'i'}, {'1'}], [{'1', 'i'}, {'1'}]]) # TS/ST >>> standard.level 2 >>> standard.content[0].level # TS 1 >>> standard.content[0].content[1].level # S 0
Note that standard variables do not have a level, and will raise
ValueError
if their level is queried>>> MetainferentialTableauxStandard('X').level Traceback (most recent call last): ... ValueError: Variable standard can have any level >>> MetainferentialTableauxStandard(['X', {'1'}]).level Traceback (most recent call last): ... ValueError: Variable standard can have any level
- is_instance_of(idx2, subst_dict=None, return_subst_dict=False)¶
Determines whether a standard is an instance of another standard
A MetainferentialTableauxStandard (self) is considered an instance of another (idx2) iff self and node have the same
bar
status, and one of the following occurs:idx2 is a standard variable (see
MetainferentialTableauxStandard.standard_variables
). The default standard variables are'W', 'X', 'Y', 'Z'
idx2 is a set (i.e. a level-0 standard) and
self.content == idx2.content
idx2 is a 2-list (a level-n>0 standard) and both members of self.content are instances of both members of idx2.content, respectively
Examples
>>> from logics.classes.propositional.proof_theories.metainferential_tableaux import MetainferentialTableauxStandard >>> simple_standard = MetainferentialTableauxStandard({'1', 'i'}, bar=False) # T >>> simple_standard.is_instance_of(MetainferentialTableauxStandard('X')) True >>> simple_standard.is_instance_of(MetainferentialTableauxStandard({'1', 'i'})) True >>> simple_standard.is_instance_of(MetainferentialTableauxStandard({'1'})) False >>> simple_standard.is_instance_of(MetainferentialTableauxStandard(['X', 'Y'])) False
>>> complex_standard = MetainferentialTableauxStandard([{'1', 'i'}, {'1'}], bar=False) # TS >>> complex_standard.is_instance_of(MetainferentialTableauxStandard('X')) True >>> complex_standard.is_instance_of(MetainferentialTableauxStandard(['X', 'Y'])) True >>> complex_standard.is_instance_of(MetainferentialTableauxStandard(['X', 'X'])) False >>> complex_standard.is_instance_of(MetainferentialTableauxStandard([{'1'}, {'1', 'i'}])) False
- class logics.classes.propositional.proof_theories.metainferential_tableaux.MetainferentialTableauxNode(content, index=None, justification=None, parent=None, children=None)¶
Nodes for metainferential tableaux
- Parameters:
content (logics.classes.propositional.Formula or logics.classes.propositional.Inference) – The formula or inference of the node
index (logics.classes.propositional.proof_theories.metainferntial_tableaux.MetainferentialTableauxStandard) – The standard of the node
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).
Notes
This subclasses
logics.classes.propositional.proof_theories.tableaux.TableauxNode
, and overrides a few methods. The functioning is almost identicalExamples
>>> from logics.utils.parsers import classical_parser >>> from logics.instances.propositional.languages import classical_infinite_language as lang >>> from logics.classes.propositional.proof_theories.metainferential_tableaux import ( ... MetainferentialTableauxStandard, MetainferentialTableauxNode >>> ) >>> S = MetainferentialTableauxStandard({'1'}) >>> Sbar = MetainferentialTableauxStandard({'1'}, bar=True) >>> ST = MetainferentialTableauxStandard([{'1'}, {'1', 'i'}]) >>> XY = MetainferentialTableauxStandard(['X', 'Y']) >>> XYbar = MetainferentialTableauxStandard(['X', 'Y'], bar=True) >>> node1 = MetainferentialTableauxNode(classical_parser.parse('p / q'), index=ST) >>> node2 = MetainferentialTableauxNode(classical_parser.parse('p / q'), index=XY) >>> node3 = MetainferentialTableauxNode(classical_parser.parse('p / q'), index=XYbar) >>> node1.is_instance_of(node2, lang) True >>> node1.is_instance_of(node3, lang) False >>> MetainferentialTableauxNode(classical_parser.parse('p'), index=S, parent=node1) >>> MetainferentialTableauxNode(classical_parser.parse('q'), index=S, parent=node1) >>> node1.print_tree(classical_parser) p / q, [{'1'}, {'1', 'i'}] ├── p, {'1'} └── q, {'1'}
Metainferential Tableaux System¶
- class logics.classes.propositional.proof_theories.metainferential_tableaux.MetainferentialTableauxSystem(base_indexes, language, rules, closure_rules, solver=None)¶
Class for metainferential tableaux systems
Takes an extra parameter
base_indexes
, which should be a set. This defines what will be the valid standards. E.g. ifbase_indexes
is{'1', 'i', '0'}
then[{'1', 'i'}, {'1'}]
will be a valid standard but[{'1', 'n'}, {'1'}]
will not.Notes
This subclasses
logics.classes.propositional.proof_theories.tableaux.TableauxSystem
, and overrides a few methods. The functioning is almost identicalAlso note that the
is_correct_tree
method has not been implemented yet for this class.
Instances¶
- logics.instances.propositional.metainferential_tableaux.CL_metainferential_tableaux_system¶
Tableaux system for every metainferential logic, of any level, using the CL (two-valued classical) schema
- logics.instances.propositional.metainferential_tableaux.SK_metainferential_tableaux_system¶
Tableaux system for every metainferential logic, of any level, using the SK (three-valued strong Kleene) schema (see citation needed, examples below)
- logics.instances.propositional.metainferential_tableaux.WK_metainferential_tableaux_system¶
Tableaux system for every metainferential logic, of any level, using the WK (three-valued weak Kleene) schema (see citation needed)
Metainferential Tableaux Solver¶
- class logics.utils.solvers.tableaux.MetainferentialTableauxSolver¶
Solver class for many-valued metainferential systems
The default instance of the class it at
logics.utils.solvers.tableaux.metainferential_tableaux_solver
The
solve
method takes as parameters:inference: a logics.classes.propositional.Inference
tableaux_system: a logics.classes.propositional.proof_theories.tableaux.MetainferentialTableauxSystem
beggining_index: a list or set like
[{'1', 'i'}, {'1'}]
. Note that this is not aMetainferentialTableauxStandard
-those are reserved for tableaux nodes.
Examples
>>> from logics.utils.parsers import classical_parser >>> from logics.instances.propositional.metainferential_tableaux import SK_metainferential_tableaux_system as sk_tableaux >>> from logics.utils.solvers.tableaux import metainferential_tableaux_solver >>> meta_explosion = classical_parser.parse('(/ p ∧ ~p) // (/q)') >>> tree = metainferential_tableaux_solver.solve( ... inference=meta_explosion, ... tableaux_system=sk_tableaux, ... beggining_index=[[{'1', 'i'}, {'1'}], [{'1'}, {'1', 'i'}]] # TS/ST, closed ... ) >>> tree.print_tree(classical_parser) (/ p ∧ ~p) // (/ q), -[[{'1', 'i'}, {'1'}], [{'1'}, {'1', 'i'}]] └── / p ∧ ~p, [{'1', 'i'}, {'1'}] (inf0) └── / q, -[{'1'}, {'1', 'i'}] (inf0) └── p ∧ ~p, {'1'} (inf1) └── q, -{'1', 'i'} (inf0) └── p, {'1'} (R∧1) └── ~p, {'1'} (R∧1) └── q, {'0'} (complement) └── p, {'0'} (R~1) └── p, set() (intersection) >>> sk_tableaux.tree_is_closed(tree) True >>> tree = metainferential_tableaux_solver.solve( ... inference=meta_explosion, ... tableaux_system=sk_tableaux, ... beggining_index=[[{'1'}, {'1', 'i'}], [{'1'}, {'1', 'i'}]], # ST/ST, not closed ... ) >>> tree.print_tree(classical_parser) (/ p ∧ ~p) // (/ q), -[[{'1'}, {'1', 'i'}], [{'1'}, {'1', 'i'}]] └── / p ∧ ~p, [{'1'}, {'1', 'i'}] (inf0) └── / q, -[{'1'}, {'1', 'i'}] (inf0) └── p ∧ ~p, {'1', 'i'} (inf1) └── q, -{'1', 'i'} (inf0) ├── p ∧ ~p, {'1'} (singleton) │ └── q, {'0'} (complement) │ └── p, {'1'} (R∧1) │ └── ~p, {'1'} (R∧1) │ └── p, {'0'} (R~1) │ └── p, set() (intersection) └── p ∧ ~p, {'i'} (singleton) └── q, {'0'} (complement) ├── p, {'1', 'i'} (R∧i) │ └── ~p, {'i'} (R∧i) │ ├── p, {'1'} (singleton) │ │ └── p, {'i'} (R~1) │ │ └── p, set() (intersection) │ └── p, {'i'} (singleton) └── p, {'i'} (R∧i) └── ~p, {'1', 'i'} (R∧i) ├── ~p, {'1'} (singleton) │ └── p, {'0'} (R~1) │ └── p, set() (intersection) └── ~p, {'i'} (singleton) >>> sk_tableaux.tree_is_closed(tree) False