Add monadic predicate tableaux feature

logics/classes/predicate/proof_theories/tableaux.py

@@ -0,0 +1,366 @@
+"""
+Tableaux implementation using AnyTree. See https://anytree.readthedocs.io/en/latest/
+In AnyTree, the root node effectively represents the entire tableaux tree.
+"""
+import string
+from copy import copy, deepcopy
+from anytree import NodeMixin, RenderTree, PreOrderIter, LevelOrderIter
+
+from logics.classes.predicate import PredicateFormula
+from logics.classes.errors import ErrorCode, CorrectionError
+
+
+class TableauxNode(NodeMixin):
+    """
+    Represents a single node in a predicate logic tableaux tree.
+    Inherits from AnyTree's NodeMixin to support tree-based operations.
+    """
+
+    separator = '==>'
+
+    def __init__(self, content, index=None, justification=None, parent=None, children=None, order=None):
+        self.content = content
+        self.index = index
+        self.justification = justification
+        self.parent = parent
+
+        if children:
+            self.children = children
+
+        # 'order' determines the priority of rule application for this node.
+        # Lower values are processed first (e.g., Alpha rules before Gamma).
+        if order:
+            self.order = order
+        else:
+            self.ordering_node()
+
+    def ordering_node(self):
+        """
+        Assigns an execution priority (order) to the node based on its main logical operator.
+        Follows standard heuristic: Non-branching (Alpha) -> Delta -> Gamma -> Branching (Beta).
+        """
+        main_operator = self.find_operator(self.content)
+        match main_operator:
+            case '∧' | '~∨' | '~→':  # Alpha Rules (Non-branching, propositional)
+                self.order = 1
+            case '∃' | '~∀':         # Delta Rules (Existential instantiation)
+                self.order = 2 
+            case '∀' | '~∃':         # Gamma Rules (Universal instantiation)
+                self.order = 3
+            case '∨' | '~∧' | '→':   # Beta Rules (Branching, propositional)
+                self.order = 4
+            case _:
+                self.order = 5       # Atomic formulas or others
+
+    def find_operator(self, content):
+        """
+        Identifies the primary logical operator or the negated operator (e.g., '~∀').
+        """
+        if content[0] == '~':
+            # Check if it is a negated complex formula
+            if content[1][0] in {'∀', '∧', '∨', '∃', '→'}:
+                return '~%s' % content[1][0]
+
+        return content[0]
+
+    def is_instance_of(self, node, language, subst_dict=None, return_subst_dict=False):
+        """
+        Checks if the current node's content and metadata match a schematic node (a rule template).
+        """
+        if subst_dict is None:
+            subst_dict = dict()
+
+        # Validate justification (rule name) matches if provided
+        if node.justification is not None and self.justification != node.justification:
+            return (False, subst_dict) if return_subst_dict else False
+
+        # Validate indices match if provided
+        if node.index is not None:
+            index_instance, subst_dict = self.index_is_instance_of(node.index, subst_dict, return_subst_dict=True)
+            if not index_instance:
+                return (False, subst_dict) if return_subst_dict else False
+
+        # Delegate formula matching to the PredicateFormula instance
+        instance, subst_dict = self.content_is_instance_of(node.content, language, subst_dict, return_subst_dict=True)
+        if not return_subst_dict:
+            return instance
+        return instance, subst_dict
+
+    def content_is_instance_of(self, content2, language, subst_dict, return_subst_dict):
+        return self.content.is_instance_of(content2, language, subst_dict, return_subst_dict)
+
+    def index_is_instance_of(self, idx2, subst_dict, return_subst_dict):
+        if return_subst_dict:
+            return self.index == idx2, subst_dict
+        return self.index == idx2
+
+    def instantiate(self, language, subst_dict, instantiate_children=True, first_iteration=True):
+        """
+        Creates a concrete TableauxNode from a schematic one by applying a substitution dictionary.
+        """
+        if first_iteration or instantiate_children:
+            self_content_substitution = self.content.instantiate(language, subst_dict)
+        else:
+            self_content_substitution = deepcopy(self.content)
+
+        new_tableaux = self.__class__(
+            content=self_content_substitution, 
+            index=self.index,
+            justification=self.justification
+        )
+
+        # Recursively instantiate all child nodes in the rule template
+        for child_node in self.children:
+            new_child = child_node.instantiate(
+                language, subst_dict, instantiate_children, first_iteration=False
+            )
+            new_child.parent = new_tableaux
+
+        return new_tableaux
+
+    @property
+    def child_index(self):
+        if self.is_root:
+            return 0
+        return self.parent.children.index(self)
+
+    def _self_string(self, parser=None):
+        """Internal helper for string representation."""
+        s = f'{self.content}' if not parser else f'{parser.unparse(self.content)}'
+        if self.index is not None:
+            s += f', {self.index}'
+        if self.justification is not None:
+            s += f' ({self.justification})'
+        return s
+
+    def __repr__(self):
+        return self._self_string()
+
+    def print_path(self, parser=None):
+        """Prints the logical steps from root to the current node."""
+        print(f' {self.separator} '.join([node._self_string(parser) for node in self.path]))
+
+    def print_tree(self, parser=None):
+        """Prints the entire tree structure in a readable format."""
+        for pre, _, node in RenderTree(self):
+            print(pre + node._self_string(parser))
+
+
+# ----------------------------------------------------------------------------------------------------------------------
+
+class TableauxSystem:
+    """
+    Manages the rules and closure conditions for a predicate logic tableaux system.
+    """
+
+    # Complex quantifier conflicts require exhaustive branch checking
+    fast_node_is_closed_enabled = False  
+
+    def __init__(self, language, rules, closure_rules, solver=None):
+        self.language = language
+        self.rules = rules
+        self.closure_rules = closure_rules
+        self.solver = solver
+        self.ground_terms = []   # Existing individual constants in the context
+        self.new_constants = []  # Specifically generated witnesses for Delta rules
+
+    def add_ground_term(self, term):
+        """Registers a new term to the available pool for Gamma rule expansions."""
+        if term not in self.ground_terms:
+            self.ground_terms.append(term)
+
+    def generate_new_constant(self):
+        """
+        Generates a fresh individual constant not currently used in the language or tree.
+        Used primarily as a witness for existential instantiation (Delta Rule).
+        """
+        # Try single letters first
+        for letter in string.ascii_lowercase:
+            if (letter not in self.new_constants and 
+                letter not in self.language.individual_constants):
+                self.new_constants.append(letter)
+                return letter
+
+        # Fallback to alphanumeric constants if single letters are exhausted
+        for i in range(1, 100):
+            for letter in string.ascii_lowercase:
+                new_const = f"{letter}{i}"
+                if (new_const not in self.new_constants and 
+                    new_const not in self.language.individual_constants):
+                    self.new_constants.append(new_const)
+                    return new_const
+
+        raise ValueError("Constant generation limit reached.")
+
+    def node_is_closed(self, node):
+        """
+        Checks if the branch ending at 'node' contains a contradiction.
+        A contradiction occurs if A and ~A appear on the same path.
+        """
+        path = node.path
+
+        # Search for direct contradictions: Formula A and its negation ~A
+        for i in range(len(path)):
+            for j in range(i+1, len(path)):
+                formula1 = path[i].content
+                formula2 = path[j].content
+
+                # Check if formula1 is the negation of formula2
+                if (formula1.main_symbol == '~' and formula1[1] == formula2 and
+                    path[i].index == path[j].index):
+                    return True
+
+                # Check if formula2 is the negation of formula1
+                if (formula2.main_symbol == '~' and formula2[1] == formula1 and
+                    path[i].index == path[j].index):
+                    return True
+
+        # Check against specifically defined closure rules (e.g., identity or modal rules)
+        for closure_rule in self.closure_rules:
+            for i in range(len(path)):
+                for j in range(i+1, len(path)):
+                    if self._nodes_match_closure_rule(path[i], path[j], closure_rule):
+                        return True
+
+        return False
+
+    def _nodes_match_closure_rule(self, node1, node2, closure_rule):
+        """Checks if a pair of nodes matches a specific closure rule template."""
+        instance1, subst_dict = node1.is_instance_of(
+            closure_rule[0], self.language, return_subst_dict=True
+        )
+        if instance1:
+            if node2.is_instance_of(closure_rule[1], self.language, subst_dict):
+                return True
+
+        # Check reverse order
+        instance3, subst_dict = node2.is_instance_of(
+            closure_rule[0], self.language, return_subst_dict=True
+        )
+        if instance3:
+            if node1.is_instance_of(closure_rule[1], self.language, subst_dict):
+                return True
+
+        return False
+
+    def tree_is_closed(self, node):
+        """
+        A tree is closed if and only if every single leaf (branch) is closed.
+        """
+        parent = node.parent
+        node.parent = None  # Isolate the node for independent analysis
+
+        for leaf in node.leaves:
+            if not self.node_is_closed(leaf):
+                node.parent = parent
+                return False
+
+        node.parent = parent
+        return True
+
+    def rule_is_applicable(self, node, rule_name, return_subst_dict=False):
+        """
+        Determines if a specific rule can be applied to a node.
+        Includes verification of quantifier-specific conditions.
+        """
+        rule = self.rules[rule_name]
+        rule_prems = [n for n in PreOrderIter(rule) if n.justification is None]
+
+        # Match current node against the main premise of the rule
+        instance, subst_dict = node.is_instance_of(
+            rule_prems[-1], self.language, return_subst_dict=True
+        )
+
+        if not instance:
+            return (False, subst_dict) if return_subst_dict else False
+
+        # Apply special checks for quantifier-related rules
+        if rule_name in ['R∀', 'R∃', 'R~∀', 'R~∃']:
+            if not self._quantifier_rule_additional_conditions(node, rule_name, subst_dict):
+                return (False, subst_dict) if return_subst_dict else False
+
+        # Verify any additional premises required by the rule higher up the branch
+        remaining_prems = rule_prems[:-1]
+        if remaining_prems:
+            first_elem = True
+            for node2 in node.iter_path_reverse():
+                if first_elem:
+                    first_elem = False
+                    continue
+
+                subst_dict2 = deepcopy(subst_dict)
+                instance2, subst_dict2 = node2.is_instance_of(
+                    remaining_prems[-1], self.language, subst_dict2, return_subst_dict=True
+                )
+
+                if instance2:
+                    subst_dict.update(subst_dict2)
+                    del remaining_prems[-1]
+                    if not remaining_prems:
+                        break
+
+        if not remaining_prems:
+            return (True, subst_dict) if return_subst_dict else True
+
+        return (False, subst_dict) if return_subst_dict else False
+
+    def _quantifier_rule_additional_conditions(self, node, rule_name, subst_dict):
+        """
+        Prevents infinite loops by checking if a quantifier rule has already 
+        exhausted its allowed applications on a particular node.
+        """
+        # Flag-based tracking for quantifier processing status
+        if rule_name == 'R∀': 
+            return not getattr(node, "_done_R∀", False)
+
+        elif rule_name == 'R∃':
+            return not getattr(node, "_done_R∃", False)
+
+        elif rule_name == 'R~∀':
+            return not getattr(node, "_done_R~∀", False)
+
+        elif rule_name == 'R~∃':
+            return not getattr(node, "_done_R~∃", False)
+
+        return True
+
+
+class ConstructiveTreeSystem(TableauxSystem):
+    """
+    Automates the construction of a tableaux tree to verify if a formula is well-formed.
+    In this system, a branch closes if it reaches an atomic formula that is well-formed.
+    """
+    fast_node_is_closed_enabled = False
+
+    def __init__(self, language, solver=None):
+        self.language = language
+        self.closure_rules = []
+        self.solver = solver
+        self.rules = dict()
+
+        # Build structural decomposition rules based on the language's constant arity
+        for constant in language.constant_arity_dict:
+            arity = language.constant_arity_dict[constant]
+            initial_formula = [constant]
+            initial_formula.extend([[f'A{num+1}'] for num in range(arity)])
+            initial_formula = PredicateFormula(initial_formula)
+            initial_node = TableauxNode(content=initial_formula, justification=None)
+
+            # Create child templates for each argument of the operator
+            for ar in range(arity):
+                TableauxNode(content=PredicateFormula([f'A{ar+1}']), justification=f'R{constant}', parent=initial_node)
+            self.rules[f'R{constant}'] = initial_node
+
+    def node_is_closed(self, node):
+        """
+        A node in a constructive tree is closed if its content is a well-formed atomic formula.
+        """
+        if node.content.is_atomic and self.language.is_well_formed(node.content):
+            return True
+        return False
+
+    def is_well_formed(self, formula):
+        """
+        Determines if a formula is well-formed by checking if its constructive tree closes.
+        """
+        return self.is_valid(formula)