diff --git a/tests/test_modus_ponens.py b/tests/test_modus_ponens.py index fa9c2258..06a74acd 100644 --- a/tests/test_modus_ponens.py +++ b/tests/test_modus_ponens.py @@ -21,14 +21,13 @@ def test_modus_ponens_without_variable(self): q_formula = u.f(r2, o2) self.assertEqual('r2(o2)', q_formula.rep_formula(encoding=pu.encodings.plaintext)) self.assertEqual('π‘Ÿβ‚‚(π‘œβ‚‚)', q_formula.rep_formula(encoding=pu.encodings.unicode)) - p_implies_q = t.i.axiom_interpretation.infer_statement(ap, u.f(u.r.implies, p_formula, - q_formula)) + p_implies_q = t.i.axiom_interpretation.infer_statement(ap, + u.f(u.r.implies, p_formula, q_formula)) p_statement = t.i.axiom_interpretation.infer_statement(ap, p_formula) mp = t.i.mp.infer_statement(p_implies_q, p_statement) self.assertEqual('r2(o2)', - mp.valid_proposition.rep_formula(encoding=pu.encodings.plaintext)) - self.assertEqual('π‘Ÿβ‚‚(π‘œβ‚‚)', - mp.valid_proposition.rep_formula(encoding=pu.encodings.unicode)) + mp.valid_proposition.rep_formula(encoding=pu.encodings.plaintext)) + self.assertEqual('π‘Ÿβ‚‚(π‘œβ‚‚)', mp.valid_proposition.rep_formula(encoding=pu.encodings.unicode)) def test_modus_ponens_with_free_variables(self): pu.configuration.echo_default = True @@ -41,18 +40,16 @@ def test_modus_ponens_with_free_variables(self): a = u.declare_axiom(random_data.random_sentence()) ap = t.include_axiom(a) with u.v() as x, u.v() as y, u.v() as z: - p_implies_q = t.i.axiom_interpretation.infer_statement( - ap, - u.f( - u.r.implies, - u.f(u.r.land, u.f(r1, x, y), u.f(r1, y, z)), - u.f(r1, x, z)), echo=True) - phi1 = t.i.axiom_interpretation.infer_statement(ap, u.f(r1, o1, o2)) - phi2 = t.i.axiom_interpretation.infer_statement(ap, u.f(r1, o2, o3)) - p_prime = t.i.ci.infer_statement(phi1, phi2, echo=True) - p_implies_q_prime = t.i.vs.infer_statement(p_implies_q, o1, o2, o3, echo=True) + p_implies_q = t.i.axiom_interpretation.infer_statement(ap, + (r1(x, y) | u.r.land | r1(y, z)) | u.r.implies | r1(x, z), echo=True) + t.i.axiom_interpretation.infer_statement(axiom=ap, formula=r1(o1, o2)) + t.i.axiom_interpretation.infer_statement(axiom=ap, formula=r1(o2, o3)) + p_prime = t.i.conjunction_introduction.infer_statement(p=r1(o1, o2), q=r1(o2, o3), + echo=True) + p_implies_q_prime = t.i.variable_substitution.infer_statement(p=p_implies_q, + phi=(o1, o2, o3), echo=True) conclusion = t.i.mp.infer_statement(p_implies_q_prime, p_prime, echo=True) self.assertEqual('r1(o1, o3)', - conclusion.valid_proposition.rep_formula(pu.encodings.plaintext)) + conclusion.valid_proposition.rep_formula(pu.encodings.plaintext)) self.assertEqual('π‘Ÿβ‚(π‘œβ‚, π‘œβ‚ƒ)', - conclusion.valid_proposition.rep_formula(pu.encodings.unicode)) + conclusion.valid_proposition.rep_formula(pu.encodings.unicode)) diff --git a/tests/test_nameset.py b/tests/test_nameset.py index db6651de..f943f926 100644 --- a/tests/test_nameset.py +++ b/tests/test_nameset.py @@ -7,15 +7,11 @@ class TestNameSet(TestCase): def test_nameset_1(self): pu.configuration.echo_default = False - n = pu.NameSet( - # symbolic names - symbol='x', index=1, dashed_name='something-precise', - # natural language names + n = pu.NameSet(# symbolic names + symbol='x', index=1, dashed_name='something-precise', # natural language names acronym='smthng', abridged_name='someth.', name='something', - explicit_name='something precise', - # section names - paragraph_header=pu.paragraph_headers.note, - ref='1.1.1', subtitle='about something') + explicit_name='something precise', # section names + paragraph_header=pu.paragraph_headers.note, ref='1.1.1', subtitle='about something') # Plaintext symbolic representations self.assertEqual('x1', n.rep_symbol(encoding=pu.encodings.plaintext)) @@ -31,7 +27,7 @@ def test_nameset_1(self): self.assertEqual('something', n.rep_conventional_name(encoding=pu.encodings.plaintext)) # Plaintext section title self.assertEqual('note 1.1.1 (x1) - about something', - n.rep_title(encoding=pu.encodings.plaintext)) + n.rep_title(encoding=pu.encodings.plaintext)) # Unicode symbolic representations self.assertEqual('π‘₯₁', n.rep_symbol(encoding=pu.encodings.unicode)) @@ -47,27 +43,26 @@ def test_nameset_1(self): self.assertEqual('π—Œπ—ˆπ—†π–Ύπ—π—π—‚π—‡π—€', n.rep_conventional_name(encoding=pu.encodings.unicode)) # Unicode section title self.assertEqual('π—»π—Όπ˜π—² 𝟭.𝟭.𝟭 (π‘₯₁) - about something', - n.rep_title(encoding=pu.encodings.unicode)) + n.rep_title(encoding=pu.encodings.unicode)) # LaTeX math basic representations self.assertEqual('\\mathit{x}_{1}', n.rep_symbol(encoding=pu.encodings.latex)) self.assertEqual('\\mathit{something-precise}', - n.rep_dashed_name(encoding=pu.encodings.latex)) + n.rep_dashed_name(encoding=pu.encodings.latex)) # LaTeX math natural language representations self.assertEqual('\\mathsf{smthng}', n.rep_acronym(encoding=pu.encodings.latex)) self.assertEqual('\\mathsf{someth.}', n.rep_abridged_name(encoding=pu.encodings.latex)) self.assertEqual('\\mathsf{something}', n.rep_name(encoding=pu.encodings.latex)) self.assertEqual('\\mathsf{something precise}', - n.rep_explicit_name(encoding=pu.encodings.latex)) + n.rep_explicit_name(encoding=pu.encodings.latex)) # LaTeX math prioritized name representations self.assertEqual('\\mathsf{someth.}', n.rep_compact_name(encoding=pu.encodings.latex)) self.assertEqual('\\mathsf{something precise}', - n.rep_accurate_name(encoding=pu.encodings.latex)) + n.rep_accurate_name(encoding=pu.encodings.latex)) self.assertEqual('\\mathsf{something}', - n.rep_conventional_name(encoding=pu.encodings.latex)) + n.rep_conventional_name(encoding=pu.encodings.latex)) def test_nameset_title(self): - n1 = pu.NameSet(symbol='x', index=1, - paragraph_header=pu.paragraph_headers._hypothesis_statement_in_child_theory) + n1 = pu.NameSet(symbol='x', index=1, paragraph_header=pu.paragraph_headers.hypothesis) s1 = n1.rep_title(encoding=pu.encodings.plaintext) print(s1)