propositions.soundness module¶
Programmatic proof of the soundness of Propositional Logic.

propositions.soundness.
rule_nonsoundness_from_specialization_nonsoundness
(general, specialization, model)¶ Demonstrated the nonsoundness of the given general inference rule given an example of the nonsoundness of the given specialization of this rule.
 Parameters
general (
InferenceRule
) – inference rule to the soundness of which to find a counterexample.specialization (
InferenceRule
) – nonsound specialization ofgeneral
.model (
Mapping
[str
,bool
]) – model in whichspecialization
does not hold.
 Return type
 Returns
A model in which
general
does not hold.

propositions.soundness.
nonsound_rule_of_nonsound_proof
(proof, model)¶ Finds a nonsound inference rule used by the given valid proof of a nonsound inference rule, and demonstrates the nonsoundness of the former rule.
 Parameters
 Return type
Tuple
[InferenceRule
,Mapping
[str
,bool
]] Returns
A pair of a nonsound inference rule used in the given proof and a model in which this rule does not hold.