Skip to content

Commit 6c766b2

Browse files
committed
implemented representation classes for prop logic
1 parent 4ca2d38 commit 6c766b2

2 files changed

Lines changed: 198 additions & 0 deletions

File tree

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
from .formula import (
2+
Formula,
3+
Atom,
4+
Truth,
5+
Falsity,
6+
Negation,
7+
Conjunction,
8+
Disjunction,
9+
Implication,
10+
Biconditional,
11+
BracketedFormula,
12+
)
13+
14+
__all__ = [
15+
"Formula",
16+
"Atom",
17+
"Truth",
18+
"Falsity",
19+
"Negation",
20+
"Conjunction",
21+
"Disjunction",
22+
"Implication",
23+
"Biconditional",
24+
"BracketedFormula",
25+
]
Lines changed: 173 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,173 @@
1+
from abc import ABC, abstractmethod
2+
from typing import Any
3+
4+
5+
class Formula(ABC):
6+
@abstractmethod
7+
def __eq__(self, other: Any) -> bool:
8+
pass
9+
10+
@abstractmethod
11+
def __hash__(self) -> int:
12+
pass
13+
14+
@abstractmethod
15+
def __repr__(self) -> str:
16+
pass
17+
18+
19+
class Atom(Formula):
20+
def __init__(self, name: str):
21+
if not name:
22+
raise ValueError("Atom name cannot be empty")
23+
self._name = name
24+
25+
@property
26+
def name(self) -> str:
27+
return self._name
28+
29+
def __eq__(self, other: Any) -> bool:
30+
if not isinstance(other, Atom):
31+
return False
32+
return self._name == other._name
33+
34+
def __hash__(self) -> int:
35+
return hash(("Atom", self._name))
36+
37+
def __repr__(self) -> str:
38+
return f"Atom('{self._name}')"
39+
40+
41+
class Truth(Formula):
42+
_instance = None
43+
44+
def __new__(cls):
45+
if cls._instance is None:
46+
cls._instance = super().__new__(cls)
47+
return cls._instance
48+
49+
def __eq__(self, other: Any) -> bool:
50+
return isinstance(other, Truth)
51+
52+
def __hash__(self) -> int:
53+
return hash("Truth")
54+
55+
def __repr__(self) -> str:
56+
return "⊤"
57+
58+
59+
class Falsity(Formula):
60+
_instance = None
61+
62+
def __new__(cls):
63+
if cls._instance is None:
64+
cls._instance = super().__new__(cls)
65+
return cls._instance
66+
67+
def __eq__(self, other: Any) -> bool:
68+
return isinstance(other, Falsity)
69+
70+
def __hash__(self) -> int:
71+
return hash("Falsity")
72+
73+
def __repr__(self) -> str:
74+
return "⊥"
75+
76+
77+
class UnaryOperator(Formula):
78+
def __init__(self, operand: Formula):
79+
if not isinstance(operand, Formula):
80+
raise TypeError("Operand must be a Formula")
81+
self._operand = operand
82+
83+
@property
84+
def operand(self) -> Formula:
85+
return self._operand
86+
87+
def __eq__(self, other: Any) -> bool:
88+
if not isinstance(other, type(self)):
89+
return False
90+
return self._operand == other._operand
91+
92+
def __hash__(self) -> int:
93+
return hash((type(self).__name__, self._operand))
94+
95+
96+
class Negation(UnaryOperator):
97+
def __repr__(self) -> str:
98+
return f"¬{self._operand}"
99+
100+
101+
class BinaryOperator(Formula):
102+
def __init__(self, left: Formula, right: Formula):
103+
if not isinstance(left, Formula):
104+
raise TypeError("Left operand must be a Formula")
105+
if not isinstance(right, Formula):
106+
raise TypeError("Right operand must be a Formula")
107+
self._left = left
108+
self._right = right
109+
110+
@property
111+
def left(self) -> Formula:
112+
return self._left
113+
114+
@property
115+
def right(self) -> Formula:
116+
return self._right
117+
118+
def __eq__(self, other: Any) -> bool:
119+
if not isinstance(other, type(self)):
120+
return False
121+
return self._left == other._left and self._right == other._right
122+
123+
def __hash__(self) -> int:
124+
return hash((type(self).__name__, self._left, self._right))
125+
126+
@abstractmethod
127+
def _operator_symbol(self) -> str:
128+
pass
129+
130+
def __repr__(self) -> str:
131+
return f"({self._left} {self._operator_symbol()} {self._right})"
132+
133+
134+
class Conjunction(BinaryOperator):
135+
def _operator_symbol(self) -> str:
136+
return "∧"
137+
138+
139+
class Disjunction(BinaryOperator):
140+
def _operator_symbol(self) -> str:
141+
return "∨"
142+
143+
144+
class Implication(BinaryOperator):
145+
def _operator_symbol(self) -> str:
146+
return "→"
147+
148+
149+
class Biconditional(BinaryOperator):
150+
def _operator_symbol(self) -> str:
151+
return "↔"
152+
153+
154+
class BracketedFormula(Formula):
155+
def __init__(self, formula: Formula):
156+
if not isinstance(formula, Formula):
157+
raise TypeError("Formula must be a Formula instance")
158+
self._formula = formula
159+
160+
@property
161+
def formula(self) -> Formula:
162+
return self._formula
163+
164+
def __eq__(self, other: Any) -> bool:
165+
if not isinstance(other, BracketedFormula):
166+
return False
167+
return self._formula == other._formula
168+
169+
def __hash__(self) -> int:
170+
return hash(("BracketedFormula", self._formula))
171+
172+
def __repr__(self) -> str:
173+
return f"({self._formula})"

0 commit comments

Comments
 (0)