documentation #195 + inference validation #126

project/sandbox.py

@@ -0,0 +1,18 @@
+import dataclasses
+
+
+@dataclasses.dataclass(frozen=True, kw_only=True)
+class InferenceRuleArguments:
+    pass
+
+
+@dataclasses.dataclass(frozen=True, kw_only=True)
+class Test(InferenceRuleArguments):
+    x: int
+    y: int
+
+
+t = Test(x=1, y=2)
+print(t)
+print(type(t))
+print(type(Test))

project/sandbox2.py

@@ -0,0 +1,18 @@
+import typing
+from typing import Optional, Union
+
+# MyArg = collections.namedtuple('MyArg', ['x', 'y'])
+super_type = Optional[Union[int, float, str]]
+
+
+class MyArg(typing.NamedTuple):
+    x: super_type
+    y: int
+
+
+MyArg2 = typing.NamedTuple('MyArg2', )
+
+t = MyArg(x=1, y=2)
+print(t)
+print(type(t))
+print(type(MyArg))

src/sample/sample_absorption.py

@@ -12,8 +12,8 @@
 # Elaborate a dummy theory with a set of propositions necessary for our demonstration
 t1 = u.t(echo=True)
 theory_axiom = t1.include_axiom(a=axiom)
-p_implies_q = t1.i.axiom_interpretation.infer_formula_statement(axiom=theory_axiom,
-    formula=r1(o1, o2) | u.r.implies | r2(o3))
+p_implies_q = t1.i.axiom_interpretation.infer_formula_statement(a=theory_axiom,
+    p=r1(o1, o2) | u.r.implies | r2(o3))
 
 # And finally, use the absorption inference-rule:
 proposition_of_interest = t1.i.absorption.infer_formula_statement(p_implies_q=p_implies_q,

src/sample/sample_axiom_interpretation.py

@@ -14,5 +14,5 @@
 theory_axiom = t1.include_axiom(a=axiom)
 
 # And finally, use the absorption inference-rule:
-proposition_of_interest = t1.i.axiom_interpretation.infer_formula_statement(axiom=theory_axiom,
+proposition_of_interest = t1.i.axiom_interpretation.infer_formula_statement(a=theory_axiom,
     formula=r1(o1, o2) | u.r.implies | r2(o3), subtitle='The proposition of interest')

src/sample/sample_biconditional_elimination_1.py

@@ -12,7 +12,7 @@
 # Elaborate a dummy theory with a set of propositions necessary for our demonstration
 t1 = u.t(echo=True)
 theory_axiom = t1.include_axiom(a=axiom)
-phi1 = t1.i.axiom_interpretation.infer_formula_statement(axiom=theory_axiom,
+phi1 = t1.i.axiom_interpretation.infer_formula_statement(a=theory_axiom,
     formula=r1(o1, o2) | u.r.biconditional | r2(o3))
 
 # And finally, use the biconditional-elimination-1 inference-rule:

src/sample/sample_biconditional_elimination_2.py

@@ -12,7 +12,7 @@
 # Elaborate a dummy theory with a set of propositions necessary for our demonstration
 t1 = u.t(echo=True)
 theory_axiom = t1.include_axiom(a=axiom)
-phi1 = t1.i.axiom_interpretation.infer_formula_statement(axiom=theory_axiom,
+phi1 = t1.i.axiom_interpretation.infer_formula_statement(a=theory_axiom,
     formula=r1(o1, o2) | u.r.biconditional | r2(o3))
 
 # And finally, use the biconditional-elimination-2 inference-rule:

src/sample/sample_biconditional_introduction.py

@@ -12,9 +12,9 @@
 # Elaborate a dummy theory with a set of propositions necessary for our demonstration
 t1 = u.t(echo=True)
 theory_axiom = t1.include_axiom(a=axiom)
-phi1 = t1.i.axiom_interpretation.infer_formula_statement(axiom=theory_axiom,
+phi1 = t1.i.axiom_interpretation.infer_formula_statement(a=theory_axiom,
     formula=r1(o1, o2) | u.r.implies | r2(o3))
-phi2 = t1.i.axiom_interpretation.infer_formula_statement(axiom=theory_axiom,
+phi2 = t1.i.axiom_interpretation.infer_formula_statement(a=theory_axiom,
     formula=r2(o3) | u.r.implies | r1(o1, o2))
 
 # And finally, use the biconditional-introduction inference-rule:

src/sample/sample_conjunction_elimination_1.py

@@ -12,7 +12,7 @@
 # Elaborate a dummy theory with a set of propositions necessary for our demonstration
 t1 = u.t(echo=True)
 theory_axiom = t1.include_axiom(axiom)
-phi1 = t1.i.axiom_interpretation.infer_formula_statement(axiom=theory_axiom,
+phi1 = t1.i.axiom_interpretation.infer_formula_statement(a=theory_axiom,
     formula=r1(o1, o2) | u.r.land | r2(o3))
 
 # And finally, use the conjunction-elimination-1 inference-rule:

src/sample/sample_conjunction_elimination_2.py

@@ -12,7 +12,7 @@
 # Elaborate a dummy theory with a set of propositions necessary for our demonstration
 t1 = u.t(echo=True)
 theory_axiom = t1.include_axiom(axiom)
-phi1 = t1.i.axiom_interpretation.infer_formula_statement(axiom=theory_axiom,
+phi1 = t1.i.axiom_interpretation.infer_formula_statement(a=theory_axiom,
     formula=r1(o1, o2) | u.r.land | r2(o3))
 
 # And finally, use the conjunction-elimination-2 inference-rule:

src/sample/sample_conjunction_introduction.py

@@ -12,8 +12,8 @@
 # Elaborate a dummy theory with a set of propositions necessary for our demonstration
 t1 = u.t(echo=True)
 theory_axiom = t1.include_axiom(a=axiom)
-phi1 = t1.i.axiom_interpretation.infer_formula_statement(axiom=theory_axiom, formula=r1(o1, o2))
-phi2 = t1.i.axiom_interpretation.infer_formula_statement(axiom=theory_axiom, formula=r2(o3))
+phi1 = t1.i.axiom_interpretation.infer_formula_statement(a=theory_axiom, formula=r1(o1, o2))
+phi2 = t1.i.axiom_interpretation.infer_formula_statement(a=theory_axiom, formula=r2(o3))
 
 # And finally, use the conjunction-introduction inference-rule:
 proposition_of_interest = t1.i.conjunction_introduction.infer_formula_statement(p=phi1, q=phi2,

src/sample/sample_disjunction_introduction_1.py

@@ -12,7 +12,7 @@
 # Elaborate a dummy theory with a set of propositions necessary for our demonstration
 t1 = u.t(echo=True)
 theory_axiom = t1.include_axiom(a=axiom)
-phi1 = t1.i.axiom_interpretation.infer_formula_statement(axiom=theory_axiom, formula=r1(o1, o2))
+phi1 = t1.i.axiom_interpretation.infer_formula_statement(a=theory_axiom, formula=r1(o1, o2))
 
 # And finally, use the disjunction-introduction-1 inference-rule:
 proposition_of_interest = t1.i.disjunction_introduction_1.infer_formula_statement(p=phi1, q=r2(o3),

src/sample/sample_disjunction_introduction_2.py

@@ -12,7 +12,7 @@
 # Elaborate a dummy theory with a set of propositions necessary for our demonstration
 t1 = u.t(echo=True)
 theory_axiom = t1.include_axiom(a=axiom)
-phi1 = t1.i.axiom_interpretation.infer_formula_statement(axiom=theory_axiom, formula=r1(o1, o2))
+phi1 = t1.i.axiom_interpretation.infer_formula_statement(a=theory_axiom, formula=r1(o1, o2))
 
 # And finally, use the disjunction-introduction-2 inference-rule:
 proposition_of_interest = t1.i.disjunction_introduction_2.infer_formula_statement(p=phi1, q=r2(o3),

src/sample/sample_double_negation_elimination.py

@@ -10,7 +10,7 @@
 # Elaborate a dummy theory with a set of propositions necessary for our demonstration
 t1 = u.t(echo=True)
 theory_axiom = t1.include_axiom(a=axiom)
-not_not_p = t1.i.axiom_interpretation.infer_formula_statement(axiom=theory_axiom,
+not_not_p = t1.i.axiom_interpretation.infer_formula_statement(a=theory_axiom,
     formula=u.r.lnot(u.r.lnot(r1(o1, o2))))
 
 # And finally, use the double-negation-elimination inference-rule:

src/sample/sample_double_negation_introduction.py

@@ -10,7 +10,7 @@
 # Elaborate a dummy theory with a set of propositions necessary for our demonstration
 t1 = u.t(echo=True)
 theory_axiom = t1.include_axiom(a=axiom)
-p = t1.i.axiom_interpretation.infer_formula_statement(axiom=theory_axiom, formula=r1(o1, o2))
+p = t1.i.axiom_interpretation.infer_formula_statement(a=theory_axiom, formula=r1(o1, o2))
 
 # And finally, use the double-negation-introduction inference-rule:
 proposition_of_interest = t1.i.double_negation_introduction.infer_formula_statement(p=p,

src/sample/sample_equal_terms_substitution.py

@@ -12,9 +12,9 @@
 # Elaborate a dummy theory with a set of propositions necessary for our demonstration
 t1 = u.t(echo=True)
 theory_axiom = t1.include_axiom(a=axiom)
-proposition_x_equal_y = t1.i.axiom_interpretation.infer_formula_statement(axiom=theory_axiom,
+proposition_x_equal_y = t1.i.axiom_interpretation.infer_formula_statement(a=theory_axiom,
     formula=u.f(u.r.equal, u.f(r1, o1, o2), u.f(r2, o3)))
-dummy_proposition = t1.i.axiom_interpretation.infer_formula_statement(axiom=theory_axiom,
+dummy_proposition = t1.i.axiom_interpretation.infer_formula_statement(a=theory_axiom,
     formula=u.f(r1, u.f(r1, u.f(r1, u.f(r1, o1, o2), u.f(r1, o1, o2)), o2),
         u.f(r2, u.f(r1, o1, o2))))
 

src/sample/sample_equality_commutativity.py

@@ -12,7 +12,7 @@
 # Elaborate a dummy theory with a set of propositions necessary for our demonstration
 t1 = u.t(echo=True)
 theory_axiom = t1.include_axiom(a=axiom)
-p = t1.i.axiom_interpretation.infer_formula_statement(axiom=theory_axiom,
+p = t1.i.axiom_interpretation.infer_formula_statement(a=theory_axiom,
     formula=r1(o1, o2) | u.r.equal | r2(o3))
 
 # And finally, use the equality-commutativity inference-rule:

src/sample/sample_hypothesis.py

@@ -14,9 +14,9 @@
 # t theory elaboration statements.
 # these are predecessor statements that are contained in the h hypothesis.
 a = t1.include_axiom(a=a1)
-predecessor = t1.i.axiom_interpretation.infer_formula_statement(axiom=a, formula=f(o2, o3))
+predecessor = t1.i.axiom_interpretation.infer_formula_statement(a=a, formula=f(o2, o3))
 with u.v('x') as x, u.v('y') as y, u.v('z') as z:
-    implication = t1.i.axiom_interpretation.infer_formula_statement(axiom=a,
+    implication = t1.i.axiom_interpretation.infer_formula_statement(a=a,
         formula=(f(x, y) | u.r.land | f(y, z)) | u.r.implies | f(x, z))
 t1.stabilize()
 t1.take_note(

src/sample/sample_modus_ponens.py

@@ -12,9 +12,9 @@
 # Elaborate a dummy theory with a set of propositions necessary for our demonstration
 t1 = u.t(echo=True)
 theory_axiom = t1.include_axiom(a=axiom)
-p_implies_q = t1.i.axiom_interpretation.infer_formula_statement(axiom=theory_axiom,
+p_implies_q = t1.i.axiom_interpretation.infer_formula_statement(a=theory_axiom,
     formula=r1(o1, o2) | u.r.implies | r2(o3))
-p = t1.i.axiom_interpretation.infer_formula_statement(axiom=theory_axiom, formula=r1(o1, o2))
+p = t1.i.axiom_interpretation.infer_formula_statement(a=theory_axiom, formula=r1(o1, o2))
 
 # And finally, use the modus-ponens inference-rule:
 proposition_of_interest = t1.i.modus_ponens.infer_formula_statement(p_implies_q=p_implies_q, p=p,

src/sample/sample_proof_by_contradiction_1.py

@@ -12,10 +12,10 @@
 # Elaborate a dummy theory with a set of propositions necessary for our demonstration
 a = t1.include_axiom(a=a1)
 pu.configuration.echo_proof = False
-t1.i.axiom_interpretation.infer_formula_statement(axiom=a, formula=f(o1, o2))
-t1.i.axiom_interpretation.infer_formula_statement(axiom=a, formula=f(o2, o3))
+t1.i.axiom_interpretation.infer_formula_statement(a=a, formula=f(o1, o2))
+t1.i.axiom_interpretation.infer_formula_statement(a=a, formula=f(o2, o3))
 with u.v('x') as x, u.v('y') as y, u.v('z') as z:
-    implication = t1.i.axiom_interpretation.infer_formula_statement(axiom=a,
+    implication = t1.i.axiom_interpretation.infer_formula_statement(a=a,
         formula=(f(x, y) | u.r.land | f(y, z)) | u.r.implies | f(x, z))
 t1.stabilize()
 

src/sample/sample_proof_by_contradiction_2.py

@@ -14,7 +14,7 @@
 f_o1_eq_f_02 = t1.i.axiom_interpretation.infer_formula_statement(theory_axiom,
     (f(o1) | u.r.eq | f(o2)))
 with u.v('x') as x, u.v('y') as y:
-    implication = t1.i.axiom_interpretation.infer_formula_statement(axiom=theory_axiom,
+    implication = t1.i.axiom_interpretation.infer_formula_statement(a=theory_axiom,
         formula=(f(x) | u.r.eq | f(y)) | u.r.implies | (x | u.r.eq | y))
 t1.stabilize()
 

src/sample/sample_proof_by_refutation_1.py

@@ -11,10 +11,10 @@
 
 # Elaborate a dummy theory with a set of propositions necessary for our demonstration
 a = t1.include_axiom(a=a1)
-t1.i.axiom_interpretation.infer_formula_statement(axiom=a, formula=f(o1, o2))
-t1.i.axiom_interpretation.infer_formula_statement(axiom=a, formula=f(o2, o3))
+t1.i.axiom_interpretation.infer_formula_statement(a=a, formula=f(o1, o2))
+t1.i.axiom_interpretation.infer_formula_statement(a=a, formula=f(o2, o3))
 with u.v('x') as x, u.v('y') as y, u.v('z') as z:
-    implication = t1.i.axiom_interpretation.infer_formula_statement(axiom=a,
+    implication = t1.i.axiom_interpretation.infer_formula_statement(a=a,
         formula=(f(x, y) | u.r.land | f(y, z)) | u.r.implies | u.r.lnot(f(x, z)))
 t1.stabilize()
 

src/sample/sample_proof_by_refutation_2.py

@@ -13,7 +13,7 @@
 f_o1_eq_f_02 = t1.i.axiom_interpretation.infer_formula_statement(theory_axiom,
     (f(o1) | u.r.eq | f(o2)))
 with u.v('x') as x, u.v('y') as y:
-    implication = t1.i.axiom_interpretation.infer_formula_statement(axiom=theory_axiom,
+    implication = t1.i.axiom_interpretation.infer_formula_statement(a=theory_axiom,
         formula=(f(x) | u.r.eq | f(y)) | u.r.implies | (x | u.r.neq | y))
 t1.stabilize()
 

src/sample/sample_variable_substitution.py

@@ -11,9 +11,9 @@
 
 # Elaborate a dummy theory with a set of propositions necessary for our demonstration
 a = t1.include_axiom(a=a1)
-t1.i.axiom_interpretation.infer_formula_statement(axiom=a, formula=f(o1, o2))
+t1.i.axiom_interpretation.infer_formula_statement(a=a, formula=f(o1, o2))
 with u.v('x') as x, u.v('y') as y:
-    implication = t1.i.axiom_interpretation.infer_formula_statement(axiom=a,
+    implication = t1.i.axiom_interpretation.infer_formula_statement(a=a,
         formula=f(x, y) | u.r.implies | f(y, x))
 t1.stabilize()
 

src/theory/theory_tao_2006_the_peano_axioms.py

@@ -330,7 +330,7 @@ def __init__(self, t: (None, pu.TheoryElaborationSequence) = None,
             # ((m is-a natural-number) ⟹ P(m))
             phi6 = (m | u.r.is_a | natural_number) | u.r.implies | p(m)
             phi7 = phi5 | u.r.implies | phi6
-            p100 = t.i.axiom_interpretation.infer_formula_statement(axiom=a_2_5b, formula=phi7)
+            p100 = t.i.axiom_interpretation.infer_formula_statement(a=a_2_5b, formula=phi7)
 
         t.take_note(paragraph_header=pu.paragraph_headers.remark, ref='2.1.10',
             content='We are a little vague on what "property" means at this point, but some possible examples of P(n) might be "n is even"; "n is equal to 3"; "n solves the equation (n + 1)2 = n2 + 2n + 1"; and so forth. Of course we haven\'t defined many of these concepts yet, but when we do, Axiom 2.5 will apply to these properties. (A logical remark: Because this axiom refers not just to variables, but also properties, it is of a different nature than the other four axioms; indeed, Axiom 2.5 should technically be called an axiom schema rather than an axiom - it is a template for producing an (infinite) number of axioms, rather than being a single axiom in its own right. To discuss this distinction further is far beyond the scope of this text, though, and falls in the realm of logic.) [Tao, 2006, p. 22]')

tests/test_inconsistency_introduction_1.py

@@ -26,13 +26,12 @@ def test_inconsistency_introduction_1_with_hypothesis(self):
         # Elaborate the parent theory
         t1 = u.t()
         axiom_theory = t1.include_axiom(a=axiom)
-        t1_p1 = t1.i.axiom_interpretation.infer_formula_statement(axiom=axiom_theory,
+        t1_p1 = t1.i.axiom_interpretation.infer_formula_statement(a=axiom_theory,
             formula=r1(o1, o2))
-        t1_p2 = t1.i.axiom_interpretation.infer_formula_statement(axiom=axiom_theory,
+        t1_p2 = t1.i.axiom_interpretation.infer_formula_statement(a=axiom_theory,
             formula=r1(o2, o3))
         with u.v() as x, u.v() as y, u.v() as z:
-            t1_p3_implication = t1.i.axiom_interpretation.infer_formula_statement(
-                axiom=axiom_theory,
+            t1_p3_implication = t1.i.axiom_interpretation.infer_formula_statement(a=axiom_theory,
                 formula=((r1(x, y) | u.r.land | r1(y, z)) | u.r.implies | r1(x, z)))
         t1.stabilize()
         hypothetical_formula = u.f(u.r.lnot, u.f(r1, o1, o3))

tests/test_modus_ponens.py

@@ -31,8 +31,8 @@ def test_modus_ponens_with_free_variables(self):
         with u.v() as x, u.v() as y, u.v() as z:
             p_implies_q = t.i.axiom_interpretation.infer_formula_statement(ap,
                 (r1(x, y) | u.r.land | r1(y, z)) | u.r.implies | r1(x, z), echo=True)
-        t.i.axiom_interpretation.infer_formula_statement(axiom=ap, formula=r1(o1, o2))
-        t.i.axiom_interpretation.infer_formula_statement(axiom=ap, formula=r1(o2, o3))
+        t.i.axiom_interpretation.infer_formula_statement(a=ap, formula=r1(o1, o2))
+        t.i.axiom_interpretation.infer_formula_statement(a=ap, formula=r1(o2, o3))
         p_prime = t.i.conjunction_introduction.infer_formula_statement(p=r1(o1, o2), q=r1(o2, o3),
             echo=True)
         p_implies_q_prime = t.i.variable_substitution.infer_formula_statement(p=p_implies_q,

tests/test_validate_formula_statement.py

@@ -18,7 +18,7 @@ def test_validate_statement_unary_function_call_formula(self):
         phi = u.f(r1, o1)
         t = u.declare_theory()
         a = t.include_axiom(a=u.declare_axiom(natural_language='Dummy axiom for testing purposes'))
-        t.i.axiom_interpretation.infer_formula_statement(axiom=a, formula=phi)
+        t.i.axiom_interpretation.infer_formula_statement(a=a, formula=phi)
         phi1_formula = pu.validate_formula_statement(t=t, input_value=u.f(r1, o1))
         self.assertTrue(phi.is_formula_syntactically_equivalent_to(phi1_formula))
         phi1_tuple = pu.validate_formula_statement(t=t, input_value=(r1, o1))

tests/test_variable_substitution.py

@@ -16,7 +16,7 @@ def test_variable_substitution_without_variable(self):
         a = u.declare_axiom(natural_language=random_data.random_sentence())
         ap = t.include_axiom(a=a)
         p_formula = r1(r2(o1, o2))
-        p_statement = t.i.axiom_interpretation.infer_formula_statement(axiom=ap, formula=p_formula,
+        p_statement = t.i.axiom_interpretation.infer_formula_statement(a=ap, formula=p_formula,
             echo=True)
         # y_sequence = tuple()
         p_prime = t.i.vs.infer_formula_statement(p=p_statement, phi=(), echo=True)
@@ -39,7 +39,7 @@ def test_variable_substitution_with_free_variables(self):
         ap = t.include_axiom(a)
         with u.v(symbol='x', auto_index=False) as x, u.v(symbol='y', auto_index=False) as y, u.v(
                 symbol='z', auto_index=False) as z:
-            p_statement = t.i.axiom_interpretation.infer_formula_statement(axiom=ap,
+            p_statement = t.i.axiom_interpretation.infer_formula_statement(a=ap,
                 formula=f(g(g(z, g(f(x), y)), g(x, y))), echo=True)
         self.assertEqual('𝑓(𝑔(𝑔(𝐳, 𝑔(𝑓(𝐱), 𝐲)), 𝑔(𝐱, 𝐲)))',
             p_statement.rep_formula(encoding=pu.encodings.unicode))