Skip to content

Commit 32ce7d9

Browse files
committed
implemented formula evaluation andexample scripts
1 parent 6c766b2 commit 32ce7d9

8 files changed

Lines changed: 346 additions & 24 deletions

File tree

evaluation_function/propositional_logic/__init__.py

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -8,8 +8,8 @@
88
Disjunction,
99
Implication,
1010
Biconditional,
11-
BracketedFormula,
1211
)
12+
from .evaluator import Assignment, FormulaEvaluator
1313

1414
__all__ = [
1515
"Formula",
@@ -21,5 +21,6 @@
2121
"Disjunction",
2222
"Implication",
2323
"Biconditional",
24-
"BracketedFormula",
24+
"Assignment",
25+
"FormulaEvaluator",
2526
]
Lines changed: 53 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,53 @@
1+
from typing import Mapping
2+
from .formula import (
3+
Formula,
4+
Atom,
5+
Truth,
6+
Falsity,
7+
Negation,
8+
Conjunction,
9+
Disjunction,
10+
Implication,
11+
Biconditional,
12+
)
13+
14+
15+
class Assignment:
16+
def __init__(self, assignment: Mapping[Atom, bool]):
17+
self._assignment = dict(assignment)
18+
19+
def get(self, atom: Atom) -> bool:
20+
if atom not in self._assignment:
21+
raise ValueError(f"Atom {atom.name} not found in assignment")
22+
return self._assignment[atom]
23+
24+
def __contains__(self, atom: Atom) -> bool:
25+
return atom in self._assignment
26+
27+
28+
class FormulaEvaluator:
29+
def __init__(self, formula: Formula, assignment: Assignment):
30+
self._formula = formula
31+
self._assignment = assignment
32+
33+
def evaluate(self) -> bool:
34+
return self._evaluate_formula(self._formula)
35+
36+
def _evaluate_formula(self, formula: Formula) -> bool:
37+
if isinstance(formula, Atom):
38+
return self._assignment.get(formula)
39+
if isinstance(formula, Truth):
40+
return True
41+
if isinstance(formula, Falsity):
42+
return False
43+
if isinstance(formula, Negation):
44+
return not self._evaluate_formula(formula.operand)
45+
if isinstance(formula, Conjunction):
46+
return self._evaluate_formula(formula.left) and self._evaluate_formula(formula.right)
47+
if isinstance(formula, Disjunction):
48+
return self._evaluate_formula(formula.left) or self._evaluate_formula(formula.right)
49+
if isinstance(formula, Implication):
50+
return not self._evaluate_formula(formula.left) or self._evaluate_formula(formula.right)
51+
if isinstance(formula, Biconditional):
52+
return self._evaluate_formula(formula.left) == self._evaluate_formula(formula.right)
53+
raise TypeError(f"Unknown formula type: {type(formula)}")

evaluation_function/propositional_logic/formula.py

Lines changed: 0 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -149,25 +149,3 @@ def _operator_symbol(self) -> str:
149149
class Biconditional(BinaryOperator):
150150
def _operator_symbol(self) -> str:
151151
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})"

examples/__init__.py

Whitespace-only changes.

examples/basic_usage.py

Lines changed: 55 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,55 @@
1+
from evaluation_function.propositional_logic import (
2+
Atom,
3+
Truth,
4+
Falsity,
5+
Negation,
6+
Conjunction,
7+
Disjunction,
8+
Implication,
9+
Biconditional,
10+
Assignment,
11+
FormulaEvaluator,
12+
)
13+
14+
15+
def main():
16+
p = Atom("p")
17+
q = Atom("q")
18+
19+
assignment = Assignment({p: True, q: False})
20+
21+
print("=== Basic Formula Evaluation ===")
22+
print(f"p = {p}")
23+
print(f"q = {q}")
24+
print(f"Assignment: p=True, q=False")
25+
print()
26+
27+
formulas = [
28+
("p", p),
29+
("q", q),
30+
("⊤", Truth()),
31+
("⊥", Falsity()),
32+
("¬p", Negation(p)),
33+
("p ∧ q", Conjunction(p, q)),
34+
("p ∨ q", Disjunction(p, q)),
35+
("p → q", Implication(p, q)),
36+
("p ↔ q", Biconditional(p, q)),
37+
]
38+
39+
for name, formula in formulas:
40+
evaluator = FormulaEvaluator(formula, assignment)
41+
result = evaluator.evaluate()
42+
print(f"{name:15} = {result}")
43+
44+
print()
45+
print("=== Different Assignment ===")
46+
assignment2 = Assignment({p: True, q: True})
47+
48+
for name, formula in formulas:
49+
evaluator = FormulaEvaluator(formula, assignment2)
50+
result = evaluator.evaluate()
51+
print(f"{name:15} = {result}")
52+
53+
54+
if __name__ == "__main__":
55+
main()

examples/complex_formulas.py

Lines changed: 76 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,76 @@
1+
from evaluation_function.propositional_logic import (
2+
Atom,
3+
Negation,
4+
Conjunction,
5+
Disjunction,
6+
Implication,
7+
Biconditional,
8+
Assignment,
9+
FormulaEvaluator,
10+
)
11+
12+
13+
def main():
14+
p = Atom("p")
15+
q = Atom("q")
16+
r = Atom("r")
17+
18+
assignment = Assignment({p: True, q: False, r: True})
19+
20+
print("=== Complex Nested Formulas ===")
21+
print(f"Assignment: p=True, q=False, r=True")
22+
print()
23+
24+
complex_formulas = [
25+
(
26+
"¬(p ∧ q)",
27+
Negation(Conjunction(p, q))
28+
),
29+
(
30+
"(p → q) → r",
31+
Implication(Implication(p, q), r)
32+
),
33+
(
34+
"p ∧ (q ∨ r)",
35+
Conjunction(p, Disjunction(q, r))
36+
),
37+
(
38+
"(p ∧ q) ∨ (p ∧ r)",
39+
Disjunction(
40+
Conjunction(p, q),
41+
Conjunction(p, r)
42+
)
43+
),
44+
(
45+
"p ↔ (q ↔ r)",
46+
Biconditional(p, Biconditional(q, r))
47+
),
48+
(
49+
"((p → q) ∧ (q → r)) → (p → r)",
50+
Implication(
51+
Conjunction(
52+
Implication(p, q),
53+
Implication(q, r)
54+
),
55+
Implication(p, r)
56+
)
57+
),
58+
(
59+
"¬(p ∨ q) ↔ (¬p ∧ ¬q)",
60+
Biconditional(
61+
Negation(Disjunction(p, q)),
62+
Conjunction(Negation(p), Negation(q))
63+
)
64+
),
65+
]
66+
67+
for name, formula in complex_formulas:
68+
evaluator = FormulaEvaluator(formula, assignment)
69+
result = evaluator.evaluate()
70+
print(f"{name:35} = {result}")
71+
print(f" Formula: {formula}")
72+
print()
73+
74+
75+
if __name__ == "__main__":
76+
main()

examples/formula_equivalence.py

Lines changed: 101 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,101 @@
1+
from itertools import product
2+
from evaluation_function.propositional_logic import (
3+
Atom,
4+
Negation,
5+
Conjunction,
6+
Disjunction,
7+
Implication,
8+
Biconditional,
9+
Assignment,
10+
FormulaEvaluator,
11+
)
12+
13+
14+
def get_atoms(formula):
15+
atoms = set()
16+
17+
if isinstance(formula, Atom):
18+
atoms.add(formula)
19+
elif hasattr(formula, "operand"):
20+
atoms.update(get_atoms(formula.operand))
21+
elif hasattr(formula, "left") and hasattr(formula, "right"):
22+
atoms.update(get_atoms(formula.left))
23+
atoms.update(get_atoms(formula.right))
24+
elif hasattr(formula, "formula"):
25+
atoms.update(get_atoms(formula.formula))
26+
27+
return atoms
28+
29+
30+
def are_equivalent(formula1, formula2):
31+
atoms1 = get_atoms(formula1)
32+
atoms2 = get_atoms(formula2)
33+
all_atoms = list(atoms1 | atoms2)
34+
35+
for assignment_values in product([False, True], repeat=len(all_atoms)):
36+
assignment_dict = {atom: val for atom, val in zip(all_atoms, assignment_values)}
37+
assignment = Assignment(assignment_dict)
38+
39+
evaluator1 = FormulaEvaluator(formula1, assignment)
40+
evaluator2 = FormulaEvaluator(formula2, assignment)
41+
42+
result1 = evaluator1.evaluate()
43+
result2 = evaluator2.evaluate()
44+
45+
if result1 != result2:
46+
return False
47+
48+
return True
49+
50+
51+
def main():
52+
p = Atom("p")
53+
q = Atom("q")
54+
55+
print("=== Formula Equivalence Checking ===")
56+
print()
57+
58+
equivalence_tests = [
59+
(
60+
"p → q",
61+
"¬p ∨ q",
62+
Implication(p, q),
63+
Disjunction(Negation(p), q)
64+
),
65+
(
66+
"p ↔ q",
67+
"(p → q) ∧ (q → p)",
68+
Biconditional(p, q),
69+
Conjunction(Implication(p, q), Implication(q, p))
70+
),
71+
(
72+
"¬(p ∧ q)",
73+
"¬p ∨ ¬q",
74+
Negation(Conjunction(p, q)),
75+
Disjunction(Negation(p), Negation(q))
76+
),
77+
(
78+
"¬(p ∨ q)",
79+
"¬p ∧ ¬q",
80+
Negation(Disjunction(p, q)),
81+
Conjunction(Negation(p), Negation(q))
82+
),
83+
(
84+
"p ∧ q",
85+
"q ∧ p",
86+
Conjunction(p, q),
87+
Conjunction(q, p)
88+
),
89+
]
90+
91+
for name1, name2, formula1, formula2 in equivalence_tests:
92+
equivalent = are_equivalent(formula1, formula2)
93+
status = "✓ EQUIVALENT" if equivalent else "✗ NOT EQUIVALENT"
94+
print(f"{name1:20}{name2:25} {status}")
95+
print(f" Formula 1: {formula1}")
96+
print(f" Formula 2: {formula2}")
97+
print()
98+
99+
100+
if __name__ == "__main__":
101+
main()

examples/truth_table.py

Lines changed: 58 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,58 @@
1+
from itertools import product
2+
from evaluation_function.propositional_logic import (
3+
Atom,
4+
Negation,
5+
Conjunction,
6+
Disjunction,
7+
Implication,
8+
Biconditional,
9+
Assignment,
10+
FormulaEvaluator,
11+
)
12+
13+
14+
def generate_truth_table(atoms, formula):
15+
print(f"=== Truth Table for: {formula} ===")
16+
print()
17+
18+
header = " | ".join([atom.name for atom in atoms] + ["Result"])
19+
separator = "-" * len(header)
20+
print(header)
21+
print(separator)
22+
23+
for assignment_values in product([False, True], repeat=len(atoms)):
24+
assignment_dict = {atom: val for atom, val in zip(atoms, assignment_values)}
25+
assignment = Assignment(assignment_dict)
26+
evaluator = FormulaEvaluator(formula, assignment)
27+
result = evaluator.evaluate()
28+
29+
row = " | ".join([str(val) for val in assignment_values] + [str(result)])
30+
print(row)
31+
32+
print()
33+
34+
35+
def main():
36+
p = Atom("p")
37+
q = Atom("q")
38+
39+
formulas = [
40+
("p ∧ q", Conjunction(p, q)),
41+
("p ∨ q", Disjunction(p, q)),
42+
("p → q", Implication(p, q)),
43+
("p ↔ q", Biconditional(p, q)),
44+
("¬(p ∧ q)", Negation(Conjunction(p, q))),
45+
("(p → q) ∧ (q → p)", Conjunction(Implication(p, q), Implication(q, p))),
46+
]
47+
48+
for name, formula in formulas:
49+
generate_truth_table([p, q], formula)
50+
51+
print("\n=== Three Variable Example ===")
52+
r = Atom("r")
53+
formula = Implication(Conjunction(p, q), r)
54+
generate_truth_table([p, q, r], formula)
55+
56+
57+
if __name__ == "__main__":
58+
main()

0 commit comments

Comments
 (0)