Proof¶
-
class
proveit.Proof(proven_truth, required_truths, marked_required_truth_indices=None)[source]¶ Bases:
objectAttributes Summary
Methods Summary
all_required_proofs(self)Returns the set of directly or indirectly required Proofs, stopping at Assumptions, Axioms, or Theorems.
assumptions(self)disable(self)Disable the use of this Proof and any of its dependents that don’t have an alternate proof that doesn’t rely on this one.
enumerated_proof_steps(self)Returns a list of Proof objects that includes self and all of its direct and indirect requirements.
get_link(self)Return the link to the proof notebook.
is_usable(self)Returns True iff this Proof is usable.
num_steps(self)Return the number of unique steps in the proof.
used_axioms(self)Returns the set of names of axioms that are used directly (not via other theorems) in this proof.
used_theorems(self)Returns the set of names of axioms that are used directly (not via other theorems) in this proof.
Attributes Documentation
Methods Documentation
-
all_required_proofs(self)[source]¶ Returns the set of directly or indirectly required Proofs, stopping at Assumptions, Axioms, or Theorems.
-
disable(self)[source]¶ Disable the use of this Proof and any of its dependents that don’t have an alternate proof that doesn’t rely on this one.
-
enumerated_proof_steps(self)[source]¶ Returns a list of Proof objects that includes self and all of its direct and indirect requirements. Duplicates will not be included, but they will be presented in an order which makes it clear that the dependencies are acyclic by making sure requirements come after dependents.
-
get_link(self)[source]¶ Return the link to the proof notebook. It the Proof is a Theorem or Axiom, this is overridden to return the link to the theorem/axiom definition.
-
is_usable(self)[source]¶ Returns True iff this Proof is usable. A Proof may be unusable because it was manually disabled or because it is not being presumed while trying to prove a Theorem (other Theorems must be explicitly presumed in order to avoid circular logic).
-