شناسایی رابط اصلی فرمول و مولفه‌های آن در منطق گزاره ها

نتایج تحلیل فرمول ورودی:

کد پایتون الگوریتم شناسایی اصلی و موئلفه‌های آن در زیر آمده است. این کد را می‌توانید با کلیک کردن کپی کنید.

یافتن رابط اصلی و موئلفه‌های (زیرفرمول‌های) اصلی آن در یک فرمول منطقی

class LogicalFormulaMnConnectiveVer2:
    # معرفی رابط‌هاو مشخص کردن رابطهای دوتایی
    CONNECTIVES = {'⊃', '∧', '∨', '≡', '~'}
    BINARY_CONNECTIVES = {'⊃', '∧', '∨', '≡'}

    # نگاشت رابط‌های ورودی به رابط‌های رایج منطقی
    CONNECTIVE_MAPPING = {
        '~': '~',
        '>': '⊃',
        '&': '∧',
        '|': '∨',
        '=': '≡' 
    }

    @staticmethod
    def _standardize_connectives(formula: str) -> str:
        """
          جایگزینی نمادهای تایپی رابط‌ها به رابط‌های منطقی 
                                  آنطور که در ساختار زیر
                    CONNECTIVE_MAPPING
                                           .تعریف شده‌اند
        """        for old_char, new_char in LogicalFormulaMnConnectiveVer2.CONNECTIVE_MAPPING.items():
            formula = formula.replace(old_char, new_char)
        return formula

    @staticmethod
    def _remove_outermost_parentheses(formula: str) -> str:
        """
        ،حذف بیرونی ترین زوج پرانتزها
         زوج پانتزهایی که کل فرمول را 
                    .را محصور کرده‌اند
          خواهیم دید که این کار ضروری 
                                 .است
        """
                
        formula = formula.strip()

        if len(formula) >= 2 and formula[0] == '(' and formula[-1] == ')':
            depth = 0
            match_found = True
            """
            آغاز چرخه برای وارسی وجود زوج پرانتزهایی
                       .که کل فرمول را محصور کرده‌اند 
            """
            for i in range(len(formula) - 1):
                char = formula[i]
                if char == '(':
                    depth += 1
                elif char == ')':
                    depth -= 1
                """
                اگر نمایان‌گر عمق صفر باشد آنگاه زوج پرانتز 
                                محصور کننده کل فرمول نیست
                       ‌دقت کنید که بیرونی‌ترین زوج پرانتزها 
                                               .حذف شده‌اند
                """
                if i > 0 and depth == 0:
                    match_found = False
                    break
            
            if match_found:
                return formula[1:-1].strip()
        
        return formula

    @staticmethod
    def _is_binary_operator(char: str) -> bool:
        """
        اگر نویسه یک رابط دوتایی است
        """
        return char in LogicalFormulaMnConnectiveVer2.BINARY_CONNECTIVES

    @staticmethod
    def _get_precedence(op: str) -> int:
        """
        .این تابع سطح اولویت یک رابط را بر می‌گرداند
               دقت کنید که مقدار کمتر عددی به معنای
                                  .اولویت بیشتر است
          این به تعیین رابط اصلی در فرمول‌های پیچیده
                                         .کمک می‌کند
        """
        if op == '≡':
            return 0  
        elif op == '⊃':
            return 1  
        elif op == '∨':
            return 2  
        elif op == '∧':
            return 3  
        else:
            return 4  # پیشفرض برای رابط‌های یکتایی

    @staticmethod
    def find_main_connective_and_subformulas(formula: str) -> tuple[str | None, int, str | None, str | None]:
        """
        تابع اصلی برای یافتن رابط اصلی و موئلفه‌های آن 


        """
        # حذف بیرونی‌ترین زوج پرانتز‌ها
        
        formula = LogicalFormulaMnConnectiveVer2._remove_outermost_parentheses(formula)
        # نگاشت رابط‌های فرمول ورودی
        formula = LogicalFormulaMnConnectiveVer2._standardize_connectives(formula)

        depth = 0  # معرفی متغیر برای نگهداشت عمق
        main_connective = None
        main_position = -1
        lowest_precedence = float('inf')  # آغاز به تقدم بی‌نهایت

        # چرخه برای پویش فرمول ورودب نیسه به نویسه
        for i, char in enumerate(formula):
            if char == '(':
                depth += 1
            elif char == ')':
                depth -= 1
            # اگر عمق صفر است پس یافتی یک رابط دوتایی
            elif depth == 0 and LogicalFormulaMnConnectiveVer2._is_binary_operator(char):
                precedence = LogicalFormulaMnConnectiveVer2._get_precedence(char)
                # در جستجوی رابطی با کمتری اولویت
                # اگر دو رابط اولویت یکسان داشته باشند، رابط در سمت راست‌تر ارجح است
                # (شرکت پذیری ازز راست برای شرطی و دو شرطی )
                if precedence <= lowest_precedence:
                    lowest_precedence = precedence
                    main_connective = char
                    main_position = i
        
        # بعد از چرخه و اگر رابط یافت شده دوتایی است        
        if main_connective is not None:
            # ساختن موئلفه‌های چپ و راست
            left_subformula = formula[0:main_position].strip()
            right_subformula = formula[main_position + 1:].strip()
            return (main_connective, main_position, left_subformula, right_subformula)
        
        # اگر رابط یافت شده دوتایی نیست آیا رابط یافت شده نقی است
        elif formula.startswith('~'):
            # The subformula is everything after the '~'
            negated_subformula = formula[1:].strip()
            return ('~', 0, negated_subformula, None)
        
        # اگر رابط دوتایی و نه رابط نقضی یافت شده است پس فرمول اتمی است 
        else:
            # The formula itself is the atomic proposition
            return (None, -1, formula.strip(), None)

# --------------------------------------
# --- مثال برار کار زدن ---------------
formula1 = "(A ∨ B) ∧ C"
print(f"نتیجه : '{formula1}'")
mc1, pos1, left1, right1 = LogicalFormulaMnConnectiveVer2.find_main_connective_and_subformulas(formula1)
print(f"  رابط اصلی: {mc1}")
print(f"مولفه سمتت چپ: '{left1}'")
print(f"موئلفه سمت راست: '{right1}'\n")
print("---------------------------------")