Initial commit

.gitignore

@@ -0,0 +1,2 @@
+__pycache__
+.vscode

R.py

@@ -0,0 +1,124 @@
+"""
+Modeling the logic R
+"""
+from logic import (
+    PropositionalVariable,
+    Rule,
+    Logic,
+    Implication,
+    Conjunction,
+    Negation,
+    Disjunction,
+    Rule,
+)
+from model import Model, ModelFunction, ModelValue
+from generate_model import generate_model
+
+
+# ===================================================
+
+# Defining the logic of R
+
+x = PropositionalVariable("x")
+y = PropositionalVariable("y")
+z = PropositionalVariable("z")
+
+
+implication_rules = {
+    Rule({}, Implication(x, x)),
+    Rule({Implication(x, y), Implication(y,  z)}, Implication(x, z)),
+    Rule({}, Implication(Implication(x, Implication(x, y)), Implication(x, y))),
+    Rule({}, Implication(Implication(x, Implication(y, z)), Implication(y, Implication(x, z)))),
+    Rule({}, Implication(Implication(x, y), Implication(Implication(z, x), Implication(z, y)))),
+    Rule({}, Implication(Implication(x, y), Implication(Implication(y, z), Implication(x, z)))),
+    Rule({Implication(x, y), x}, y)
+}
+
+negation_rules = {
+    Rule({}, Implication(Negation(Negation(x)), x)),
+    Rule({}, Implication(x, Negation(Negation(x)))),
+    Rule({Implication(x, y)}, Implication(Negation(y), Negation(x))),
+    Rule({}, Implication(Implication(x, y), Implication(Negation(y), Negation(x))))
+}
+
+conjunction_rules = {
+    Rule({y, z}, Conjunction(y, z)),
+    Rule({}, Implication(Conjunction(x, y), x)),
+    Rule({}, Implication(Conjunction(x, y), y)),
+    Rule({}, Implication(Conjunction(Implication(x, y), Implication(x, z)), Implication(x, Conjunction(y, z))))
+}
+
+disjunction_rules = {
+    Rule({}, Implication(x, Disjunction(x, y))),
+    Rule({}, Implication(y, Disjunction(x, y))),
+    Rule({}, Implication(Conjunction(Implication(x, z), Implication(y, z)),  Implication(Disjunction(x, y), z))),
+    Rule({}, Implication(Conjunction(x, Disjunction(y, z)), Disjunction(Conjunction(x, y), Conjunction(x, z))))
+}
+
+logic_rules = implication_rules | negation_rules | conjunction_rules | disjunction_rules
+
+operations = {Negation, Conjunction, Disjunction, Implication}
+
+R_logic = Logic(operations, logic_rules)
+
+# ===============================
+
+# Example Model of R
+
+
+a0 = ModelValue("a0")
+a1 = ModelValue("a1")
+
+carrier_set = {a0, a1}
+
+mnegation = ModelFunction({
+    a0: a1,
+    a1: a0
+})
+
+mimplication = ModelFunction({
+    (a0, a0): a1,
+    (a0, a1): a1,
+    (a1, a0): a0,
+    (a1, a1): a1
+})
+
+mconjunction = ModelFunction({
+    (a0, a0): a0,
+    (a0, a1): a0,
+    (a1, a0): a0,
+    (a1, a1): a1  
+})
+
+mdisjunction = ModelFunction({
+    (a0, a0): a0,
+    (a0, a1): a1,
+    (a1, a0): a1,
+    (a1, a1): a1  
+})
+
+
+designated_values = {a1}
+
+logical_operations = {
+    mnegation, mimplication, mconjunction, mdisjunction
+}
+R_model_2 = Model(carrier_set, logical_operations, designated_values)
+
+interpretation = {
+    Negation: mnegation,
+    Conjunction: mconjunction,
+    Disjunction: mdisjunction,
+    Implication: mimplication
+}
+
+
+# =================================
+
+# Generate models of R of a given size
+
+model_size = 2
+satisfiable_models = generate_model(R_logic, model_size)
+
+print(f"There are {len(satisfiable_models)} satisfiable models of element length {model_size}")
+

generate_model.py

@@ -0,0 +1,63 @@
+"""
+File which generates all the models
+"""
+from logic import Logic
+from model import ModelValue, Model, satisfiable, ModelFunction
+from itertools import combinations, chain, product
+
+def possible_designations(iterable):
+    """Powerset without the empty and complete set"""
+    s = list(iterable)
+    return chain.from_iterable(combinations(s, r) for r in range(1, len(s)))
+
+def possible_functions(operation, carrier_set):
+    arity = operation.arity
+
+    inputs = list(product(*(carrier_set for _ in range(arity))))
+    possible_outputs = product(*(carrier_set for _ in range(len(inputs))))
+    for outputs in possible_outputs:
+        assert len(inputs) == len(outputs)
+        new_function = dict()
+        for input, output in zip(inputs, outputs):
+            new_function[input] = output
+        
+        yield ModelFunction(new_function, operation.symbol)
+
+def possible_interpretations(logic, carrier_set):
+    operations = []
+    model_functions = []
+
+    for operation in logic.operations:
+        operations.append(operation)
+        model_functions.append(possible_functions(operation, carrier_set))
+
+    functions_choice = product(*model_functions)
+    for functions in functions_choice:
+        assert len(operations) == len(functions)
+        interpretation = dict()
+        for operation, function in zip(operations, functions):
+            interpretation[operation] = function
+        yield interpretation
+
+def generate_model(logic: Logic, number_elements: int):
+    carrier_set = {
+        ModelValue("a" + str(i)) for i in range(number_elements)
+    }
+
+    possible_designated_values = possible_designations(carrier_set)
+    possible_interps = possible_interpretations(logic, carrier_set)
+
+    satisfied_models = []
+    checked = 0
+    for designated_values, interpretation in product(possible_designated_values, possible_interps):
+        checked += 1
+        designated_values = set(designated_values)
+        
+        model = Model(carrier_set, set(interpretation.values()), designated_values)
+        if satisfiable(logic, model, interpretation):
+            satisfied_models.append(model)
+            print(model)
+        
+    print("Checked", checked)
+    
+    return satisfied_models

logic.py

@@ -0,0 +1,128 @@
+from typing import Any, Set
+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
+    
+    def __hash__(self):
+        return self.hashed_value
+    
+    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)
+        
+
+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
+    
+    def __hash__(self):
+        return self.hashed_value
+    # def __setattr__(self, name: str, value: Any):
+        # raise Exception("Propositional variables are immutable")
+    def __str__(self):
+        return self.name
+
+# def PropTerm(Term):
+#     def __init__(self, v: PropositionalVariable):
+#         self.v = v
+
+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
+    
+    def __hash__(self):
+        return self.hashed_value
+    
+    def __str__(self):
+        arg_strs = [str(a) for a in self.arguments]
+        return self.operation.symbol + "(" + ",".join(arg_strs) + ")"
+
+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):
+        return str(self.antecedant) + "≤" + str(self.consequent) 
+
+class InequalityRule:
+    def __init__(self, premises : Set[Inequation], conclusion: Inequation):
+        self.premises = premises
+        self.conclusion = conclusion
+    
+    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
+    
+    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:
+    def __init__(self, operations: Set[Operation], rules: Set[Rule]):
+        self.operations = operations
+        self.rules = rules
+
+
+def get_prop_var_from_term(t: Term):
+    if isinstance(t, PropositionalVariable):
+        return {t,}
+
+    result = set()
+    for arg in t.arguments:
+        result |= get_prop_var_from_term(arg)
+    
+    return result
+
+def get_propostional_variables(rules):
+    vars = set()
+
+    for rule in rules:
+        # Get all vars in premises
+        for premise in rule.premises:
+            vars |= get_prop_var_from_term(premise)
+    
+        # Get vars in conclusion
+        vars |= get_prop_var_from_term(rule.conclusion)
+
+    return vars

model.py

@@ -0,0 +1,130 @@
+"""
+Defining what it means to be a model
+"""
+from logic import (
+PropositionalVariable, get_propostional_variables, Logic, Term,
+Operation
+) 
+from typing import Set, List, Dict
+from itertools import product
+
+__all__ = ['ModelValue', 'ModelFunction', 'Model']
+
+
+def set_to_str(x):
+    return "{" + ", ".join((str(xi) for xi in x)) + "}"
+
+class ModelValue:
+    def __init__(self, name):
+        self.name = name
+        self.hashed_value = hash(self.name)
+        def immutable(self, name, value):
+            raise Exception("Model values are immutable")
+        self.__setattr__ = immutable
+    def __str__(self):
+        return self.name
+    def __hash__(self):
+        return self.hashed_value
+    def __eq__(self, other):
+        return isinstance(other, ModelValue) and self.name == other.name
+
+
+class ModelFunction:
+    def __init__(self, mapping, operation_name = ""):
+        self.operation_name = operation_name
+
+        # Correct input to always be a tuple
+        corrected_mapping = dict()
+        for k, v in mapping.items():
+            if isinstance(k, tuple):
+                corrected_mapping[k] = v
+            elif isinstance(k, list):
+                corrected_mapping[tuple(k)] = v
+            else: # Assume it's atomic
+                corrected_mapping[(k,)] = v
+        
+        self.mapping = corrected_mapping
+    
+    def __str__(self):
+        str_dict = dict()
+        for k, v in self.mapping.items():
+            inputstr = "(" + ", ".join(str(ki) for ki in k) + ")"
+            str_dict[inputstr] = str(v)
+        return str(str_dict)
+
+    def __call__(self, *args):
+        return self.mapping[args]
+    
+    # def __eq__(self, other):
+    #     return isinstance(other, ModelFunction) and self.name == other.name and self.arity == other.arity
+
+class Model:
+    def __init__(
+            self,
+            carrier_set: Set[ModelValue],
+            logical_operations: Set[ModelFunction],
+            designated_values: Set[ModelValue]
+    ):
+        assert designated_values <= carrier_set
+        self.carrier_set = carrier_set
+        self.logical_operations = logical_operations
+        self.designated_values = designated_values
+    
+    def __str__(self):
+        result = f"""Carrier Set: {set_to_str(self.carrier_set)}
+Designated Values: {set_to_str(self.designated_values)}
+"""
+        for function in self.logical_operations:
+            result += f"{str(function)}\n"
+        
+        return result
+
+
+def evaluate_term(t: Term, f: Dict[PropositionalVariable, ModelValue], interpretation: Dict[Operation, ModelFunction]):
+    if isinstance(t, PropositionalVariable):
+        return f[t]
+
+    model_function = interpretation[t.operation]
+    model_arguments = []
+    for logic_arg in t.arguments:
+        model_arg = evaluate_term(logic_arg, f, interpretation)
+        model_arguments.append(model_arg)
+    
+    return model_function(*model_arguments)
+
+def all_model_valuations(
+        pvars: Set[PropositionalVariable],
+        mvalues: Set[ModelValue]):
+    
+    pvars = list(pvars)
+    possible_valuations = [mvalues for _ in pvars]
+    all_possible_values = product(*possible_valuations)
+
+    for valuation in all_possible_values:
+        mapping = dict()
+        assert len(pvars) == len(valuation)
+        for pvar, value in zip(pvars, valuation):
+            mapping[pvar] = value
+        yield mapping
+    
+
+def satisfiable(logic: Logic, model: Model, interpretation: Dict[Operation, ModelFunction]):
+    pvars = get_propostional_variables(logic.rules)
+    mappings = all_model_valuations(pvars, model.carrier_set)
+
+    for mapping in mappings:
+        for rule in logic.rules:
+            premise_met = True
+            for premise in rule.premises:
+                t = evaluate_term(premise, mapping, interpretation)
+                if t not in model.designated_values:
+                    premise_met = False
+                    break
+            if not premise_met:
+                continue
+            
+            t = evaluate_term(rule.conclusion, mapping, interpretation)
+            if t not in model.designated_values:
+                return False
+    
+    return True