propositions.soundness module

Programmatic proof of the soundness of Propositional Logic.

propositions.soundness.rule_nonsoundness_from_specialization_nonsoundness(general, specialization, model)

Demonstrates the non-soundness of the given general inference rule given an example of the non-soundness of the given specialization of this rule.

Parameters

  • general (InferenceRule) – inference rule to the soundness of which to find a counterexample.

  • specialization (InferenceRule) – non-sound specialization of general.

  • model (Mapping[str, bool]) – model in which specialization does not hold.

Return type

Mapping[str, bool]

Returns

A model in which general does not hold.

propositions.soundness.nonsound_rule_of_nonsound_proof(proof, model)

Finds a non-sound inference rule used by the given valid proof of a non-sound inference rule, and demonstrates the non-soundness of the former rule.

Parameters

  • proof (Proof) – valid proof of a non-sound inference rule.

  • model (Mapping[str, bool]) – model in which the inference rule proved by the given proof does not hold.

Return type

Tuple[InferenceRule, Mapping[str, bool]]

Returns

A pair of a non-sound inference rule used in the given proof and a model in which this rule does not hold.