Tags: inference-rule inclusion class python

InferenceRuleInclusion (python class)

class punctilious.InferenceRuleInclusion(i, t, symbol=None, index=None, auto_index=None, dashed_name=None, acronym=None, abridged_name=None, name=None, explicit_name=None, nameset=None, echo=None, proof=None)

This python abstract class models the inclusion of an inference-rule in a theory-derivation.

abstract property check_premises_validity

This python method verifies the validity of the premises. It is called by the python constructor of the InferredStatement python class to assure that formula-statements are inferred if and only if they are valid.

Returns True if the premises are valid and allow the execution of the inference algorithm. In this case, the constructor of the InferredStatement class will succeed and create an InferredStatement instance.

Returns False if the premises are not valid and do not allow the execution of the inference algorithm. In this case, the constructor of the InferredStatement class will fail and raise a PunctiliousException error.

Note

Note the critical distinction between the construct_formula and the infer_formula_statement methods. The former only verifies the syntactic correctness but does not verify the validity of the premises, it then applies the inference-rule algorithm, and produces a formula that may be invalid . The later verifies the validity of the premises, applies the inference-rule algorithm, and produces a formula-statement that is valid by definition.

Taking the modus-ponens inference-rule as an example, the construct_formula method requires two premise arguments: p_implies_q and p. One may pass a formula as the p_implies_q argument that is not valid in the theory-derivation under consideration, but that is syntactically correct. On the other hand, the infer_formula_statement method requires that both premise arguments be valid.

This distinction makes it possible to use the algorithms of inference-rules in “what if” scenarii, i.e. building invalid formulae. And at the same time, it assures that all formula_statements are valid.

compose_class()

This python method yields the default mathematical-class of the object in the punctilious data model.

Return type: Generator[Composable, None, None]

compose_report(proof=None, **kwargs)

This python method yields a human-readable formal report on the object.

Parameters

proof – True if the report must include a formal proof. False otherwise.
kwargs –

Returns

abstract property construct_formula: punctilious.core.CompoundFormula

This python method verify the syntactic correctness of the premises, but does not verify the validity of the premises, it then applies the inference-rule algorithm, and returns a formula.

Note

Note the critical distinction between the construct_formula and the infer_formula_statement methods. The former only verifies the syntactic correctness but does not verify the validity of the premises, it then applies the inference-rule algorithm, and produces a formula that may be invalid . The later verifies the validity of the premises, applies the inference-rule algorithm, and produces a formula-statement that is valid by definition.

Taking the modus-ponens inference-rule as an example, the construct_formula method requires two premise arguments: p_implies_q and p. One may pass a formula as the p_implies_q argument that is not valid in the theory-derivation under consideration, but that is syntactically correct. On the other hand, the infer_formula_statement method requires that both premise arguments be valid.

This distinction makes it possible to use the algorithms of inference-rules in “what if” scenarii, i.e. building invalid formulae. And at the same time, it assures that all formula_statements are valid.

Return type: CompoundFormula

property definition: punctilious.core.CompoundFormula

This python property returns a formal definition of the object.

Return type: CompoundFormula
Returns: a formula.

property i

Returns

abstract property infer_formula_statement: punctilious.core.InferredStatement

This python method verifies the syntactic correctness and validity of the premises, it then applies the inference-rule algorithm, and returns a formula-statement.

Note

Note the critical distinction between the construct_formula and the infer_formula_statement methods. The former only verifies the syntactic correctness but does not verify the validity of the premises, it then applies the inference-rule algorithm, and produces a formula that may be invalid . The later verifies the validity of the premises, applies the inference-rule algorithm, and produces a formula-statement that is valid by definition.

Taking the modus-ponens inference-rule as an example, the construct_formula method requires two premise arguments: p_implies_q and p. One may pass a formula as the p_implies_q argument that is not valid in the theory-derivation under consideration, but that is syntactically correct. On the other hand, the infer_formula_statement method requires that both premise arguments be valid.

This distinction makes it possible to use the algorithms of inference-rules in “what if” scenarii, i.e. building invalid formulae. And at the same time, it assures that all formula_statements are valid.

Return type: InferredStatement

property is_strictly_propositional: bool

By definition, an inference-rule-inclusion is not a propositional object.

Return type: bool