[Python] The logic of multi-operations [closed]

I am writing a program that checks whether a formula is closed in multioperations or not. And the code for each formula gives me one answer.: The formula is not closed (contradictory).

from typing import List, Tuple
import re
import uuid

class Term:
def __init__(self, symbol: str, subterms: List['Term'] = None):
self.symbol = symbol
self.subterms = tuple(subterms) if subterms else tuple() # Используем кортеж вместо списка

def __repr__(self):
if not self.subterms:
return self.symbol
return f"{self.symbol}({', '.join(map(str, self.subterms))})"

def __eq__(self, other):
return (
isinstance(other, Term) and
self.symbol == other.symbol and
self.subterms == other.subterms
)

def __hash__(self):
return hash((self.symbol, self.subterms)) # Хэшируем кортеж

class Formula:
def __init__(self, left: Term = None, right: Term = None,
connective: str = None, subformulas: List['Formula'] = None):
self.left = left
self.right = right
self.connective = connective
self.subformulas = tuple(subformulas) if subformulas else tuple() # Кортеж

def __eq__(self, other):
return (
isinstance(other, Formula) and
self.connective == other.connective and
self.subformulas == other.subformulas and
self.left == other.left and
self.right == other.right
)

def __hash__(self):
return hash((
self.connective,
self.left,
self.right,
self.subformulas
))

class MarkedFormula:
def __init__(self, formula: Formula, relation: str, alpha: float):
self.formula = formula
self.relation = relation
self.alpha = alpha

def __eq__(self, other):
return (
isinstance(other, MarkedFormula) and
self.formula == other.formula and
self.relation == other.relation and
abs(self.alpha - other.alpha) < 1e-9
)

def __hash__(self):
return hash((self.formula, self.relation, self.alpha))

# --------------------------------------------
# Парсер формул (расширенный)
# --------------------------------------------
class FormulaParser:
@staticmethod
def parse_term(s: str) -> Term:
s = s.strip()
if '(' not in s:
return Term(s)

symbol, rest = s.split('(', 1)
subterms = []
buffer = []
depth = 0

for c in rest.rstrip(')'):
if c == '(':
depth += 1
elif c == ')':
depth -= 1
if c == ',' and depth == 0:
subterms.append(FormulaParser.parse_term(''.join(buffer).strip()))
buffer = []
continue
buffer.append(c)

if buffer:
subterms.append(FormulaParser.parse_term(''.join(buffer).strip()))

return Term(symbol.strip(), subterms)

@staticmethod
def parse_formula(s: str) -> Formula:
s = s.strip().replace(' ', '')

# Обработка отрицания
if s.startswith('¬'):
return Formula(subformulas=[FormulaParser.parse_formula(s[1:])], connective='¬')

# Обработка скобок (только если вся формула в скобках)
if s.startswith('(') and s.endswith(')'):
# Проверяем, что закрывающая скобка соответствует открывающей
depth = 1
for i in range(1, len(s)-1):
if s == '(':
depth += 1
elif s == ')':
depth -= 1
if depth == 0:
break
else:
# Если все скобки закрыты, парсим внутреннюю часть
return FormulaParser.parse_formula(s[1:-1])

# Порядок важен: сначала проверяем связки с более низким приоритетом
for conn in ['⊆', '→', '∨', '&']:
try:
parts = FormulaParser.split_formula(s, conn)
if conn == '⊆':
return Formula(
left=FormulaParser.parse_term(parts[0]),
right=FormulaParser.parse_term(parts[1]),
connective='⊆'
)
else:
return Formula(
subformulas=[
FormulaParser.parse_formula(parts[0]),
FormulaParser.parse_formula(parts[1])
],
connective=conn
)
except ValueError:
continue

# Если не нашли связок, пытаемся распознать как терм
try:
term = FormulaParser.parse_term(s)
return Formula(left=term) # Условно, если требуется
except:
raise ValueError(f"Invalid formula: {s}")

@staticmethod
def split_formula(s: str, connector: str) -> Tuple[str, str]:
depth = 0
i = 0
connector_len = len(connector)
while i <= len(s) - connector_len:
if s == '(':
depth += 1
elif s == ')':
depth -= 1
elif depth == 0 and s[i:i+connector_len] == connector:
left = s[:i]
right = s[i+connector_len:]
return left.strip(), right.strip()
i += 1
raise ValueError(f"Failed to split by {connector} in {s}")

@staticmethod
def parse_marked(s: str) -> MarkedFormula:
match = re.match(r"(.+?)(<=|>=|<|>)(\d*\.?\d+)", s.replace(' ', ''))
if not match:
raise ValueError(f"Invalid marked formula: {s}")
formula_part = match.group(1)
relation = match.group(2)
alpha = float(match.group(3))
formula = FormulaParser.parse_formula(formula_part)
return MarkedFormula(formula, relation, alpha)
# --------------------------------------------
# Правила вывода (5 групп)
# --------------------------------------------
class InferenceRule:
def apply(self, mf: MarkedFormula) -> List[List[MarkedFormula]]:
return []


class Group1Rule(InferenceRule):
"""Правила для отношений ⊆ с порогами"""

def apply(self, mf: MarkedFormula):
if mf.formula.connective == '⊆':
if mf.relation == '>':
if mf.alpha > 0:
return [[MarkedFormula(Formula(mf.formula.right, mf.formula.left, '⊆'), '>', 0)]]
elif mf.relation == '<':
if mf.alpha < 1:
return [[MarkedFormula(Formula(mf.formula.right, mf.formula.left, '⊆'), '<', 1)]]
return []


class Group2Rule(InferenceRule):
"""Правила для логических связок"""

def apply(self, mf: MarkedFormula):
if mf.formula.connective == '&':
if mf.relation in ('>', '>='):
return [[
MarkedFormula(mf.formula.subformulas[0], mf.relation, mf.alpha),
MarkedFormula(mf.formula.subformulas[1], mf.relation, mf.alpha)
]]
elif mf.relation in ('<', '<='):
return [
[MarkedFormula(mf.formula.subformulas[0], mf.relation, mf.alpha)],
[MarkedFormula(mf.formula.subformulas[1], mf.relation, mf.alpha)]
]

elif mf.formula.connective == '∨':
if mf.relation in ('>', '>='):
return [
[MarkedFormula(mf.formula.subformulas[0], mf.relation, mf.alpha)],
[MarkedFormula(mf.formula.subformulas[1], mf.relation, mf.alpha)]
]
elif mf.relation in ('<', '<='):
return [[
MarkedFormula(mf.formula.subformulas[0], mf.relation, mf.alpha),
MarkedFormula(mf.formula.subformulas[1], mf.relation, mf.alpha)
]]

elif mf.formula.connective == '→':
if mf.relation in ('>', '>='):
return [[
MarkedFormula(mf.formula.subformulas[0], '<=' if mf.relation == '>' else '<', 1 - mf.alpha),
MarkedFormula(mf.formula.subformulas[1], mf.relation, mf.alpha)
]]
return []


class Group3Rule(InferenceRule):
"""Правила для отрицаний"""

def apply(self, mf: MarkedFormula):
if mf.formula.connective == '¬':
new_rel = {'>': '<=', '>=': '<', '<': '>=', '<=': '>'}.get(mf.relation, mf.relation)
return [[MarkedFormula(mf.formula.subformulas[0], new_rel, 1 - mf.alpha)]]
return []


class Group4Rule(InferenceRule):
"""Правила транзитивности с ограничением по существующим термам"""

def apply(self, mf: MarkedFormula):
if (
mf.formula.connective == '⊆'
and mf.relation in ('>', '>=')
and not self._contains_placeholder(mf.formula)
and self._has_existing_terms(mf) # Новая проверка
):
unique_id = uuid.uuid4().hex[:6]
new_term = Term(f"X_{unique_id}")
return [[
MarkedFormula(Formula(mf.formula.left, new_term, '⊆'), mf.relation, mf.alpha),
MarkedFormula(Formula(new_term, mf.formula.right, '⊆'), mf.relation, mf.alpha)
]]
return []

def _contains_placeholder(self, formula: Formula) -> bool:
"""Проверяет, содержит ли формула плейсхолдеры (например, терм X)"""

def check_term(term: Term) -> bool:
return 'X_' in term.symbol # Проверяем наличие плейсхолдера в терме

# Проверяем и левую, и правую части формулы
return check_term(formula.left) or check_term(formula.right)

def _has_existing_terms(self, mf: MarkedFormula) -> bool:
"""Проверяет, есть ли в формуле термы из исходного запроса"""
original_terms = {'A', 'B', 'C'} # Пример для теста транзитивности

def check_term(term: Term):
return term.symbol in original_terms or any(check_term(t) for t in term.subterms)

return check_term(mf.formula.left) or check_term(mf.formula.right)


class Group5Rule(InferenceRule):
"""Специальные правила для термов"""

def apply(self, mf: MarkedFormula):
if (mf.formula.connective == '⊆' and
mf.formula.left == mf.formula.right and
mf.relation in ('<', '<=') and
mf.alpha >= 1):
return [[]] # Закрытие ветки
return []


# --------------------------------------------
# Система вывода с проверкой замкнутости
# --------------------------------------------
class TableauxSystem:
def __init__(self, max_depth=10):
self.rules = [
Group1Rule(),
Group2Rule(),
Group3Rule(),
Group4Rule(),
Group5Rule()
]
self.max_depth = max_depth # Максимальная глубина ветки

def build_table(self, root: MarkedFormula) -> bool:
branches = [[root]]
step = 0

while branches and step < self.max_depth:
current_branch = branches.pop()

if self._is_closed(current_branch):
continue

if self._is_saturated(current_branch):
return False

new_branches = self._apply_rules(current_branch)
branches.extend(new_branches)
step += 1

return False # Если достигнут лимит шагов

def _is_closed(self, branch: List[MarkedFormula]) -> bool:
formulas = set()
for mf in branch:
formula_key = (mf.formula, mf.relation)
inverse_rel = {'<': '>=', '>': '<=', '<=': '>', '>=': '<'}.get(mf.relation)
inverse_key = (mf.formula, inverse_rel)

# Проверка на противоречия
if inverse_key in formulas:
return True

formulas.add(formula_key)

# Дополнительная проверка на противоречие для одинаковых формул с различными знаками отношений
if (mf.relation in ('<', '<=') and mf.alpha >= 1) or (mf.relation in ('>', '>=') and mf.alpha <= 0):
return True

# Обработка специального случая для (A ⊆ A) < 1
if mf.formula.left == mf.formula.right and mf.relation in ('<', '<=') and mf.alpha >= 1:
return True

return False

def _is_saturated(self, branch: List[MarkedFormula]) -> bool:
"""Проверяет, насыщена ли ветка, то есть не может быть расширена дальше"""
# Например, можно считать ветку насыщенной, если она не содержит
# новых элементов для применения правил вывода.
return all(self._has_no_applicable_rules(mf) for mf in branch)

def _has_no_applicable_rules(self, mf: MarkedFormula) -> bool:
"""Проверяет, нет ли применимых правил вывода для данной формулы"""
for rule in self.rules:
if rule.apply(mf):
return False
return True

def _apply_rules(self, branch: List[MarkedFormula]) -> List[List[MarkedFormula]]:
"""Применяет правила вывода к ветке и возвращает новые ветви"""
new_branches = []
for mf in branch:
for rule in self.rules:
new_branches.extend(rule.apply(mf))
return new_branches


# --------------------------------------------
# Тестирование сложных примеров
# --------------------------------------------
def is_valid_formula(user_input):
""" Проверяет, является ли ввод допустимой формулой. """
# Разрешённые символы: отрицание, логические связки, подмножество, скобки, переменные, числа и вероятность
pattern = r'^[¬∧∨⊆()A-Z0-9\s&|>.\-]+$'

# Проверяем, что строка содержит только допустимые символы
if not re.fullmatch(pattern, user_input):
return False

# Проверяем, что нет запрещённых сочетаний
if "⊆ >" in user_input or user_input.count('(') != user_input.count(')'):
return False

return True


def main():
print("Введите формулы. Для завершения ввода введите 'exit'.")
while True:
user_input = input("Введите формулу: ").strip()
if user_input.lower() == 'exit':
break

if not is_valid_formula(user_input):
print("Ошибка: некорректный ввод формулы.")
continue # Пропускаем обработку

try:
# Парсим входную формулу в объект MarkedFormula
marked_formula = FormulaParser.parse_marked(user_input)

# Создаем систему вывода
system = TableauxSystem(max_depth=10)

# Строим таблицу для формулы
result = system.build_table(marked_formula)

if result:
print("Формула замкнута (непротиворечива).")
else:
print("Формула не замкнута (противоречива).")

except ValueError as e:
print(f"Ошибка: {e}")


if __name__ == "__main__":
main()


Here is an example:

Введите формулу: (A ⊆ B & B ⊆ C) > 0.7 Формула не замкнута (противоречива).

As I understand it, the answer is wrong, it should be closed.

Or is my code correct?

Continue reading...