diff --git a/README.md b/README.md index b9bac56..9ce66d2 100644 --- a/README.md +++ b/README.md @@ -95,7 +95,7 @@ pip install mathesis ## Roadmap -- [ ] Add tests +- [ ] Add tests (WIP) - [ ] Hilbert systems - [x] Natural deduction - [ ] Boolean algebra diff --git a/mathesis/forms.py b/mathesis/forms.py index d3e5a47..3e39f2a 100644 --- a/mathesis/forms.py +++ b/mathesis/forms.py @@ -46,7 +46,7 @@ def free_terms(self): return self.terms def replace_term(self, replaced_term, replacing_term): - fml = self + fml = self.clone() fml.terms = [ replacing_term if term == replaced_term else term for term in self.terms ] @@ -132,7 +132,7 @@ def free_terms(self): return self.sub.free_terms def replace_term(self, replaced_term, replacing_term): - fml = self + fml = self.clone() fml.sub = self.sub.replace_term(replaced_term, replacing_term) return fml @@ -187,9 +187,9 @@ def free_terms(self): def replace_term(self, replaced_term, replacing_term): # fml = copy(self) - fml = self + fml = self.clone() subs = [] - for subfml in self.subs: + for subfml in deepcopy(self.subs): subs.append(subfml.replace_term(replaced_term, replacing_term)) fml.subs = subs return fml @@ -205,7 +205,7 @@ def latex(self): def __str__(self) -> str: # print(self.subs) # return f"{self.connective}".join(map(lambda x: f"({x})", self.subs)) - return f"{self.connective}".join( + return f" {self.connective} ".join( map( lambda x: f"({x})" if isinstance(x, Binary) else f"{x}", self.subs, diff --git a/mathesis/semantics/truth_table/base.py b/mathesis/semantics/truth_table/base.py index deca59c..d75e23d 100644 --- a/mathesis/semantics/truth_table/base.py +++ b/mathesis/semantics/truth_table/base.py @@ -4,7 +4,7 @@ from itertools import product from anytree import NodeMixin, PostOrderIter -from prettytable import PLAIN_COLUMNS, PrettyTable +from prettytable import TableStyle, PrettyTable from mathesis import forms @@ -47,7 +47,7 @@ def to_table(self): return table - def to_string(self, style=PLAIN_COLUMNS): + def to_string(self, style=TableStyle.PLAIN_COLUMNS): table = self.to_table() table.set_style(style) return str(table) @@ -405,7 +405,7 @@ def to_table(self): return table - def to_string(self, style=PLAIN_COLUMNS): + def to_string(self, style=TableStyle.PLAIN_COLUMNS): table = self.to_table() table.set_style(style) return str(table) diff --git a/tests/test_forms.py b/tests/test_forms.py new file mode 100644 index 0000000..f7491ca --- /dev/null +++ b/tests/test_forms.py @@ -0,0 +1,130 @@ +from mathesis.forms import ( + Formula, + Atom, + Top, + Bottom, + Negation, + Disjunction, + Conjunction, + Conditional, + Universal, + Particular +) + + +# ⊤ ∨ (¬Q ∨ R) +propositional_formula_1 = Disjunction( + Top(), + Disjunction( + Negation(Atom("Q")), + Atom("R") + ) +) + +# (P ∧ ¬P) → ⊥ +propositional_formula_2 = Conditional( + Conjunction( + Atom("P"), + Negation(Atom("P")) + ), + Bottom() +) + +# ∀x(P(x) → (Q(x) ∨ R(x))) +quantified_formula_1 = Universal( + "x", + Conditional( + Atom("P", terms=["x"]), + Disjunction( + Atom("Q", terms=["x"]), + Atom("R", terms=["x"]) + ) + ) +) + +# ∃y(¬Q(y) ∧ ¬R(a, b, y)) +quantified_formula_2 = Particular( + "y", + Conjunction( + Negation(Atom("Q", terms=["y"])), + Negation(Atom("R", terms=["a", "b", "y"])) + ) +) + + +def test_repr(): + assert repr(propositional_formula_1) == "Disj[Top, Disj[Neg[Atom[Q]], Atom[R]]]" + assert repr(propositional_formula_2) == "Cond[Conj[Atom[P], Neg[Atom[P]]], Bottom]" + assert repr(quantified_formula_1) == "Forall[Cond[Atom[P(x)], Disj[Atom[Q(x)], Atom[R(x)]]]]" + assert repr(quantified_formula_2) == "Exists[Conj[Neg[Atom[Q(y)]], Neg[Atom[R(a, b, y)]]]]" + + +def test_str(): + assert str(propositional_formula_1) == "⊤ ∨ (¬Q ∨ R)" + assert str(propositional_formula_2) == "(P ∧ ¬P) → ⊥" + assert str(quantified_formula_1) == "∀x(P(x) → (Q(x) ∨ R(x)))" + assert str(quantified_formula_2) == "∃y(¬Q(y) ∧ ¬R(a, b, y))" + + +def test_latex(): + assert propositional_formula_1.latex() == r"\top \lor (\neg Q \lor R)" + assert propositional_formula_2.latex() == r"(P \land \neg P) \to \bot" + assert quantified_formula_1.latex() == r"\forall x (P(x) \to (Q(x) \lor R(x)))" + assert quantified_formula_2.latex() == r"\exists y (\neg Q(y) \land \neg R(a, b, y))" + + +def test_atoms(): + assert propositional_formula_1.atoms == { + "Q": [Atom("Q")], + "R": [Atom("R")] + } + assert propositional_formula_2.atoms == { + "P": [Atom("P"), Atom("P")] + } + assert quantified_formula_1.atoms == { + "P(x)": [Atom("P", terms=["x"])], + "Q(x)": [Atom("Q", terms=["x"])], + "R(x)": [Atom("R", terms=["x"])] + } + assert quantified_formula_2.atoms == { + "Q(y)": [Atom("Q", terms=["y"])], + "R(a, b, y)": [Atom("R", terms=["a", "b", "y"])] + } + + +def test_atom_symbols(): + assert propositional_formula_1.atom_symbols == ["Q", "R"] + assert propositional_formula_2.atom_symbols == ["P"] + assert quantified_formula_1.atom_symbols == ["P(x)", "Q(x)", "R(x)"] + assert quantified_formula_2.atom_symbols == ["Q(y)", "R(a, b, y)"] + + +def test_equality(): + assert propositional_formula_1 == propositional_formula_1 + assert propositional_formula_2 != propositional_formula_1 + assert propositional_formula_2 != quantified_formula_1 + assert quantified_formula_1 == quantified_formula_1 + assert quantified_formula_2 == quantified_formula_2 + assert quantified_formula_1 != quantified_formula_2 + + +def test_free_terms(): + assert propositional_formula_1.free_terms == [] + assert propositional_formula_2.free_terms == [] + assert quantified_formula_1.free_terms == [] + assert quantified_formula_2.free_terms == ["a", "b"] + + +def test_replace_term(): + assert propositional_formula_1.replace_term("Q", "R") == propositional_formula_1 + assert quantified_formula_1.replace_term("x", "y") == Conditional( + Atom("P", terms=["y"]), + Disjunction( + Atom("Q", terms=["y"]), + Atom("R", terms=["y"]) + ) + ) + assert quantified_formula_2.replace_term("a", "b") == Conjunction( + Negation(Atom("Q", terms=["y"])), + Negation(Atom("R", terms=["b", "b", "y"])) + ) diff --git a/tests/test_grammars.py b/tests/test_grammars.py new file mode 100644 index 0000000..72e1fb9 --- /dev/null +++ b/tests/test_grammars.py @@ -0,0 +1,85 @@ +from mathesis.grammars import ( + BasicPropositionalGrammar, + BasicGrammar +) +from mathesis.forms import ( + Atom, + Top, + Bottom, + Negation, + Conjunction, + Disjunction, + Conditional, + Universal, + Particular +) + + +def test_propositional_grammar(): + grammar = BasicPropositionalGrammar() + assert grammar.parse("⊥ ∨ (B → C)") == Disjunction( + Bottom(), + Conditional( + Atom("B"), + Atom("C") + ) + ) + assert grammar.parse("⊤ ∧ (P_1 ∧ ¬P_2)") == Conjunction( + Top(), + Conjunction( + Atom("P_1"), + Negation(Atom("P_2")) + ) + ) + + # Test for the order of precedence of operators + assert grammar.parse("P ∨ Q ∧ ¬R → T") == Conditional( + Disjunction( + Atom("P"), + Conjunction( + Atom("Q"), + Negation(Atom("R")) + ) + ), + Atom("T") + ) + + # Test for symbol customization + grammar = BasicPropositionalGrammar( + symbols={"conditional": "->"} + ) + assert grammar.parse("A -> B") == Conditional(Atom("A"), Atom("B")) + + +def test_first_order_grammar(): + grammar = BasicGrammar() + assert grammar.parse("∀x((P(x) ∧ Q(x)) → R(x, x))") == Universal( + "x", + Conditional( + Conjunction( + Atom("P", terms=["x"]), + Atom("Q", terms=["x"]) + ), + Atom("R", terms=["x", "x"]) + ) + ) + + assert grammar.parse("∃y∀x(P123(x, y) ∨ P123(y, x))") == Particular( + "y", + Universal( + "x", + Disjunction( + Atom("P123", terms=["x", "y"]), + Atom("P123", terms=["y", "x"]) + ) + ) + ) + + # Test with nullary predicates (propositions) + assert grammar.parse("⊤ ∨ (A → B)") == Disjunction( + Top(), + Conditional( + Atom("A"), + Atom("B") + ) + )