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
-
__init__
(assumptions, conclusion)¶ Initializes an
InferenceRule
from its assumptions and conclusion.
-
__repr__
()¶ Computes a string representation of the current inference rule.
- Return type
- 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
- Returns
True
if the given object is anInferenceRule
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
- Returns
True
if the given object is not anInferenceRule
object or does not does not equal the current inference rule,False
otherwise.
-
variables
()¶ Finds all variable names in the current inference rule.
-
specialize
(specialization_map)¶ Specializes the current inference rule by simultaneously substituting each variable name
v
that is a key inspecialization_map
with the formulaspecialization_map[v]
.
-
static
_merge_specialization_maps
(specialization_map1, specialization_map2)¶ Merges the given specialization maps while checking their consistency.
- Parameters
- Return type
- 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 isNone
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
- Return type
- Returns
The computed specialization map, or
None
ifspecialization
is in fact not a specialization ofgeneral
.
-
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
- Returns
The computed specialization map, or
None
ifspecialization
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
- Returns
True
if the current inference rule is a specialization ofgeneral
,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
statement (
InferenceRule
) – the statement proven by the proof.rules (
AbstractSet
[InferenceRule
]) – the allowed rules of the proof.
-
__init__
(statement, rules, lines)¶ Initializes a
Proof
from its statement, allowed inference rules, and lines.- Parameters
statement (
InferenceRule
) – the statement to be proven by the proof.rules (
AbstractSet
[InferenceRule
]) – the allowed rules for the proof.
-
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; orNone
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; orNone
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, orNone
if the formula is to be justified as an assumption of the proof.
-
__repr__
()¶ Computes a string representation of the current line.
- Return type
- Returns
A string representation of the current line.
-
__repr__
()¶ Computes a string representation of the current proof.
- Return type
- 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
- 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
- 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:The conclusion of that specialization is the formula justified by that line.
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.
-
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
- 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
- Return type
- 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 inmain_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 inmain_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
- Return type
- 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 bylemma_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 bylemma_proof
.