Bug fix for tableaux with multiple versions of 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.3] - 2024-04-17
+### Fixed
+- Bug in tableaux `is_correct_tree` method when multiple version of a rule were given
+
 ## [1.10.2] - 2024-04-17
 ### Added
 - Possibility of having different versions of a rule in tableaux systems

docs/source/conf.py

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

logics/classes/propositional/proof_theories/tableaux.py

@@ -764,37 +764,49 @@ def is_correct_tree(self, tree, inference=None, return_error_list=False, exit_on
             # 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()
+            rules_applicable_but_not_applied = 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
 
+                # If another version of the rule was correctly applied, move on
+                if actual_rule_name in rules_applied_to_node:
+                    continue
+
                 # 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]
                 if applicable:
                     subst_dict = result[1]
+
                     # Get the rule premises
                     rule_prems = [n for n in PreOrderIter(self.rules[rule_name]) if n.justification is None]
+
                     # See if the rule is correctly applied
                     # (rule_prems[-1] contains the last premise AND ITS SUBTREE)
                     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,
-                                                          index=tuple(n.child_index for n in node.path),
-                                                          description=f'Rule {rule_name} was not applied to '
-                                                                      f'node {node._self_string(parser)}'))
-                        if exit_on_first_error:
-                            return False, error_list
+                        # It does not mean the tree is incorrect, maybe another version of the rule has been applied
+                        rules_applicable_but_not_applied.add(actual_rule_name)
                     else:
                         rules_applied_to_node.add(actual_rule_name)
+                        if actual_rule_name in rules_applicable_but_not_applied:
+                            rules_applicable_but_not_applied.remove(actual_rule_name)
                         correctly_derived_nodes |= result3[1]
+                        break  # this assumes that no more than one rule should be applied to each node
+
+            # If after going through every rule you find that some applicable rule was not applied, throw an error
+            if rules_applicable_but_not_applied:
+                if not return_error_list:
+                    return False
+                not_applied_rule_name = next(iter(rules_applicable_but_not_applied))
+                error_list.append(CorrectionError(code=ErrorCode.TBL_RULE_NOT_APPLIED,
+                                                  index=tuple(n.child_index for n in node.path),
+                                                  description=f'Rule {not_applied_rule_name} was not applied to '
+                                                              f'node {node._self_string(parser)}'))
+                if exit_on_first_error:
+                    return False, error_list
 
         # After visiting all nodes, check that all premises and conclusions are present in the tableaux
         if inference is not None:

setup.cfg

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

tests/propositional/test_tableaux.py

@@ -291,49 +291,49 @@ def test_is_correct_tree(self):
     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∧'])
+        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'])
+        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)
+        n2 = TableauxNode(content=Formula(['q']), justification='R∧', parent=n1)
+        TableauxNode(content=Formula(['p']), justification='R∧', parent=n2)
         '''
         p ∧ q
-        └── q
-            └── p
+        └── q (R∧)
+            └── p (R∧)
         '''
         self.assertFalse(classical_tableaux_system.is_correct_tree(n1))
-        self.assertFalse(classical_tableaux_system_modified.is_correct_tree(n1))
+        self.assertTrue(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∨'])
+        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'])
+        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)
+        TableauxNode(content=Formula(['q']), justification='R∨', parent=n1)
+        TableauxNode(content=Formula(['p']), justification='R∨', parent=n1)
         '''
-        p ∧ q
-        ├── q
-        └── p
+        p ∨ q
+        ├── q (R∨)
+        └── p (R∨)
         '''
         self.assertFalse(classical_tableaux_system.is_correct_tree(n1))
-        self.assertFalse(classical_tableaux_system_modified.is_correct_tree(n1))
+        self.assertTrue(classical_tableaux_system_modified.is_correct_tree(n1))
 
     def test_classical_indexed_tableaux(self):
         # Node is closed