p_implies_q – A formula-statement of the
- form: (P ⟹ Q).
-
t – The current
- theory-elaboration-sequence.
-
-
-
Returns:
-
The (proven) formula: (P ⟹ (P ∧ Q)).
-
-
+
This python method does not verify the validity of the
+ arguments, applies the inference-rule algorithm, and returns
+ a formula.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
p_implies_q – (mandatory) The
- implication statement.
-
-
Returns:
-
The inferred formula q.
-
-
+
This python method does not verify the validity of the
+ arguments, applies the inference-rule algorithm, and returns
+ a formula.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
Apply the absorption inference-rule and return the
- inferred-statement.
-
-
Parameters:
-
p_implies_q – (mandatory) The
- implication statement.
-
-
Returns:
-
An inferred-statement proving p implies p and
- q in the current theory.
-
-
+
This python method verifies the validity of the arguments, applies the inference-rule algorithm, and returns a
+ formula-statement.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
p_implies_q – A formula-statement of the
- form: (P ⟹ Q).
-
t – The current
- theory-elaboration-sequence.
-
-
-
Returns:
-
The (proven) formula: (P ⟹ (P ∧ Q)).
-
-
+
This python method does not verify the validity of the
+ arguments, applies the inference-rule algorithm, and returns
+ a formula.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
This python method does not verify the validity of the
+ arguments, applies the inference-rule algorithm, and returns
+ a formula.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
Apply the biconditional elimination #1 inference-rule and return the
- inferred-statement.
-
-
Parameters:
-
p_iff_q – (mandatory) The
- biconditional statement.
-
-
Returns:
-
The proven inferred-statement p implies q in
- the current theory.
-
-
+
This python method verifies the validity of the arguments, applies the inference-rule algorithm, and returns a
+ formula-statement.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
p_iff_q – A formula-statement of the
- form: (P ⟺ Q).
-
t – The current
- theory-elaboration-sequence.
-
-
-
Returns:
-
The (proven) formula: (Q ⟹ P).
-
-
+
This python method does not verify the validity of the
+ arguments, applies the inference-rule algorithm, and returns
+ a formula.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
This python method does not verify the validity of the
+ arguments, applies the inference-rule algorithm, and returns
+ a formula.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
Apply the biconditional elimination #2 inference-rule and return the
- inferred-statement.
-
-
Parameters:
-
p_iff_q – (mandatory) The
- biconditional statement.
-
-
Returns:
-
The proven inferred-statement p implies q in
- the current theory.
-
-
+
This python method verifies the validity of the arguments, applies the inference-rule algorithm, and returns a
+ formula-statement.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
Infer formula (P ⟺ Q) from formulae (P ⟹ Q), and (Q ⟹ P).
+
This python method does not verify the validity of the
+ arguments, applies the inference-rule algorithm, and returns
+ a formula.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
This python method does not verify the validity of the
+ arguments, applies the inference-rule algorithm, and returns
+ a formula.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
Apply the biconditional elimination #2 inference-rule and return the
- inferred-statement.
-
-
Parameters:
-
p_iff_q – (mandatory) The
- biconditional statement.
-
-
Returns:
-
The proven inferred-statement p implies q in
- the current theory.
-
-
+
This python method verifies the validity of the arguments, applies the inference-rule algorithm, and returns a
+ formula-statement.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
p_land_q – A formula-statement of the
- form: (P ⋀ Q).
-
t – The current
- theory-elaboration-sequence.
-
echo –
-
-
-
Returns:
-
The (proven) formula: P.
-
-
+
This python method does not verify the validity of the
+ arguments, applies the inference-rule algorithm, and returns
+ a formula.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
This python method does not verify the validity of the
+ arguments, applies the inference-rule algorithm, and returns
+ a formula.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
Apply the conjunction elimination #1 inference-rule and return the
- inferred-statement.
-
-
Parameters:
-
p_and_q –
-
-
Returns:
-
The proven inferred-statement p implies q in
- the current theory.
-
-
+
This python method verifies the validity of the arguments, applies the inference-rule algorithm, and returns a
+ formula-statement.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
p_land_q – A formula-statement of the
- form: (P ∧ Q).
-
t – The current
- theory-elaboration-sequence.
-
-
-
Returns:
-
The (proven) formula: Q.
-
-
+
This python method does not verify the validity of the
+ arguments, applies the inference-rule algorithm, and returns
+ a formula.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
This python method does not verify the validity of the
+ arguments, applies the inference-rule algorithm, and returns
+ a formula.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
Apply the conjunction elimination #2 inference-rule and return the
- inferred-statement.
-
-
Parameters:
-
p_and_q – (mandatory) The
- conjunction statement.
-
-
Returns:
-
The proven inferred-statement p implies q in
- the current theory.
-
-
+
This python method verifies the validity of the arguments, applies the inference-rule algorithm, and returns a
+ formula-statement.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
p – (mandatory) A formula-statement of
- the form \(P\) .
-
-
q – (mandatory) A formula-statement of
- the form \(Q\) .
-
-
t – (mandatory) The target
- theory-elaboration-sequence that must contain \(P\) .
-
-
echo –
-
-
-
Returns:
-
The resulting formula \(\left( P \land Q \right)\)
- .
-
-
+
This python method does not verify the validity of the
+ arguments, applies the inference-rule algorithm, and returns
+ a formula.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
p – (mandatory) A formula-statement of
- the form \(P\) .
-
-
q – (mandatory) A formula-statement of
- the form \(Q\) .
-
-
echo –
-
-
-
Returns:
-
The resulting formula \(\left( P \land Q \right)\)
- .
-
-
+
This python method does not verify the validity of the
+ arguments, applies the inference-rule algorithm, and returns
+ a formula.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
p – (mandatory) A formula-statement of
- the form: \(P\) .
-
-
q – (mandatory) A formula-statement of
- the form: \(Q\) .
-
-
nameset –
-
ref –
-
paragraph_header –
-
subtitle –
-
echo –
-
-
-
Returns:
-
The resulting inferred-statement: \(\left( P \land Q \right)\)
- .
-
-
+ class="std std-ref">inference-rule algorithm, and returns a
+ formula-statement.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
p – (mandatory) A formula-statement of
- the form \(P\) .
-
-
q – (mandatory) A formula of the form
- \(Q\) .
-
-
t – (mandatory) The target
- theory-elaboration-sequence that must contain \(P\) .
-
-
echo –
-
-
-
Returns:
-
The resulting formula \(\left( Q \lor P \right)\)
- .
-
-
+
This python method does not verify the validity of the
+ arguments, applies the inference-rule algorithm, and returns
+ a formula.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
p – (mandatory) A formula-statement of
- the form \(P\) .
-
-
q – (mandatory) A formula of the form
- \(Q\) .
-
-
echo –
-
-
-
Returns:
-
The resulting formula \(\left( P \lor Q \right)\)
- .
-
-
+
This python method does not verify the validity of the
+ arguments, applies the inference-rule algorithm, and returns
+ a formula.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
p – (mandatory) A formula-statement of
- the form: \(P\) .
-
-
q – (mandatory) A formula of the form:
- \(Q\) .
-
-
nameset –
-
ref –
-
paragraph_header –
-
subtitle –
-
echo –
-
-
-
Returns:
-
The resulting inferred-statement: \(\left( P \lor Q \right)\)
- .
-
-
+ class="std std-ref">inference-rule algorithm, and returns a
+ formula-statement.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
p – (mandatory) A formula-statement of
- the form \(P\) .
-
-
q – (mandatory) A formula of the form
- \(Q\) .
-
-
t – (mandatory) The target
- theory-elaboration-sequence that must contain \(P\) .
-
-
echo –
-
-
-
Returns:
-
The resulting formula \(\left( P \lor Q \right)\)
- .
-
-
+
This python method does not verify the validity of the
+ arguments, applies the inference-rule algorithm, and returns
+ a formula.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
p – (mandatory) A formula-statement of
- the form \(P\) .
-
-
q – (mandatory) A formula of the form
- \(Q\) .
-
-
echo –
-
-
-
Returns:
-
The resulting formula \(\left( P \lor Q \right)\)
- .
-
-
+
This python method does not verify the validity of the
+ arguments, applies the inference-rule algorithm, and returns
+ a formula.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
p – (mandatory) A formula-statement of
- the form: \(P\) .
-
-
q – (mandatory) A formula of the form:
- \(Q\) .
-
-
nameset –
-
ref –
-
paragraph_header –
-
subtitle –
-
echo –
-
-
-
Returns:
-
The resulting inferred-statement: \(\left( P \lor Q \right)\)
- .
-
-
+ class="std std-ref">inference-rule algorithm, and returns a
+ formula-statement.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
not_not_p – A formula-statement of the
- form: ¬(¬(P)).
-
t – The current
- theory-elaboration-sequence.
-
-
-
Returns:
-
The (proven) formula: P.
-
-
+
This python method does not verify the validity of the
+ arguments, applies the inference-rule algorithm, and returns
+ a formula.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
Apply the double-negation-elimination inference-rule and return the
- inferred-formula.
+
This python method does not verify the validity of the
+ arguments, applies the inference-rule algorithm, and returns
+ a formula.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
Apply the double-negation-elimination inference-rule and return the
- inferred-statement.
-
-
Parameters:
-
not_not_p – (mandatory)
-
-
Returns:
-
An inferred-statement proving p in the current
- theory.
-
-
+
This python method verifies the validity of the arguments, applies the inference-rule algorithm, and returns a
+ formula-statement.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
p – (mandatory) A formula-statement of
- the form \(P\) .
-
-
t – (mandatory) The target
- theory-elaboration-sequence that must contain \(P\) .
-
-
echo –
-
-
-
Returns:
-
The resulting formula \(\lnot \left( \lnot \left( P \right) \right)\)
- .
-
-
+
This python method does not verify the validity of the
+ arguments, applies the inference-rule algorithm, and returns
+ a formula.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
p – (mandatory) A formula or
- formula-statement of the form: \(P\) .
-
-
echo –
-
-
-
Returns:
-
The resulting formula: \(\lnot \left( \lnot \left( P \right) \right)\)
- .
-
-
+
This python method does not verify the validity of the
+ arguments, applies the inference-rule algorithm, and returns
+ a formula.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
p – (mandatory) A formula-statement of
- the form: \(P\) .
-
-
nameset –
-
ref –
-
paragraph_header –
-
subtitle –
-
echo –
-
-
-
Returns:
-
The resulting inferred-statement: \(\lnot \left( \lnot \left( P \right) \right)\)
- .
-
-
+ class="std std-ref">inference-rule algorithm, and returns a
+ formula-statement.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
Apply the inference-rule equal-terms-substitution and return the inferred
- formula.
-
-
Parameters:
-
-
-
p – a formula-statement of the form: P.
-
-
x_equal_y – an equality
- formula-statement of the form: (Q = R).
-
-
-
Returns:
-
(FormulaStatement) The formula-statement P
- modified such that all occurrences of Q in P are replaced with
- R.
-
-
+
This python method does not verify the validity of the
+ arguments, applies the inference-rule algorithm, and returns
+ a formula.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
Apply the equal-terms-substitution inference-rule and return the
- inferred-formula.
+
This python method does not verify the validity of the
+ arguments, applies the inference-rule algorithm, and returns
+ a formula.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
This python method verifies the validity of the arguments, applies the inference-rule algorithm, and returns a
+ formula-statement.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
Apply the inference-rule equality-commutativity and return the inferred
- formula.
-
-
Parameters:
-
x_equal_y – an equality
- formula-statement of the form: (P = Q).
-
-
Returns:
-
(FormulaStatement) The inferred-statement (Q =
- P).
-
-
+
This python method does not verify the validity of the
+ arguments, applies the inference-rule algorithm, and returns
+ a formula.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
Apply the equality-commutativity inference-rule and return the
- inferred-formula.
+
This python method does not verify the validity of the
+ arguments, applies the inference-rule algorithm, and returns
+ a formula.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
This python method verifies the validity of the arguments, applies the inference-rule algorithm, and returns a
+ formula-statement.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
Apply this inference-rules on input statements and return the resulting
- statement.
+
This python method does not verify the validity of the
+ arguments, applies the inference-rule algorithm, and returns
+ a formula.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
Apply the inconsistency-introduction inference-rule and return the
- inferred-formula.
+
This python method does not verify the validity of the
+ arguments, applies the inference-rule algorithm, and returns
+ a formula.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
Apply the inconsistency-introduction inference-rule and return the
- inferred-statement.
-
-
Parameters:
-
-
-
p – (mandatory) .
-
not_p – (mandatory) .
-
inconsistent_theory – (conditional) .
-
-
-
-
Returns:
-
An inferred-statement proving p in the current
- theory.
-
-
+
This python method verifies the validity of the arguments, applies the inference-rule algorithm, and returns a
+ formula-statement.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
Apply this inference-rules on input statements and return the resulting
- statement.
+
This python method does not verify the validity of the
+ arguments, applies the inference-rule algorithm, and returns
+ a formula.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
Apply the inconsistency-introduction inference-rule and return the
- inferred-formula.
+
This python method does not verify the validity of the
+ arguments, applies the inference-rule algorithm, and returns
+ a formula.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
Apply the inconsistency-introduction inference-rule and return the
- inferred-statement.
-
-
Parameters:
-
-
-
p – (mandatory) .
-
not_p – (mandatory) .
-
inconsistent_theory – (conditional) .
-
-
-
-
Returns:
-
An inferred-statement proving p in the current
- theory.
-
-
+
This python method verifies the validity of the arguments, applies the inference-rule algorithm, and returns a
+ formula-statement.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
Apply this inference-rules on input statements and return the resulting
- statement.
+
This python method does not verify the validity of the
+ arguments, applies the inference-rule algorithm, and returns
+ a formula.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
Apply the inconsistency-introduction inference-rule and return the
- inferred-formula.
+
This python method does not verify the validity of the
+ arguments, applies the inference-rule algorithm, and returns
+ a formula.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
Apply the inconsistency-introduction inference-rule and return the
- inferred-statement.
-
-
Parameters:
-
-
-
p – (mandatory) .
-
not_p – (mandatory) .
-
inconsistent_theory – (conditional) .
-
-
-
-
Returns:
-
An inferred-statement proving p in the current
- theory.
-
-
+
This python method verifies the validity of the arguments, applies the inference-rule algorithm, and returns a
+ formula-statement.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
In complement, it conveniently exposes as python properties a catalog of natively
+ supported inference-rules that are automatically declared in the universe-of-discourse when they are
+ accessed for the first time.
This python method does not verify the validity of the
+ arguments, applies the inference-rule algorithm, and returns
+ a formula.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
In complement, it conveniently exposes as python properties a catalog of natively
+ supported inference-rules that are automatically included in the theory-elaboration-sequence when they are
+ accessed for the first time.
Axiom-interpretation is especially dangerous because, contrary to
+ most
+ inference-rules,
+ it allows the introduction of arbitrary truthes in the theory. For
+ this reason,
+ one must be very attentive when applying this inference-rule to
+ assure the resulting
+ formula-statement complies / interprets properly its related
+ contentual-axiom.
Axiom-interpretation is especially dangerous because, contrary to
+ most inference-rules,
+ it allows the introduction of arbitrary truthes in the theory. For
+ this reason,
+ one must be very attentive when applying this inference-rule to
+ assure the resulting
+ formula-statement complies / interprets properly its related
+ contentual-definition.
The well-known modus-ponens inference-rule: (P ⟹ Q), P ⊢ Q.
+
Abridged property: u.i.mp
+
The implication (P ⟹ Q) may contain free-variables. If such is the
+ case, the resulting Q’ is computed by extracting variable-values
+ from P’ and applying variable-substitution.
+
If the well-known inference-rule does not exist in the
+ universe-of-discourse,
+ the inference-rule is automatically declared.
This python method does not verify the validity of the
+ arguments, applies the inference-rule algorithm, and returns
+ a formula.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
This python method verifies the validity of the arguments, applies the inference-rule algorithm, and returns a
+ formula-statement.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
This python method does not verify the validity of the
+ arguments, applies the inference-rule algorithm, and returns
+ a formula.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
Apply the modus-ponens inference-rule and return the
- inferred-formula.
-
-
Parameters:
-
-
-
p_implies_q – (mandatory) The
- implication statement.
-
p – (mandatory) The p statement, proving
- that p is true in the current theory.
-
-
-
Returns:
-
The inferred formula q.
-
-
+
This python method does not verify the validity of the
+ arguments, applies the inference-rule algorithm, and returns
+ a formula.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
Apply the modus-ponens inference-rule and return the
- inferred-statement.
-
-
Parameters:
-
-
-
p_implies_q – (mandatory) The
- implication statement.
-
p – (mandatory) The p statement, proving
- that p is true in the current theory.
-
-
-
Returns:
-
An inferred-statement proving p in the current
- theory.
-
-
+
This python method verifies the validity of the arguments, applies the inference-rule algorithm, and returns a
+ formula-statement.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
Apply this inference-rules on input statements and return the resulting
- statement.
+
This python method does not verify the validity of the
+ arguments, applies the inference-rule algorithm, and returns
+ a formula.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
Apply the proof-by-contradiction inference-rule and return the
- inferred-formula.
-
-
Parameters:
-
-
-
not_p_hypothesis – (mandatory) The (¬P)
- hypothesis-statement.
-
inc_hypothesis – (mandatory) The proof
- of inconsistency of the not_p hypothetical-theory: Inc(¬P).
-
-
-
-
Returns:
-
The inferred formula .
-
-
+
This python method does not verify the validity of the
+ arguments, applies the inference-rule algorithm, and returns
+ a formula.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
Apply the modus-ponens inference-rule and return the
- inferred-statement.
-
-
Parameters:
-
-
-
not_p_hypothesis – (mandatory) The
- implication statement.
-
inc_hypothesis – (mandatory) The p
- statement, proving that p is true in the current theory.
-
-
-
-
Returns:
-
An inferred-statement proving p in the current
- theory.
-
-
+
This python method verifies the validity of the arguments, applies the inference-rule algorithm, and returns a
+ formula-statement.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
Apply this inference-rules on input statements and return the resulting
- statement.
+
This python method does not verify the validity of the
+ arguments, applies the inference-rule algorithm, and returns
+ a formula.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
This python method does not verify the validity of the
+ arguments, applies the inference-rule algorithm, and returns
+ a formula.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
This python method verifies the validity of the arguments, applies the inference-rule algorithm, and returns a
+ formula-statement.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
Apply this inference-rules on input statements and return the resulting
- statement.
+
This python method does not verify the validity of the
+ arguments, applies the inference-rule algorithm, and returns
+ a formula.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
p_hypothesis – (mandatory) The \(\neg \mathbf{P}\)
- hypothesis.
-
inc_hypothesis – (mandatory) The proof
- of inconsistency of the \(\neg \mathbf{P}\)
- hypothesis \(Inc\left(\mathcal{H}\right)\)
- .
-
echo –
-
-
-
Returns:
-
The inferred formula: \(\mathbf{P}\) .
-
-
+
This python method does not verify the validity of the
+ arguments, applies the inference-rule algorithm, and returns
+ a formula.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
Apply the modus-ponens inference-rule and return the
- inferred-statement.
-
-
Parameters:
-
-
-
p_hypothesis – (mandatory) The
- implication statement.
-
inc_hypothesis – (mandatory) The p
- statement, proving that p is true in the current theory.
-
-
-
-
Returns:
-
An inferred-statement proving p in the current
- theory.
-
-
+
This python method verifies the validity of the arguments, applies the inference-rule algorithm, and returns a
+ formula-statement.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
Apply this inference-rules on input statements and return the resulting
- statement.
+
This python method does not verify the validity of the
+ arguments, applies the inference-rule algorithm, and returns
+ a formula.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
This python method does not verify the validity of the
+ arguments, applies the inference-rule algorithm, and returns
+ a formula.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
This python method verifies the validity of the arguments, applies the inference-rule algorithm, and returns a
+ formula-statement.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
Compute the formula that results from applying this inference-rule with
- those arguments.
-
-
Parameters:
-
-
-
p – A formula statement that may contain
- n variables.
-
phi – A sequence of n well-formed
- formulae.
-
t – The current
- theory-elaboration-sequence.
-
-
-
Returns:
-
(Formula) The inferred formula.
-
-
+
This python method does not verify the validity of the
+ arguments, applies the inference-rule algorithm, and returns
+ a formula.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
This python method does not verify the validity of the
+ arguments, applies the inference-rule algorithm, and returns
+ a formula.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.
Apply the variable-substitution inference-rule and return the
- inferred-statement.
-
-
Parameters:
-
-
-
p –
-
phi –
-
nameset –
-
ref –
-
paragraph_header –
-
subtitle –
-
echo –
-
-
-
Returns:
-
-
-
+
This python method verifies the validity of the arguments, applies the inference-rule algorithm, and returns a
+ formula-statement.
+
+
Note
+
Note the critical distinction between the infer_formula and the infer_formula_statement methods. The
+ former does not verify the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula that may be invalid
+ . The later verifies the validity of the arguments, applies the inference-rule algorithm, and
+ produces a formula-statement that is
+ valid by definition.