Or

class proveit.logic.Or(*operands, styles=None)

Bases: proveit.Operation

Attributes Summary

trivial_disjunctions

Methods Summary

affirm_via_contradiction(self, conclusion, …)	From (A or B), derive the conclusion provided that the negated conclusion implies not(A) and not(B), and the conclusion is a Boolean.
associate(self, start_idx, length, …)	From self, derive and return a form in which operands in the range [start_idx, start_idx+length) are grouped together.
associated(expr, \*args, \*\*kwargs)	Return an equivalent form of this expression derived via ‘association’.
association(self, start_idx, length, …)	Given Boolean operands, deduce that this expression is equal to a form in which operands in the range [start_idx, start_idx+length) are grouped together.
commutation(self[, init_idx, final_idx])	Given Boolean operands, deduce that this expression is equal to a form in which the operand at index init_idx has been moved to final_idx.
commute(self[, init_idx, final_idx])	From self, derive and return a form in which the operand at index init_idx has been moved to final_idx.
commuted(expr, \*args, \*\*kwargs)	Return an equivalent form of this expression derived via ‘commutation’.
conclude(self, \*\*defaults_config)	Try to automatically conclude this disjunction.
conclude_negation(self, \*\*defaults_config)	Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.
conclude_via_both(self, \*\*defaults_config)	Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.
conclude_via_demorgans(self, \*\*defaults_config)	# created by JML 6/28/19 From A and B and C conclude Not(Not(A) or Not(B) or Not(C))
conclude_via_example(self, true_operand, …)	From one true operand, conclude that this ‘or’ expression is true.
conclude_via_left(self, \*\*defaults_config)	From A being (or assumed) True, conclude that (A V B) is True.
conclude_via_only_left(self, \*\*defaults_config)	Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.
conclude_via_only_right(self, …)	Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.
conclude_via_permutation(self, …)	From some true (or assumed true) but permutated version of this ‘or’ expression, conclude that this ‘or’ expression is true. For example, let this_or = A V B V C V D and let perm_of_this_or = S |- B V A V C V D. From perm_of_this_or, conclude this_or, using the following: this_or.conclude_via_permuation(perm_of_this_or, assumptions = S), which will return S |– A V B V C V D.
conclude_via_some(self, subset_disjunction, …)	From some true (or assumed true) disjunctive subset of the operands, conclude that this ‘or’ expression is true. This is similar to the conclude_via_example method above. For example, we might have a disjunction such as: example_disj = A V B V C V D, where we know (or assume) that B V D is true. We could call example_disj.conclude_via_some(B V D, assumptions=[B V D]), which will return {B V D} |– A V B V C V D.
deduce_in_bool(self, \*\*defaults_config)	Attempt to deduce, then return, that this ‘or’ expression is in the set of BOOLEANS.
deduce_left_in_bool(self, \*\*defaults_config)	Deduce A in Boolean from (A or B) in Boolean.
deduce_not_left_if_neither(self, …)	Deduce not(A) assuming not(A or B) where self is (A or B).
deduce_not_right_if_neither(self, …)	Deduce not(B) assuming not(A or B) where self is (A or B).
deduce_part_in_bool(self, index_or_expr, …)	Deduce X in Boolean from (A or B or .
deduce_right_in_bool(self, \*\*defaults_config)	Deduce B in Boolean from (A or B) in Boolean.
deny_via_contradiction(self, conclusion, …)	From (A or B), derive the negated conclusion provided that the conclusion implies both not(A) and not(B), and the conclusion is a Boolean.
derive_contradiction(self, \*\*defaults_config)	From (A or B), and assuming not(A) and not(B), derive and return FALSE.
derive_in_bool(self, \*\*defaults_config)	If the expression can be proven, it must be TRUE and therefore Boolean.
derive_left_if_not_right(self, …)	From (A or B) derive and return A assuming in_bool(A), Not(B).
derive_right_if_not_left(self, …)	From (A or B) derive and return B assuming Not(A), in_bool(B).
derive_via_dilemma(self, conclusion, …)	If the conclusion is also an Or operation with the same number of operands as self, try derive_via_multi_dilemma.
derive_via_multi_dilemma(self, conclusion, …)	From (A or B) as self, and assuming A => C, B => D, and A, B, C, and D are Boolean, derive and return the conclusion, C or D.
derive_via_singular_dilemma(self, …)	From (A or B) as self, and assuming A => C, B => C, and A and B are Boolean, derive and return the conclusion, C.
disassociate(self, idx, \*\*defaults_config)	From self, derive and return a form in which the operand at the given index is ungrouped. For example, from (A or B … or (L or … or M) or … or Y or Z) derive (A or B or … or Y or Z).
disassociated(expr, \*args, \*\*kwargs)	Return an equivalent form of this expression derived via ‘disassociation’.
disassociation(self, idx, \*\*defaults_config)	Given Boolean operands, deduce that this expression is equal to a form in which the operand at index idx is no longer grouped together. For example, (A or B … or (L or … or M) or … or Y or Z) = (A or B or … or Y or Z).
evaluation(self, \*\*defaults_config)	If possible, return a Judgment of this expression equal to an irreducible value.
group_commutation(self, init_idx, final_idx, …)	Given Boolean operands, deduce that this expression is equal to a form in which the operands at indices [init_idx, init_idx+length) have been moved to [final_idx, final_idx+length). It will do this by performing association first. If disassociate is True, it will be disassociated afterward. For example, the call Or(A,B,C,D).group_commutation(0, 1, length=2, assumptions=in_bool(A,B,C,D)) will conceptually follow the steps: (1) associates 2 elements (i.e. length = 2) starting at index 0 to obtain (A V B) V C V D (2) removes the element to be commuted to obtain C V D (3) inserts the element to be commuted at the desire index 1 to obtain C V (A V B) V D (4) then disassociates to obtain C V A V B V D (5) eventually producing the output: {A in Bool, …, D in Bool} |- (A V B V C V D) = (C V A V B V D).
group_commute(self, init_idx, final_idx, length)	Given self, deduce and return a form in which the operands at indices [init_idx, init_idx+length) have been moved to [final_idx.
group_commuted(expr, \*args, \*\*kwargs)	Return an equivalent form of this expression derived via ‘group_commutation’.
in_bool_side_effects(self, judgment)	From (A or B or .
negation_side_effects(self, judgment)	Side-effect derivations to attempt automatically for Not(A or B or .
side_effects(self, judgment)	Side-effect derivations to attempt automatically.
unary_reduction(self, \*\*defaults_config)	For the degenerate case of Or(A), where A is Boolean, derive and return |–[V](A) = A. For example, calling Or(A).unary_reduction([in_bool(A)]) will return: {A in Bool} |– [V](A) = A.

Attributes Documentation

trivial_disjunctions = {}

Methods Documentation

affirm_via_contradiction(self, conclusion, \*\*defaults_config)

From (A or B), derive the conclusion provided that the negated conclusion implies not(A) and not(B), and the conclusion is a Boolean.

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

associate(self, start_idx, length, \*\*defaults_config)

From self, derive and return a form in which operands in the range [start_idx, start_idx+length) are grouped together. For example, from (A or B or … or Y or Z) derive (A or B … or (L or … or M) or … or Y or Z).

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

associated(expr, \*args, \*\*kwargs)

Return an equivalent form of this expression derived via ‘association’.

association(self, start_idx, length, \*\*defaults_config)

Given Boolean operands, deduce that this expression is equal to a form in which operands in the range [start_idx, start_idx+length) are grouped together. For example, (A or B or … or Y or Z) = (A or B … or (L or … or M) or … or Y or Z)

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

‘associated’ returns the right-hand side of ‘association’. ‘associate’, called on an InnerExpr of a Judgment, substitutes the right-hand side of ‘association’ for the inner expression.

commutation(self, init_idx=None, final_idx=None, \*\*defaults_config)

Given Boolean operands, deduce that this expression is equal to a form in which the operand at index init_idx has been moved to final_idx. For example, (A or B or … or Y or Z) = (A or … or Y or B or Z) via init_idx = 1 and final_idx = -2.

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

‘commuted’ returns the right-hand side of ‘commutation’. ‘commute’, called on an InnerExpr of a Judgment, substitutes the right-hand side of ‘commutation’ for the inner expression.

commute(self, init_idx=None, final_idx=None, \*\*defaults_config)

From self, derive and return a form in which the operand at index init_idx has been moved to final_idx. For example, given (A or B or … or Y or Z) derive (A or … or Y or B or Z) via init_idx = 1 and final_idx = -2.

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

commuted(expr, \*args, \*\*kwargs)

Return an equivalent form of this expression derived via ‘commutation’.

conclude(self, \*\*defaults_config)

Try to automatically conclude this disjunction. If any of its operands have pre-existing proofs, it will be proven via the or_if_any theorem. Otherwise, a reduction proof will be attempted (evaluating the operands).

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

conclude_negation(self, \*\*defaults_config)

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

conclude_via_both(self, \*\*defaults_config)

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

conclude_via_demorgans(self, \*\*defaults_config)

# created by JML 6/28/19 From A and B and C conclude Not(Not(A) or Not(B) or Not(C))

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

conclude_via_example(self, true_operand, \*\*defaults_config)

From one true operand, conclude that this ‘or’ expression is true. Requires all of the operands to be in the set of BOOLEANS.

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

conclude_via_left(self, \*\*defaults_config)

From A being (or assumed) True, conclude that (A V B) is True.

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

conclude_via_only_left(self, \*\*defaults_config)

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

conclude_via_only_right(self, \*\*defaults_config)

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

conclude_via_permutation(self, permuted_disjunction, \*\*defaults_config)

From some true (or assumed true) but permutated version of this ‘or’ expression, conclude that this ‘or’ expression is true. For example, let this_or = A V B V C V D and let perm_of_this_or = S |- B V A V C V D. From perm_of_this_or, conclude this_or, using the following: this_or.conclude_via_permuation(perm_of_this_or, assumptions = S), which will return S |– A V B V C V D.

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

conclude_via_some(self, subset_disjunction, \*\*defaults_config)

From some true (or assumed true) disjunctive subset of the operands, conclude that this ‘or’ expression is true. This is similar to the conclude_via_example method above. For example, we might have a disjunction such as:

example_disj = A V B V C V D,

where we know (or assume) that B V D is true. We could call

example_disj.conclude_via_some(B V D, assumptions=[B V D]),

which will return

{B V D} |– A V B V C V D

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

deduce_in_bool(self, \*\*defaults_config)

Attempt to deduce, then return, that this ‘or’ expression is in the set of BOOLEANS.

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

deduce_left_in_bool(self, \*\*defaults_config)

Deduce A in Boolean from (A or B) in Boolean.

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

deduce_not_left_if_neither(self, \*\*defaults_config)

Deduce not(A) assuming not(A or B) where self is (A or B).

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

deduce_not_right_if_neither(self, \*\*defaults_config)

Deduce not(B) assuming not(A or B) where self is (A or B).

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

deduce_part_in_bool(self, index_or_expr, \*\*defaults_config)

Deduce X in Boolean from (A or B or .. or X or .. or Z) in Boolean provided X by expression or index number.

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

deduce_right_in_bool(self, \*\*defaults_config)

Deduce B in Boolean from (A or B) in Boolean.

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

deny_via_contradiction(self, conclusion, \*\*defaults_config)

From (A or B), derive the negated conclusion provided that the conclusion implies both not(A) and not(B), and the conclusion is a Boolean.

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

derive_contradiction(self, \*\*defaults_config)

From (A or B), and assuming not(A) and not(B), derive and return FALSE.

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

derive_in_bool(self, \*\*defaults_config)

If the expression can be proven, it must be TRUE and therefore Boolean.

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

derive_left_if_not_right(self, \*\*defaults_config)

From (A or B) derive and return A assuming in_bool(A), Not(B).

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

derive_right_if_not_left(self, \*\*defaults_config)

From (A or B) derive and return B assuming Not(A), in_bool(B).

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

derive_via_dilemma(self, conclusion, \*\*defaults_config)

If the conclusion is also an Or operation with the same number of operands as self, try derive_via_multi_dilemma. Otherwise, or if that fails, try derive_via_singular_dilemma.

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

derive_via_multi_dilemma(self, conclusion, \*\*defaults_config)

From (A or B) as self, and assuming A => C, B => D, and A, B, C, and D are Boolean, derive and return the conclusion, C or D.

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

derive_via_singular_dilemma(self, conclusion, \*\*defaults_config)

From (A or B) as self, and assuming A => C, B => C, and A and B are Boolean, derive and return the conclusion, C.

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

disassociate(self, idx, \*\*defaults_config)

From self, derive and return a form in which the operand at the given index is ungrouped. For example, from

(A or B … or (L or … or M) or … or Y or Z)

derive (A or B or … or Y or Z).

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

disassociated(expr, \*args, \*\*kwargs)

Return an equivalent form of this expression derived via ‘disassociation’.

disassociation(self, idx, \*\*defaults_config)

Given Boolean operands, deduce that this expression is equal to a form in which the operand at index idx is no longer grouped together. For example,

(A or B … or (L or … or M) or … or Y or Z) = (A or B or … or Y or Z)

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

‘disassociated’ returns the right-hand side of ‘disassociation’. ‘disassociate’, called on an InnerExpr of a Judgment, substitutes the right-hand side of ‘disassociation’ for the inner expression.

evaluation(self, \*\*defaults_config)

If possible, return a Judgment of this expression equal to an irreducible value. This Operation.evaluation version simplifies the operands and then calls shallow_simplification with must_evaluat=True.

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

‘evaluated’ returns the right-hand side of ‘evaluation’. ‘evaluate’, called on an InnerExpr of a Judgment, substitutes the right-hand side of ‘evaluation’ for the inner expression.

group_commutation(self, init_idx, final_idx, length, disassociate=True, \*\*defaults_config)

Given Boolean operands, deduce that this expression is equal to a form in which the operands at indices [init_idx, init_idx+length) have been moved to [final_idx, final_idx+length). It will do this by performing association first. If disassociate is True, it will be disassociated afterward. For example, the call Or(A,B,C,D).group_commutation(0, 1, length=2,

assumptions=in_bool(A,B,C,D))

will conceptually follow the steps: (1) associates 2 elements (i.e. length = 2) starting at index 0

to obtain (A V B) V C V D

2. removes the element to be commuted to obtain C V D

3. inserts the element to be commuted at the desire index 1 to obtain C V (A V B) V D

4. then disassociates to obtain C V A V B V D

5. eventually producing the output: {A in Bool, …, D in Bool} |- (A V B V C V D) = (C V A V B V D)

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

‘group_commuted’ returns the right-hand side of ‘group_commutation’. ‘group_commute’, called on an InnerExpr of a Judgment, substitutes the right-hand side of ‘group_commutation’ for the inner expression.

group_commute(self, init_idx, final_idx, length, disassociate=True, \*\*defaults_config)

Given self, deduce and return a form in which the operands at indices [init_idx, init_idx+length) have been moved to [final_idx. final_idx+length). It will do this by performing association first. If disassocate is True, it will be disassociated afterwards.

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

group_commuted(expr, \*args, \*\*kwargs)

Return an equivalent form of this expression derived via ‘group_commutation’.

in_bool_side_effects(self, judgment)

From (A or B or .. or Z) in Boolean deduce (A in Boolean), (B in Boolean), … (Z in Boolean).

negation_side_effects(self, judgment)

Side-effect derivations to attempt automatically for Not(A or B or .. or .. Z).

side_effects(self, judgment)

Side-effect derivations to attempt automatically.

unary_reduction(self, \*\*defaults_config)

For the degenerate case of Or(A), where A is Boolean, derive and return |–[V](A) = A. For example, calling

Or(A).unary_reduction([in_bool(A)])

will return:

{A in Bool} |– [V](A) = A

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

‘unary_reduced’ returns the right-hand side of ‘unary_reduction’. ‘unary_reduce’, called on an InnerExpr of a Judgment, substitutes the right-hand side of ‘unary_reduction’ for the inner expression.