Tags: inference-rule declaration class python

InferenceRuleDeclaration (python class)

class punctilious.InferenceRuleDeclaration(u, definition=None, compose_paragraph_proof_method=None, symbol=None, index=None, auto_index=None, dashed_name=None, acronym=None, abridged_name=None, name=None, explicit_name=None, ref=None, subtitle=None, echo=None)

This python abstract class models the declaration of an inference-rule in a universe-of-discourse.

compose_paragraph_proof(**kwargs)

This python method yields a paragraph-proof that demonstrates the validity of the object.

This method should be overridden by specialized inference-rule classes to provide accurate proofs.

Return type

Generator[Composable, Composable, bool]

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.

echo()

This python method prints the object to the console (sys.stdout).

Returns

property is_strictly_propositional: bool

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

Return type

bool