From cb779c0be2691bad1edc2b34df0ce3eb4c6bb7a2 Mon Sep 17 00:00:00 2001
From: David Doret <david.doret@me.com>
Date: Tue, 3 Oct 2023 13:33:15 +0200
Subject: [PATCH] documentation #195 + inference validation #126 + support for
 the composition of collection-like formulae + usage of
 sequent-collection-comma to define inference-rules + enhanced exceptions with
 user-friendly reports + #220 interdiction of variable-substitution of
 propositional objects with non-propositional objects.

---
 .idea/workspace.xml                           | 179 ++++++++++--------
 src/punctilious/core.py                       |  82 ++++----
 .../sample_conjunction_elimination_1.py       |   2 +-
 .../sample_conjunction_elimination_2.py       |   2 +-
 src/sample/sample_conjunction_introduction.py |   4 +-
 5 files changed, 145 insertions(+), 124 deletions(-)

diff --git a/.idea/workspace.xml b/.idea/workspace.xml
index 9c204320..73d292d5 100644
--- a/.idea/workspace.xml
+++ b/.idea/workspace.xml
@@ -7,6 +7,9 @@
     <list default="true" id="48b609c4-0198-44a9-8f40-0a1e1f4ae31e" name="Changes" comment="documentation #195 + inference validation #126 + support for the composition of collection-like formulae + usage of sequent-collection-comma to define inference-rules + enhanced exceptions with user-friendly reports + #220 interdiction of variable-substitution of propositional objects with non-propositional objects.">
       <change beforePath="$PROJECT_DIR$/.idea/workspace.xml" beforeDir="false" afterPath="$PROJECT_DIR$/.idea/workspace.xml" afterDir="false" />
       <change beforePath="$PROJECT_DIR$/src/punctilious/core.py" beforeDir="false" afterPath="$PROJECT_DIR$/src/punctilious/core.py" afterDir="false" />
+      <change beforePath="$PROJECT_DIR$/src/sample/sample_conjunction_elimination_1.py" beforeDir="false" afterPath="$PROJECT_DIR$/src/sample/sample_conjunction_elimination_1.py" afterDir="false" />
+      <change beforePath="$PROJECT_DIR$/src/sample/sample_conjunction_elimination_2.py" beforeDir="false" afterPath="$PROJECT_DIR$/src/sample/sample_conjunction_elimination_2.py" afterDir="false" />
+      <change beforePath="$PROJECT_DIR$/src/sample/sample_conjunction_introduction.py" beforeDir="false" afterPath="$PROJECT_DIR$/src/sample/sample_conjunction_introduction.py" afterDir="false" />
     </list>
     <option name="SHOW_DIALOG" value="false" />
     <option name="HIGHLIGHT_CONFLICTS" value="true" />
@@ -119,7 +122,7 @@
       <recent name="C:\Users\David\PycharmProjects\punctilious\continuous_integration" />
     </key>
   </component>
-  <component name="RunManager" selected="Python tests.Python tests in test_axiom_interpretation.py">
+  <component name="RunManager" selected="Python.sample_conjunction_introduction">
     <configuration name="build" type="PythonConfigurationType" factoryName="Python" nameIsGenerated="true">
       <module name="2023_05_02_PyCharmProject_Maths" />
       <option name="INTERPRETER_OPTIONS" value="" />
@@ -227,6 +230,90 @@
       <option name="INPUT_FILE" value="" />
       <method v="2" />
     </configuration>
+    <configuration name="sample_biconditional_introduction" type="PythonConfigurationType" factoryName="Python" temporary="true" nameIsGenerated="true">
+      <module name="2023_05_02_PyCharmProject_Maths" />
+      <option name="INTERPRETER_OPTIONS" value="" />
+      <option name="PARENT_ENVS" value="true" />
+      <envs>
+        <env name="PYTHONUNBUFFERED" value="1" />
+      </envs>
+      <option name="SDK_HOME" value="" />
+      <option name="WORKING_DIRECTORY" value="$PROJECT_DIR$/src/sample" />
+      <option name="IS_MODULE_SDK" value="true" />
+      <option name="ADD_CONTENT_ROOTS" value="true" />
+      <option name="ADD_SOURCE_ROOTS" value="true" />
+      <option name="SCRIPT_NAME" value="$PROJECT_DIR$/src/sample/sample_biconditional_introduction.py" />
+      <option name="PARAMETERS" value="" />
+      <option name="SHOW_COMMAND_LINE" value="false" />
+      <option name="EMULATE_TERMINAL" value="false" />
+      <option name="MODULE_MODE" value="false" />
+      <option name="REDIRECT_INPUT" value="false" />
+      <option name="INPUT_FILE" value="" />
+      <method v="2" />
+    </configuration>
+    <configuration name="sample_conjunction_elimination_1" type="PythonConfigurationType" factoryName="Python" temporary="true" nameIsGenerated="true">
+      <module name="2023_05_02_PyCharmProject_Maths" />
+      <option name="INTERPRETER_OPTIONS" value="" />
+      <option name="PARENT_ENVS" value="true" />
+      <envs>
+        <env name="PYTHONUNBUFFERED" value="1" />
+      </envs>
+      <option name="SDK_HOME" value="" />
+      <option name="WORKING_DIRECTORY" value="$PROJECT_DIR$/src/sample" />
+      <option name="IS_MODULE_SDK" value="true" />
+      <option name="ADD_CONTENT_ROOTS" value="true" />
+      <option name="ADD_SOURCE_ROOTS" value="true" />
+      <option name="SCRIPT_NAME" value="$PROJECT_DIR$/src/sample/sample_conjunction_elimination_1.py" />
+      <option name="PARAMETERS" value="" />
+      <option name="SHOW_COMMAND_LINE" value="false" />
+      <option name="EMULATE_TERMINAL" value="false" />
+      <option name="MODULE_MODE" value="false" />
+      <option name="REDIRECT_INPUT" value="false" />
+      <option name="INPUT_FILE" value="" />
+      <method v="2" />
+    </configuration>
+    <configuration name="sample_conjunction_elimination_2" type="PythonConfigurationType" factoryName="Python" temporary="true" nameIsGenerated="true">
+      <module name="2023_05_02_PyCharmProject_Maths" />
+      <option name="INTERPRETER_OPTIONS" value="" />
+      <option name="PARENT_ENVS" value="true" />
+      <envs>
+        <env name="PYTHONUNBUFFERED" value="1" />
+      </envs>
+      <option name="SDK_HOME" value="" />
+      <option name="WORKING_DIRECTORY" value="$PROJECT_DIR$/src/sample" />
+      <option name="IS_MODULE_SDK" value="true" />
+      <option name="ADD_CONTENT_ROOTS" value="true" />
+      <option name="ADD_SOURCE_ROOTS" value="true" />
+      <option name="SCRIPT_NAME" value="$PROJECT_DIR$/src/sample/sample_conjunction_elimination_2.py" />
+      <option name="PARAMETERS" value="" />
+      <option name="SHOW_COMMAND_LINE" value="false" />
+      <option name="EMULATE_TERMINAL" value="false" />
+      <option name="MODULE_MODE" value="false" />
+      <option name="REDIRECT_INPUT" value="false" />
+      <option name="INPUT_FILE" value="" />
+      <method v="2" />
+    </configuration>
+    <configuration name="sample_conjunction_introduction" type="PythonConfigurationType" factoryName="Python" temporary="true" nameIsGenerated="true">
+      <module name="2023_05_02_PyCharmProject_Maths" />
+      <option name="INTERPRETER_OPTIONS" value="" />
+      <option name="PARENT_ENVS" value="true" />
+      <envs>
+        <env name="PYTHONUNBUFFERED" value="1" />
+      </envs>
+      <option name="SDK_HOME" value="" />
+      <option name="WORKING_DIRECTORY" value="$PROJECT_DIR$/src/sample" />
+      <option name="IS_MODULE_SDK" value="true" />
+      <option name="ADD_CONTENT_ROOTS" value="true" />
+      <option name="ADD_SOURCE_ROOTS" value="true" />
+      <option name="SCRIPT_NAME" value="$PROJECT_DIR$/src/sample/sample_conjunction_introduction.py" />
+      <option name="PARAMETERS" value="" />
+      <option name="SHOW_COMMAND_LINE" value="false" />
+      <option name="EMULATE_TERMINAL" value="false" />
+      <option name="MODULE_MODE" value="false" />
+      <option name="REDIRECT_INPUT" value="false" />
+      <option name="INPUT_FILE" value="" />
+      <method v="2" />
+    </configuration>
     <configuration name="pytest tests" type="ShConfigurationType">
       <option name="SCRIPT_TEXT" value="pytest tests" />
       <option name="INDEPENDENT_SCRIPT_PATH" value="true" />
@@ -288,20 +375,6 @@
       <option name="docutils_open_in_browser" value="false" />
       <method v="2" />
     </configuration>
-    <configuration name="Python tests in test_absorption.py" type="tests" factoryName="Autodetect" temporary="true" nameIsGenerated="true">
-      <module name="2023_05_02_PyCharmProject_Maths" />
-      <option name="INTERPRETER_OPTIONS" value="" />
-      <option name="PARENT_ENVS" value="true" />
-      <option name="SDK_HOME" value="" />
-      <option name="WORKING_DIRECTORY" value="$PROJECT_DIR$/tests" />
-      <option name="IS_MODULE_SDK" value="true" />
-      <option name="ADD_CONTENT_ROOTS" value="true" />
-      <option name="ADD_SOURCE_ROOTS" value="true" />
-      <option name="_new_additionalArguments" value="&quot;&quot;" />
-      <option name="_new_target" value="&quot;$PROJECT_DIR$/tests/test_absorption.py&quot;" />
-      <option name="_new_targetType" value="&quot;PATH&quot;" />
-      <method v="2" />
-    </configuration>
     <configuration name="Python tests in test_axiom_interpretation.py" type="tests" factoryName="Autodetect" temporary="true" nameIsGenerated="true">
       <module name="2023_05_02_PyCharmProject_Maths" />
       <option name="INTERPRETER_OPTIONS" value="" />
@@ -316,48 +389,6 @@
       <option name="_new_targetType" value="&quot;PATH&quot;" />
       <method v="2" />
     </configuration>
-    <configuration name="Python tests in test_biconditional_elimination_1.py" type="tests" factoryName="Autodetect" temporary="true" nameIsGenerated="true">
-      <module name="2023_05_02_PyCharmProject_Maths" />
-      <option name="INTERPRETER_OPTIONS" value="" />
-      <option name="PARENT_ENVS" value="true" />
-      <option name="SDK_HOME" value="" />
-      <option name="WORKING_DIRECTORY" value="$PROJECT_DIR$/tests" />
-      <option name="IS_MODULE_SDK" value="true" />
-      <option name="ADD_CONTENT_ROOTS" value="true" />
-      <option name="ADD_SOURCE_ROOTS" value="true" />
-      <option name="_new_additionalArguments" value="&quot;&quot;" />
-      <option name="_new_target" value="&quot;$PROJECT_DIR$/tests/test_biconditional_elimination_1.py&quot;" />
-      <option name="_new_targetType" value="&quot;PATH&quot;" />
-      <method v="2" />
-    </configuration>
-    <configuration name="Python tests in test_biconditional_elimination_2.py" type="tests" factoryName="Autodetect" temporary="true" nameIsGenerated="true">
-      <module name="2023_05_02_PyCharmProject_Maths" />
-      <option name="INTERPRETER_OPTIONS" value="" />
-      <option name="PARENT_ENVS" value="true" />
-      <option name="SDK_HOME" value="" />
-      <option name="WORKING_DIRECTORY" value="$PROJECT_DIR$/tests" />
-      <option name="IS_MODULE_SDK" value="true" />
-      <option name="ADD_CONTENT_ROOTS" value="true" />
-      <option name="ADD_SOURCE_ROOTS" value="true" />
-      <option name="_new_additionalArguments" value="&quot;&quot;" />
-      <option name="_new_target" value="&quot;$PROJECT_DIR$/tests/test_biconditional_elimination_2.py&quot;" />
-      <option name="_new_targetType" value="&quot;PATH&quot;" />
-      <method v="2" />
-    </configuration>
-    <configuration name="Python tests in test_biconditional_introduction.py" type="tests" factoryName="Autodetect" temporary="true" nameIsGenerated="true">
-      <module name="2023_05_02_PyCharmProject_Maths" />
-      <option name="INTERPRETER_OPTIONS" value="" />
-      <option name="PARENT_ENVS" value="true" />
-      <option name="SDK_HOME" value="" />
-      <option name="WORKING_DIRECTORY" value="$PROJECT_DIR$/tests" />
-      <option name="IS_MODULE_SDK" value="true" />
-      <option name="ADD_CONTENT_ROOTS" value="true" />
-      <option name="ADD_SOURCE_ROOTS" value="true" />
-      <option name="_new_additionalArguments" value="&quot;&quot;" />
-      <option name="_new_target" value="&quot;$PROJECT_DIR$/tests/test_biconditional_introduction.py&quot;" />
-      <option name="_new_targetType" value="&quot;PATH&quot;" />
-      <method v="2" />
-    </configuration>
     <configuration name="Python tests in tests" type="tests" factoryName="Autodetect">
       <module name="2023_05_02_PyCharmProject_Maths" />
       <option name="INTERPRETER_OPTIONS" value="" />
@@ -378,24 +409,24 @@
       <item itemvalue="Python.prebuild_generate_theory_reports" />
       <item itemvalue="Python.build" />
       <item itemvalue="Python.prebuild_generate_sample_outputs" />
+      <item itemvalue="Python.sample_biconditional_introduction" />
+      <item itemvalue="Python.sample_conjunction_elimination_1" />
+      <item itemvalue="Python.sample_conjunction_elimination_2" />
+      <item itemvalue="Python.sample_conjunction_introduction" />
       <item itemvalue="Python docs.Sphinx HTML" />
       <item itemvalue="Python tests.Python tests in tests" />
       <item itemvalue="Python tests.Python tests in test_axiom_interpretation.py" />
-      <item itemvalue="Python tests.Python tests in test_biconditional_elimination_1.py" />
-      <item itemvalue="Python tests.Python tests in test_biconditional_elimination_2.py" />
-      <item itemvalue="Python tests.Python tests in test_biconditional_introduction.py" />
-      <item itemvalue="Python tests.Python tests in test_absorption.py" />
       <item itemvalue="Shell Script.pytest tests" />
       <item itemvalue="Shell Script.pytest" />
       <item itemvalue="Shell Script.python -m build" />
     </list>
     <recent_temporary>
       <list>
+        <item itemvalue="Python.sample_conjunction_introduction" />
+        <item itemvalue="Python.sample_conjunction_elimination_2" />
+        <item itemvalue="Python.sample_conjunction_elimination_1" />
+        <item itemvalue="Python.sample_biconditional_introduction" />
         <item itemvalue="Python tests.Python tests in test_axiom_interpretation.py" />
-        <item itemvalue="Python tests.Python tests in test_absorption.py" />
-        <item itemvalue="Python tests.Python tests in test_biconditional_elimination_1.py" />
-        <item itemvalue="Python tests.Python tests in test_biconditional_elimination_2.py" />
-        <item itemvalue="Python tests.Python tests in test_biconditional_introduction.py" />
       </list>
     </recent_temporary>
   </component>
@@ -408,14 +439,6 @@
       <option name="presentableId" value="Default" />
       <updated>1687980987309</updated>
     </task>
-    <task id="LOCAL-00288" summary="#201 + #195">
-      <option name="closed" value="true" />
-      <created>1694899002452</created>
-      <option name="number" value="00288" />
-      <option name="presentableId" value="LOCAL-00288" />
-      <option name="project" value="LOCAL" />
-      <updated>1694899002452</updated>
-    </task>
     <task id="LOCAL-00289" summary="#201 + #195">
       <option name="closed" value="true" />
       <created>1694932915854</created>
@@ -800,7 +823,15 @@
       <option name="project" value="LOCAL" />
       <updated>1696305197720</updated>
     </task>
-    <option name="localTasksCounter" value="337" />
+    <task id="LOCAL-00337" summary="documentation #195 + inference validation #126 + support for the composition of collection-like formulae + usage of sequent-collection-comma to define inference-rules + enhanced exceptions with user-friendly reports + #220 interdiction of variable-substitution of propositional objects with non-propositional objects.">
+      <option name="closed" value="true" />
+      <created>1696331518332</created>
+      <option name="number" value="00337" />
+      <option name="presentableId" value="LOCAL-00337" />
+      <option name="project" value="LOCAL" />
+      <updated>1696331518332</updated>
+    </task>
+    <option name="localTasksCounter" value="338" />
     <servers />
   </component>
   <component name="Vcs.Log.Tabs.Properties">
diff --git a/src/punctilious/core.py b/src/punctilious/core.py
index 51f1873b..7ac67286 100644
--- a/src/punctilious/core.py
+++ b/src/punctilious/core.py
@@ -7052,22 +7052,21 @@ def __init__(self, t: TheoryElaborationSequence, echo: (None, bool) = None,
             abridged_name=abridged_name, name=name, explicit_name=explicit_name, echo=echo,
             proof=proof)
 
+    def check_premises_validity(self, p_and_q: FlexibleFormula) -> bool:
+        error_code: ErrorCode = error_codes.error_003_inference_premise_validity_error
+        # Validate that expected formula-statements are formula-statements in the current theory.
+        verify_formula_statement(arg='p_and_q', t=self.t, input_value=p_and_q,
+            form=self.i.parameter_p_and_q, mask=self.i.parameter_p_and_q_mask, raise_exception=True,
+            error_code=error_code)
+        # The method either raises an exception during validation, or return True.
+        return True
+
     def compose_paragraph_proof(self, o: InferredStatement) -> collections.abc.Generator[
         Composable, Composable, bool]:
         output = yield from configuration.locale.compose_conjunction_elimination_1_paragraph_proof(
             o=o)
         return output
 
-    def check_inference_validity(self, p_land_q: FormulaStatement = None,
-            t: TheoryElaborationSequence = None) -> bool:
-        verify(t.contains_theoretical_objct(p_land_q),
-            'Statement ⌜p_land_q⌝ must be contained in theory ⌜t⌝''s hierarchy.', p_land_q=p_land_q,
-            t=t, slf=self)
-        verify(p_land_q.relation is t.u.r.conjunction,
-            'The relation of formula ⌜p_land_q⌝ must be a conjunction.',
-            p_land_q_relation=p_land_q.relation, p_land_q=p_land_q, t=t, slf=self)
-        return True
-
     @property
     def i(self) -> ConjunctionElimination1Declaration:
         """Override the base class i property with a specialized inherited class type."""
@@ -7081,15 +7080,16 @@ def construct_formula(self, p_and_q: FlexibleFormula) -> Formula:
         """
         return self.i.construct_formula(p_and_q=p_and_q)
 
-    def infer_formula_statement(self, p_and_q: (None, FormulaStatement) = None,
-            ref: (None, str) = None, paragraph_header: (None, ParagraphHeader) = None,
-            subtitle: (None, str) = None, echo: (None, bool) = None) -> InferredStatement:
+    def infer_formula_statement(self, p_and_q: FlexibleFormula, ref: (None, str) = None,
+            paragraph_header: (None, ParagraphHeader) = None, subtitle: (None, str) = None,
+            echo: (None, bool) = None) -> InferredStatement:
         """
         .. include:: ../../include/infer_formula_statement_python_method.rstinc
 
         """
-        return super().infer_formula_statement(p_and_q, ref=ref, paragraph_header=paragraph_header,
-            subtitle=subtitle, echo=echo)
+        premises = self.i.Premises(p_and_q=p_and_q)
+        return InferredStatement(i=self, premises=premises, ref=ref,
+            paragraph_header=paragraph_header, subtitle=subtitle, echo=echo)
 
 
 class ConjunctionElimination2Inclusion(InferenceRuleInclusion):
@@ -7114,14 +7114,13 @@ def compose_paragraph_proof(self, o: InferredStatement) -> collections.abc.Gener
             o=o)
         return output
 
-    def check_inference_validity(self, p_land_q: FormulaStatement = None,
-            t: TheoryElaborationSequence = None) -> bool:
-        verify(t.contains_theoretical_objct(p_land_q),
-            'Statement ⌜p_land_q⌝ must be contained in theory ⌜t⌝''s hierarchy.', p_land_q=p_land_q,
-            t=t, slf=self)
-        verify(p_land_q.relation is t.u.r.conjunction,
-            'The relation of formula ⌜p_land_q⌝ must be a conjunction.',
-            p_land_q_relation=p_land_q.relation, p_land_q=p_land_q, t=t, slf=self)
+    def check_premises_validity(self, p_and_q: FlexibleFormula) -> bool:
+        error_code: ErrorCode = error_codes.error_003_inference_premise_validity_error
+        # Validate that expected formula-statements are formula-statements in the current theory.
+        verify_formula_statement(arg='p_and_q', t=self.t, input_value=p_and_q,
+            form=self.i.parameter_p_and_q, mask=self.i.parameter_p_and_q_mask, raise_exception=True,
+            error_code=error_code)
+        # The method either raises an exception during validation, or return True.
         return True
 
     @property
@@ -7137,7 +7136,7 @@ def construct_formula(self, p_and_q: FlexibleFormula) -> Formula:
         """
         return self.i.construct_formula(p_and_q=p_and_q)
 
-    def infer_formula_statement(self, p_and_q: (None, FormulaStatement) = None,
+    def infer_formula_statement(self, p_and_q: FlexibleFormula,
             nameset: (None, str, NameSet) = None, ref: (None, str) = None,
             paragraph_header: (None, ParagraphHeader) = None, subtitle: (None, str) = None,
             echo: (None, bool) = None) -> InferredStatement:
@@ -7145,7 +7144,8 @@ def infer_formula_statement(self, p_and_q: (None, FormulaStatement) = None,
         .. include:: ../../include/infer_formula_statement_python_method.rstinc
 
         """
-        return super().infer_formula_statement(p_and_q, nameset=nameset, ref=ref,
+        premises = self.i.Premises(p_and_q=p_and_q)
+        return InferredStatement(i=self, premises=premises, ref=ref,
             paragraph_header=paragraph_header, subtitle=subtitle, echo=echo)
 
 
@@ -7172,22 +7172,14 @@ def compose_paragraph_proof(self, o: InferredStatement) -> collections.abc.Gener
             o=o)
         return output
 
-    def check_inference_validity(self, p: FormulaStatement, q: FormulaStatement,
-            t: TheoryElaborationSequence) -> bool:
-        """Verify the correctness of the parameters provided to the :ref:`double-negation-introduction<double_negation_introduction_math_inference_rule>` :ref:`inference-rule<inference_rule_math_concept>` .
-
-        :param p: (mandatory) A formula-statement of the form :math:`P` .
-        :param q: (mandatory) A formula-statement of the form :math:`Q` .
-        :param t: (mandatory) The target theory-elaboration-sequence that must contain :math:`P` .
-
-        :return: True (bool) if the parameters are correct.
-        """
-        _, p, _ = verify_formula_statement(t=t, arity=None, input_value=p)
-        _, q, _ = verify_formula_statement(t=t, arity=None, input_value=q)
-        verify(t.contains_theoretical_objct(p),
-            'Statement ⌜p⌝ must be contained in theory ⌜t⌝''s hierarchy.', p=p, t=t, slf=self)
-        verify(t.contains_theoretical_objct(q),
-            'Statement ⌜q⌝ must be contained in theory ⌜t⌝''s hierarchy.', q=q, t=t, slf=self)
+    def check_premises_validity(self, p: FlexibleFormula, q: FlexibleFormula) -> bool:
+        error_code: ErrorCode = error_codes.error_003_inference_premise_validity_error
+        # Validate that expected formula-statements are formula-statements in the current theory.
+        verify_formula_statement(arg='p', t=self.t, input_value=p, raise_exception=True,
+            error_code=error_code)
+        verify_formula_statement(arg='q', t=self.t, input_value=q, raise_exception=True,
+            error_code=error_code)
+        # The method either raises an exception during validation, or return True.
         return True
 
     @property
@@ -7203,17 +7195,15 @@ def construct_formula(self, p: FlexibleFormula, q: FlexibleFormula) -> Formula:
         """
         return self.i.construct_formula(p=p, q=q)
 
-    def infer_formula_statement(self, p: (None, FormulaStatement) = None,
-            q: (None, FormulaStatement) = None, nameset: (None, str, NameSet) = None,
+    def infer_formula_statement(self, p: FlexibleFormula, q: FlexibleFormula,
             ref: (None, str) = None, paragraph_header: (None, ParagraphHeader) = None,
             subtitle: (None, str) = None, echo: (None, bool) = None) -> InferredStatement:
         """
         .. include:: ../../include/infer_formula_statement_python_method.rstinc
 
         """
-        _, p, _ = verify_formula_statement(t=self.t, arity=None, input_value=p)
-        _, q, _ = verify_formula_statement(t=self.t, arity=None, input_value=q)
-        return super().infer_formula_statement(p, q, nameset=nameset, ref=ref,
+        premises = self.i.Premises(p=p, q=q)
+        return InferredStatement(i=self, premises=premises, ref=ref,
             paragraph_header=paragraph_header, subtitle=subtitle, echo=echo)
 
 
diff --git a/src/sample/sample_conjunction_elimination_1.py b/src/sample/sample_conjunction_elimination_1.py
index 73b3986f..643c239a 100644
--- a/src/sample/sample_conjunction_elimination_1.py
+++ b/src/sample/sample_conjunction_elimination_1.py
@@ -13,7 +13,7 @@
 t1 = u.t(echo=True)
 theory_axiom = t1.include_axiom(axiom)
 phi1 = t1.i.axiom_interpretation.infer_formula_statement(a=theory_axiom,
-    formula=r1(o1, o2) | u.r.land | r2(o3))
+    p=r1(o1, o2) | u.r.land | r2(o3))
 
 # And finally, use the conjunction-elimination-1 inference-rule:
 proposition_of_interest = t1.i.conjunction_elimination_1.infer_formula_statement(p_and_q=phi1,
diff --git a/src/sample/sample_conjunction_elimination_2.py b/src/sample/sample_conjunction_elimination_2.py
index 8b100a94..1ad07317 100644
--- a/src/sample/sample_conjunction_elimination_2.py
+++ b/src/sample/sample_conjunction_elimination_2.py
@@ -13,7 +13,7 @@
 t1 = u.t(echo=True)
 theory_axiom = t1.include_axiom(axiom)
 phi1 = t1.i.axiom_interpretation.infer_formula_statement(a=theory_axiom,
-    formula=r1(o1, o2) | u.r.land | r2(o3))
+    p=r1(o1, o2) | u.r.land | r2(o3))
 
 # And finally, use the conjunction-elimination-2 inference-rule:
 proposition_of_interest = t1.i.conjunction_elimination_2.infer_formula_statement(p_and_q=phi1,
diff --git a/src/sample/sample_conjunction_introduction.py b/src/sample/sample_conjunction_introduction.py
index cfe7112f..36b67b8f 100644
--- a/src/sample/sample_conjunction_introduction.py
+++ b/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(a=theory_axiom, formula=r1(o1, o2))
-phi2 = t1.i.axiom_interpretation.infer_formula_statement(a=theory_axiom, formula=r2(o3))
+phi1 = t1.i.axiom_interpretation.infer_formula_statement(a=theory_axiom, p=r1(o1, o2))
+phi2 = t1.i.axiom_interpretation.infer_formula_statement(a=theory_axiom, p=r2(o3))
 
 # And finally, use the conjunction-introduction inference-rule:
 proposition_of_interest = t1.i.conjunction_introduction.infer_formula_statement(p=phi1, q=phi2,