matmod/logic.py

142 lines
4.1 KiB
Python
Raw Normal View History

2024-05-29 13:50:20 -04:00
from typing import Optional, Set, Tuple
2024-04-08 23:59:21 -04:00
from functools import lru_cache
class Operation:
def __init__(self, symbol: str, arity: int):
self.symbol = symbol
self.arity = arity
self.hashed_value = hash(self.symbol) + self.arity
def immutable(self, name, value):
raise Exception("Operations are immutable")
self.__setattr__ = immutable
2024-05-29 13:50:20 -04:00
2024-04-08 23:59:21 -04:00
def __hash__(self):
return self.hashed_value
2024-05-29 13:50:20 -04:00
2024-04-08 23:59:21 -04:00
def __call__(self, *args):
# Ensure the arity is met
assert len(args) == self.arity
# Ensure every argument is a term
for t in args:
assert isinstance(t, Term)
return OpTerm(self, args)
2024-05-29 13:50:20 -04:00
2024-04-08 23:59:21 -04:00
class Term:
def __init__(self):
pass
def __lt__(self, y):
return Inequation(self, y)
class PropositionalVariable(Term):
def __init__(self, name):
self.name = name
self.hashed_value = hash(self.name)
def immutable(self, name, value):
raise Exception("Propositional variables are immutable")
self.__setattr__ = immutable
2024-05-29 13:50:20 -04:00
2024-04-08 23:59:21 -04:00
def __hash__(self):
return self.hashed_value
2024-04-15 00:08:00 -04:00
2024-04-08 23:59:21 -04:00
def __str__(self):
return self.name
class OpTerm(Term):
def __init__(self, operation: Operation, arguments):
assert len(arguments) == operation.arity
self.operation = operation
self.arguments = arguments
self.hashed_value = hash(self.operation) * hash(self.arguments)
def immutable(self, name, value):
raise Exception("Terms are immutable")
self.__setattr__ = immutable
2024-05-29 13:50:20 -04:00
2024-04-08 23:59:21 -04:00
def __hash__(self):
return self.hashed_value
2024-05-29 13:50:20 -04:00
2024-04-08 23:59:21 -04:00
def __str__(self):
arg_strs = [str(a) for a in self.arguments]
return self.operation.symbol + "(" + ",".join(arg_strs) + ")"
2024-04-15 00:08:00 -04:00
# Standard operators
2024-04-08 23:59:21 -04:00
Negation = Operation("¬", 1)
Conjunction = Operation("", 2)
Disjunction = Operation("", 2)
Implication = Operation("", 2)
class Inequation:
def __init__(self, antecedant : Term, consequent: Term):
self.antecedant = antecedant
self.consequent = consequent
def __str__(self):
2024-05-29 13:50:20 -04:00
return str(self.antecedant) + "" + str(self.consequent)
2024-04-08 23:59:21 -04:00
class InequalityRule:
def __init__(self, premises : Set[Inequation], conclusion: Inequation):
self.premises = premises
self.conclusion = conclusion
2024-05-29 13:50:20 -04:00
2024-04-08 23:59:21 -04:00
def __str__(self):
str_premises = [str(p) for p in self.premises]
str_premises2 = "{" + ",".join(str_premises) + "}"
return str(str_premises2) + "=>" + str(self.conclusion)
class Rule:
def __init__(self, premises : Set[Term], conclusion: Term):
self.premises = premises
self.conclusion = conclusion
2024-05-29 13:50:20 -04:00
2024-04-08 23:59:21 -04:00
def __str__(self):
str_premises = [str(p) for p in self.premises]
str_premises2 = "{" + ",".join(str_premises) + "}"
return str(str_premises2) + "=>" + str(self.conclusion)
class Logic:
2024-05-29 13:50:20 -04:00
def __init__(self,
operations: Set[Operation], rules: Set[Rule],
name: Optional[str] = None):
2024-04-08 23:59:21 -04:00
self.operations = operations
self.rules = rules
2024-05-29 13:50:20 -04:00
self.name = str(abs(hash((
frozenset(operations),
frozenset(rules)
))))[:5] if name is None else name
2024-04-08 23:59:21 -04:00
2024-04-15 00:08:00 -04:00
def get_prop_var_from_term(t: Term) -> Set[PropositionalVariable]:
2024-04-08 23:59:21 -04:00
if isinstance(t, PropositionalVariable):
return {t,}
2024-04-15 00:08:00 -04:00
result: Set[PropositionalVariable] = set()
2024-04-08 23:59:21 -04:00
for arg in t.arguments:
result |= get_prop_var_from_term(arg)
2024-05-29 13:50:20 -04:00
2024-04-08 23:59:21 -04:00
return result
2024-04-15 00:08:00 -04:00
@lru_cache
def get_propostional_variables(rules: Tuple[Rule]) -> Set[PropositionalVariable]:
vars: Set[PropositionalVariable] = set()
2024-04-08 23:59:21 -04:00
for rule in rules:
# Get all vars in premises
for premise in rule.premises:
vars |= get_prop_var_from_term(premise)
2024-05-29 13:50:20 -04:00
2024-04-08 23:59:21 -04:00
# Get vars in conclusion
vars |= get_prop_var_from_term(rule.conclusion)
2024-04-15 00:08:00 -04:00
return vars
def get_operations_from_term(t: Term) -> Set[Operation]:
if isinstance(t, PropositionalVariable):
return set()
2024-05-29 13:50:20 -04:00
2024-04-15 00:08:00 -04:00
result: Set[Operation] = {t.operation,}
for arg in t.arguments:
result |= get_operations_from_term(arg)
2024-05-29 13:50:20 -04:00
2024-04-15 00:08:00 -04:00
return result