propositions.proofs module

Proofs by deduction in Propositional Logic.

propositions.proofs.SpecializationMap

A mapping from variable names to formulas.

alias of Mapping[str, propositions.syntax.Formula]

class propositions.proofs.InferenceRule(assumptions, conclusion)

Bases: object

An immutable inference rule in Propositional Logic, comprised of zero or more assumed propositional formulas, and a conclusion propositional formula.

Variables
  • assumptions (Tuple[Formula, …]) – the assumptions of the rule.

  • conclusion (Formula) – the conclusion of the rule.

__init__(assumptions, conclusion)

Initializes an InferenceRule from its assumptions and conclusion.

Parameters
  • assumptions (Sequence[Formula]) – the assumptions for the rule.

  • conclusion (Formula) – the conclusion for the rule.

__repr__()

Computes a string representation of the current inference rule.

Return type

str

Returns

A string representation of the current inference rule.

__eq__(other)

Compares the current inference rule with the given one.

Parameters

other (object) – object to compare to.

Return type

bool

Returns

True if the given object is an InferenceRule object that equals the current inference rule, False otherwise.

__ne__(other)

Compares the current inference rule with the given one.

Parameters

other (object) – object to compare to.

Return type

bool

Returns

True if the given object is not an InferenceRule object or does not does not equal the current inference rule, False otherwise.

variables()

Finds all variable names in the current inference rule.

Return type

Set[str]

Returns

A set of all variable names used in the assumptions and in the conclusion of the current inference rule.

specialize(specialization_map)

Specializes the current inference rule by simultaneously substituting each variable name v that is a key in specialization_map with the formula specialization_map[v].

Parameters

specialization_map (Mapping[str, Formula]) – mapping defining the specialization to be performed.

Return type

InferenceRule

Returns

The resulting inference rule.

static _merge_specialization_maps(specialization_map1, specialization_map2)

Merges the given specialization maps while checking their consistency.

Parameters
Return type

Optional[Mapping[str, Formula]]

Returns

A single mapping containing all (key, value) pairs that appear in either of the given maps, or None if one of the given maps is None or if some key appears in both given maps but with different values.

static _formula_specialization_map(general, specialization)

Computes the minimal specialization map by which the given formula specializes to the given specialization.

Parameters
  • general (Formula) – non-specialized formula for which to compute the map.

  • specialization (Formula) – specialization for which to compute the map.

Return type

Optional[Mapping[str, Formula]]

Returns

The computed specialization map, or None if specialization is in fact not a specialization of general.

specialization_map(specialization)

Computes the minimal specialization map by which the current inference rule specializes to the given specialization.

Parameters

specialization (InferenceRule) – specialization for which to compute the map.

Return type

Optional[Mapping[str, Formula]]

Returns

The computed specialization map, or None if specialization is in fact not a specialization of the current rule.

is_specialization_of(general)

Checks if the current inference rule is a specialization of the given inference rule.

Parameters

general (InferenceRule) – non-specialized inference rule to check.

Return type

bool

Returns

True if the current inference rule is a specialization of general, False otherwise.

class propositions.proofs.Proof(statement, rules, lines)

Bases: object

An immutable deductive proof in Propositional Logic, comprised of a statement in the form of an inference rule, a set of inference rules that may be used in the proof, and a list of lines that prove the statement via these inference rules.

Variables
__init__(statement, rules, lines)

Initializes a Proof from its statement, allowed inference rules, and lines.

Parameters
class Line(formula, rule=None, assumptions=None)

Bases: object

An immutable line in a deductive proof, comprised of a formula that is justified either as an assumption of the proof, or as the conclusion of a specialization of an allowed inference rule of the proof, the assumptions of which are justified by previous lines in the proof.

Variables
  • formula (Formula) – the formula justified by the line.

  • rule (Optional[InferenceRule]) – the inference rule, out of those allowed in the proof, that has a specialization that concludes the formula; or None if the formula is justified as an assumption of the proof.

  • assumptions (Optional[Tuple[int]) – tuple of zero or more numbers of previous lines in the proof whose formulas are the respective assumptions of the specialization of the rule that concludes the formula, if the formula is not justified as an assumption of the proof.

__init__(formula, rule=None, assumptions=None)

Initializes a Line from its formula, and optionally its rule and numbers of justifying previous lines.

Parameters
  • formula (Formula) – the formula to be justified by the line.

  • rule (Optional[InferenceRule]) – the inference rule, out of those allowed in the proof, that has a specialization that concludes the formula; or None if the formula is to be justified as an assumption of the proof.

  • assumptions (Optional[Sequence[int]]) – numbers of previous lines in the proof whose formulas are the respective assumptions of the specialization of the rule that concludes the formula, or None if the formula is to be justified as an assumption of the proof.

__repr__()

Computes a string representation of the current line.

Return type

str

Returns

A string representation of the current line.

is_assumption()

Checks if the current proof line is justified as an assumption of the proof.

Return type

bool

Returns

True if the current proof line is justified as an assumption of the proof, False otherwise.

__repr__()

Computes a string representation of the current proof.

Return type

str

Returns

A string representation of the current proof.

rule_for_line(line_number)

Computes the inference rule whose conclusion is the formula justified by the specified line, and whose assumptions are the formulas justified by the lines specified as the assumptions of that line.

Parameters

line_number (int) – number of the line according to which to compute the inference rule.

Return type

Optional[InferenceRule]

Returns

The computed inference rule, with assumptions ordered in the order of their numbers in the specified line, or None if the specified line is justified as an assumption.

is_line_valid(line_number)

Checks if the specified line validly follows from its justifications.

Parameters

line_number (int) – number of the line to check.

Return type

bool

Returns

If the specified line is justified as an assumption, then True if the formula justified by this line is an assumption of the current proof, False otherwise. Otherwise (i.e., if the specified line is justified as a conclusion of an inference rule), True if the rule specified for that line is one of the allowed inference rules in the current proof, and it has a specialization that satisfies all of the following:

  1. The conclusion of that specialization is the formula justified by that line.

  2. The assumptions of this specialization are the formulas justified by the lines that are specified as the assumptions of that line (in the order of their numbers in that line), all of which must be previous lines.

is_valid()

Checks if the current proof is a valid proof of its claimed statement via its inference rules.

Return type

bool

Returns

True if the current proof is a valid proof of its claimed statement via its inference rules, False otherwise.

propositions.proofs.prove_specialization(proof, specialization)

Converts the given proof of an inference rule to a proof of the given specialization of that inference rule.

Parameters
  • proof (Proof) – valid proof to convert.

  • specialization (InferenceRule) – specialization of the rule proven by the given proof.

Return type

Proof

Returns

A valid proof of the given specialization via the same inference rules as the given proof.

propositions.proofs._inline_proof_once(main_proof, line_number, lemma_proof)

Inlines the given proof of a “lemma” inference rule into the given proof that uses that “lemma” rule, eliminating the usage of (a specialization of) that “lemma” rule in the specified line in the latter proof.

Parameters
  • main_proof (Proof) – valid proof to inline into.

  • line_number (int) – number of the line in main_proof that should be replaced.

  • lemma_proof (Proof) – valid proof of the inference rule of the specified line (an allowed inference rule of main_proof).

Return type

Proof

Returns

A valid proof obtained by replacing the specified line in main_proof with a full (specialized) list of lines proving the formula of the specified line from the lines specified as the assumptions of that line, and updating justification line numbers specified throughout the proof to maintain the validity of the proof. The set of allowed inference rules in the returned proof is the union of the rules allowed in the two given proofs, but the “lemma” rule that is used in the specified line in main_proof is no longer used in the corresponding lines in the returned proof (and thus, this “lemma” rule is used one less time in the returned proof than in main_proof).

propositions.proofs.inline_proof(main_proof, lemma_proof)

Inlines the given proof of a “lemma” inference rule into the given proof that uses that “lemma” rule, eliminating all usages of (any specializations of) that “lemma” rule in the latter proof.

Parameters
  • main_proof (Proof) – valid proof to inline into.

  • lemma_proof (Proof) – valid proof of one of the allowed inference rules of main_proof.

Return type

Proof

Returns

A valid proof obtained from main_proof by inlining (an appropriate specialization of) lemma_proof in lieu of each line that specifies the “lemma” inference rule proved by lemma_proof as its justification. The set of allowed inference rules in the returned proof is the union of the rules allowed in the two given proofs but without the “lemma” rule proved by lemma_proof.