Tableaux systems with multiple versions of a rule

CHANGELOG.md

@@ -5,6 +5,10 @@ All notable changes to this project will be documented in this file.
 The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
 and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).
 
+## [1.10.2] - 2024-04-17
+### Added
+- Possibility of having different versions of a rule in tableaux systems
+
 ## [1.10.1] - 2024-03-23
 ### Fixed
 - Bug in the biconditional rule of classical tableaux system

docs/source/conf.py

@@ -22,7 +22,7 @@
 author = 'Ariel Jonathan Roffe'
 
 # The full version, including alpha/beta/rc tags
-release = '1.10.1'
+release = '1.10.2'
 
 
 # -- General configuration ---------------------------------------------------

logics/classes/propositional/proof_theories/tableaux.py

@@ -392,7 +392,10 @@ class TableauxSystem:
 
     Notes
     -----
-    There are predefined instances of this class for known systems, see below.
+    - 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.
     """
     # Assumes a branch is closed if a node and its negation (with the same index) are present in a branch:
     fast_node_is_closed_enabled = True
@@ -599,6 +602,7 @@ def rule_is_applicable(self, node, rule_name, return_subst_dict=False):
         """
         rule = self.rules[rule_name]
         rule_prems = [n for n in PreOrderIter(rule) if n.justification is None]  # Rule premises
+        # Check if the node is an instance of the last premise of the rule
         instance, subst_dict = node.is_instance_of(rule_prems[-1], self.language, return_subst_dict=True)
         if instance:
             # If it is, check that the rest of the premises of the rule (if there are any) are present
@@ -759,7 +763,11 @@ def is_correct_tree(self, tree, inference=None, return_error_list=False, exit_on
             # Check if a rule applies to the node and is correctly applied in the tree
             # e.g. if the node is a conjunction, see that both conjuncts are below in the tree, and save both conjuncts
             # as correctly derived nodes
+            rules_applied_to_node = set()
             for rule_name in self.rules:
+                # Some rules have names like R∧_1 and R∧_2 but are actually different versions of the same rule
+                actual_rule_name = rule_name[:-2] if rule_name[-2] == '_' and rule_name[-1].isdigit() else rule_name
+
                 # For each rule, see if the current node is an instance of the LAST premise of the rule
                 result = self.rule_is_applicable(node, rule_name, return_subst_dict=True)
                 applicable = result[0]
@@ -772,6 +780,10 @@ def is_correct_tree(self, tree, inference=None, return_error_list=False, exit_on
                     result3 = self._is_correctly_applied(node, rule_prems[-1], correctly_derived_nodes, subst_dict)
                     correct = result3[0]
                     if not correct:
+                        # If another version of the rule was correctly applied, do not count it as an error
+                        if actual_rule_name in rules_applied_to_node:
+                            continue
+
                         if not return_error_list:
                             return False
                         error_list.append(CorrectionError(code=ErrorCode.TBL_RULE_NOT_APPLIED,
@@ -781,6 +793,7 @@ def is_correct_tree(self, tree, inference=None, return_error_list=False, exit_on
                         if exit_on_first_error:
                             return False, error_list
                     else:
+                        rules_applied_to_node.add(actual_rule_name)
                         correctly_derived_nodes |= result3[1]
 
         # After visiting all nodes, check that all premises and conclusions are present in the tableaux

setup.cfg

@@ -1,6 +1,6 @@
 [metadata]
 name = logics
-version = 1.10.1
+version = 1.10.2
 author = Ariel Jonathan Roffé
 author_email = arielroffe@filo.uba.ar
 url = https://github.com/ariroffe/logics

tests/propositional/test_tableaux.py

@@ -1,4 +1,5 @@
 import unittest
+from copy import deepcopy
 
 from logics.classes.propositional.proof_theories.tableaux import TableauxNode, ConstructiveTreeSystem
 from logics.classes.propositional import Formula, Inference
@@ -287,6 +288,53 @@ def test_is_correct_tree(self):
 
         # More extensive tests (with the random argument generator) are made in tests/utils/test_tableaux_solver
 
+    def test_is_correct_tree_multiple_versions_of_rule(self):
+        # Build a classical system but with two conjunction rules, that swap A and B in the conclusions
+        classical_tableaux_system_modified = deepcopy(classical_tableaux_system)
+        classical_tableaux_system_modified.rules['R∧1'] = deepcopy(classical_tableaux_system_modified.rules['R∧'])
+        classical_tableaux_system_modified.rules['R∧2'] = deepcopy(classical_tableaux_system_modified.rules['R∧'])
+        del classical_tableaux_system_modified.rules['R∧']
+        classical_tableaux_system_modified.rules['R∧2'].children[0].content = Formula(['B'])
+        classical_tableaux_system_modified.rules['R∧2'].children[0].children[0].content = Formula(['A'])
+        """
+        ['∧', ['A'], ['B']]
+        └── ['B'] (R∧)
+            └── ['A'] (R∧)
+        """
+
+        n1 = TableauxNode(content=Formula(['∧', ['p'], ['q']]))
+        n2 = TableauxNode(content=Formula(['q']), parent=n1)
+        n3 = TableauxNode(content=Formula(['p']), parent=n2)
+        '''
+        p ∧ q
+        └── q
+            └── p
+        '''
+        self.assertFalse(classical_tableaux_system.is_correct_tree(n1))
+        self.assertFalse(classical_tableaux_system_modified.is_correct_tree(n1))
+
+        # Try the same with disjunction, inverting the leaves
+        classical_tableaux_system_modified.rules['R∨1'] = deepcopy(classical_tableaux_system_modified.rules['R∨'])
+        classical_tableaux_system_modified.rules['R∨2'] = deepcopy(classical_tableaux_system_modified.rules['R∨'])
+        del classical_tableaux_system_modified.rules['R∨']
+        classical_tableaux_system_modified.rules['R∨2'].children[0].content = Formula(['B'])
+        classical_tableaux_system_modified.rules['R∨2'].children[1].content = Formula(['A'])
+        """
+        ['∨', ['A'], ['B']]
+        ├── ['B'] (R∨)
+        └── ['A'] (R∨)
+        """
+        n1 = TableauxNode(content=Formula(['∨', ['p'], ['q']]))
+        n2 = TableauxNode(content=Formula(['q']), parent=n1)
+        n3 = TableauxNode(content=Formula(['p']), parent=n1)
+        '''
+        p ∧ q
+        ├── q
+        └── p
+        '''
+        self.assertFalse(classical_tableaux_system.is_correct_tree(n1))
+        self.assertFalse(classical_tableaux_system_modified.is_correct_tree(n1))
+
     def test_classical_indexed_tableaux(self):
         # Node is closed
         n1 = TableauxNode(content=Formula(['p']), index=1)