punctilious

A human-friendly and developer-friendly math proof assistant

Table of contents

• Front matter
  • Title
  • About
  • Contributing
  • Roadmap
  • Project
  • Support
• Math
  • Concepts
    • alpha-equivalence
    • atomic-formula
    • axiom
    • axiomatic-method
    • bound-variable
    • compound-formula
    • definition
    • elimination-rule
    • formula
    • formula-statement
    • free-variable
    • hypothesis
    • inference-rule
    • inferred-statement
    • introduction-rule
    • is-a
    • meta-object
    • notation-form
    • object
    • object-creation
    • object-declaration
    • object-inclusion
    • paragraph-proof
    • connective
    • statement
    • theory-derivation
    • validity-of-formula
    • variable
    • universe-of-discourse
  • Inference rules
    • absorption
    • axiom-interpretation
    • biconditional-elimination-1
    • biconditional-elimination-2
    • biconditional-introduction
    • conjunction-elimination-1
    • conjunction-elimination-2
    • conjunction-introduction
    • constructive-dilemma
    • definition-interpretation
    • destructive-dilemma
    • disjunction-introduction-1
    • disjunction-introduction-2
    • disjunctive-resolution
    • disjunctive-syllogism-1
    • disjunctive-syllogism-2
    • double-negation-elimination
    • double-negation-introduction
    • equal-terms-substitution
    • equality-commutativity
    • hypothetical-syllogism
    • inconsistency-introduction-1
    • inconsistency-introduction-2
    • inconsistency-introduction-3
    • modus-ponens
    • modus-tollens
    • proof-by-contradiction-1
    • proof-by-contradiction-2
    • proof-by-refutation-1
    • proof-by-refutation-2
    • variable-substitution
  • Theories
    • MGZ 2021
      • Minimal logic
      • Intuitionistic logic
      • Classical logic
    • Tao 2006
      • The Peano axioms
• Python
  • Prerequisites
  • Installation
  • Source code repository
  • Class
    • Class diagram
    • AbsorptionDeclaration
    • AbsorptionInclusion
    • BiconditionalElimination1Declaration
    • BiconditionalElimination1Inclusion
    • BiconditionalElimination2Declaration
    • BiconditionalElimination2Inclusion
    • BiconditionalIntroductionDeclaration
    • BiconditionalIntroductionInclusion
    • ConjunctionElimination1Declaration
    • ConjunctionElimination1Inclusion
    • ConjunctionElimination2Declaration
    • ConjunctionElimination2Inclusion
    • ConjunctionIntroductionDeclaration
    • ConjunctionIntroductionInclusion
    • ConstructiveDilemmaDeclaration
    • ConstructiveDilemmaInclusion
    • DestructiveDilemmaDeclaration
    • DestructiveDilemmaInclusion
    • DisjunctionIntroduction1Declaration
    • DisjunctionIntroduction1Inclusion
    • DisjunctionIntroduction2Declaration
    • DisjunctionIntroduction2Inclusion
    • DisjunctiveResolutionDeclaration
    • DisjunctiveResolutionInclusion
    • DisjunctiveSyllogism1Declaration
    • DisjunctiveSyllogism1Inclusion
    • DisjunctiveSyllogism2Declaration
    • DisjunctiveSyllogism2Inclusion
    • DoubleNegationEliminationDeclaration
    • DoubleNegationEliminationInclusion
    • DoubleNegationIntroductionDeclaration
    • DoubleNegationIntroductionInclusion
    • EqualTermsSubstitutionDeclaration
    • EqualTermsSubstitutionInclusion
    • EqualityCommutativityDeclaration
    • EqualityCommutativityInclusion
    • FreeVariable
    • HypotheticalSyllogismDeclaration
    • HypotheticalSyllogismInclusion
    • InconsistencyIntroduction1Declaration
    • InconsistencyIntroduction1Inclusion
    • InconsistencyIntroduction2Declaration
    • InconsistencyIntroduction2Inclusion
    • InconsistencyIntroduction3Declaration
    • InconsistencyIntroduction3Inclusion
    • InferenceRuleDeclaration
    • InferenceRuleDeclarationAccretor
    • InferenceRuleInclusion
    • InferenceRuleInclusionCollection
    • ModusPonensDeclaration
    • ModusPonensInclusion
    • ModusTollensDeclaration
    • ModusTollensInclusion
    • ProofByContradiction1Declaration
    • ProofByContradiction1Inclusion
    • ProofByContradiction2Declaration
    • ProofByContradiction2Inclusion
    • ProofByRefutation1Declaration
    • ProofByRefutation1Inclusion
    • ProofByRefutation2Declaration
    • ProofByRefutation2Inclusion
    • UniverseOfDiscourse
    • VariableSubstitutionDeclaration
    • VariableSubstitutionInclusion
  • Function
    • create_universe_of_discourse
  • Sample
    • absorption_python_sample
    • biconditional_elimination_1_python_sample
    • biconditional_elimination_2_python_sample
    • biconditional_introduction_python_sample
    • conjunction_elimination_1_python_sample
    • conjunction_elimination_2_python_sample
    • conjunction_introduction_python_sample
    • disjunction_introduction_1_python_sample
    • disjunction_introduction_2_python_sample
    • double_negation_elimination_python_sample
    • double_negation_introduction_python_sample
    • equal_terms_substitution_python_sample
    • equality_commutativity_python_sample
    • free_variable_python_sample
    • inconsistency_introduction_1_python_sample
    • inconsistency_introduction_2_python_sample
    • inconsistency_introduction_3_python_sample
    • modus_ponens_python_sample
    • proof_by_contradiction_1_python_sample
    • proof_by_contradiction_2_python_sample
    • proof_by_refutation_1_python_sample
    • proof_by_refutation_2_python_sample
    • variable_substitution_python_sample
• Back matter
  • Reference tables
    • inference rules
  • Bibliography