Skip to content

Inference Rules

Jump to bottom
bhpayne edited this page Jan 4, 2015 · 7 revisions

Observations on categories of inference rules:

  • pairs which undo each other -- "divide both sides by" versus "multiply both sides by"
  • triplets -- "add X to LHS" and "add X to RHS" and "add X to both sides"

Table of Contents

derivation mechanics

declareFinalEq

declareInitialEq

declareAssumption

claimLHSequalsRHS

  • verbal: "claim left-hand-side equals right-hand-side of this expression"
  • terminates a derivation

declareIdentity

declareGuessSolution

swapLHSwithRHS

  • verbal: "swap left-hand-side with the right-hand-side of this expression"
  • example:
    given "A*x=B", swapLHSwithRHS yields "B=A*x"

algebra

sumExponents

  • verbal: sum the exponents of this expression
  • example:
    given "(A^x)*(A^y)=(C^3)*(C^r)+2", sumExponents yields "A^(x+y)=(C^(3+r))+2"

sumExponentsLHS

  • verbal: sum the exponents of left-hand-side of this expression
  • complement of sumExponentsRHS
  • example:
    given "(A^x)*(A^y)=(C^3)*(C^r)+2", sumExponents yields "A^(x+y)=(C^3)*(C^r)+2"

sumExponentsRHS

  • verbal: sum the exponents of left-hand-side of this expression
  • complement of sumExponentsRHS
  • example:
    given "(A^x)*(A^y)=(C^3)*(C^r)+2", sumExponents yields "(A^x)*(A^y)=(C^(3+r))+2"

addEqXtoEqY

  • verbal: add expression X to expression Y
  • example
    given "A*x=B" and "C*y=F", addEqXtoEqY yields "A*x+C*y=B+F"

subRHSofEqXintoEqY

  • verbal: substitute right-hand-side of expression X into expression Y
  • complement of subLHSofEqXintoEqY
  • example
    given "A*x=B" and "C*y=A*x", subRHSofEqXintoEqY yields "C*y=B"

subLHSofEqXintoEqY

  • verbal: substitute left-hand-side of expression X into expression Y
  • complement of subRHSofEqXintoEqY
  • example
    given "A*x=B" and "C*y=B", subLHSofEqXintoEqY yields "C*y=A*x"

multEqXbyEqY

  • verbal: multiply expression X by expression Y
  • example
    given "A*x=B" and "C*y=D", multEqXbyEqY yields "A*x*C*y=B*D"

LHSofEqXeqLHSofEqY

  • verbal: left-hand-side of expression X equals left-hand-side of expression Y
  • example
    given "A*x=B" and "A*x=C", LHSofEqXeqLHSofEqY yields "B=C"

RHSofEqXeqRHSofEqY

  • verbal: right-hand-side of expression X equals right-hand-side of expression Y
  • example
    given "A*x=B" and "C=B", RHSofEqXeqRHSofEqY yields "A*x=C"

subXforY

  • verbal: "substitute variable X for variable Y in this expression"
  • origin: substitution property of equality
  • example: 
     given "A*x=B", subXforY(input feed=A,output feed=C) yields "C*x=B"

multLHSbyUnity

  • verbal: "multiple left-hand-side of this expression by unity"
  • origin: multiplicative identity
  • example
    given "A*x=B", multLHSbyUnity(feed=C/C) yields "(A*x*C)/C=B"

multRHSbyUnity

  • verbal: "multiple left-hand-side of this expression by unity"
  • origin: multiplicative identity
  • example
    given "A*x=B", multLHSbyUnity(feed=C/C) yields "A*x=(B*C)/C"

functionIsEven

  • terminates derivation
  • f(x)=f(-x)
  • example: cosine

functionIsOdd

  • terminates derivation
  • -f(x) = f(-x)
  • example: sine

addZerotoLHS

  • origin: additive identity
  • example
    given "A*x=B", addZerotoLHS(feed=C-C) yields "A*x+C-C=B"

addZerotoRHS

  • verbal: add zero to the right-hand-side of expression
  • origin: additive identity
  • example
    given "A*x=B", addZerotoRHS(feed=C-C) yields "A*x=B+C-C"

multbothsidesby

  • verbal: "multiply both sides of this expression by"
  • example
    given "A*x=B", multbothsidesby(feed=2) yields "A*x*2=B*2"

dividebothsidesby

  • verbal: "multiply both sides of this expression by"
  • example:
    given "A*x=B", dividebothsidesby(feed=2) yields "(A*x)/2=B/2"

addXtoBothSides

  • verbal: "add the quantity to both sides of the expression"
  • example:
    given "A*x=B", addXtoBothSides(feed=2) yields "A*x+2=B+2"

subtractXfromBothSides

  • verbal: "subtract quantity from both sides of the expression"
  • example:
    given "A*x=B", subtractXfromBothSides(feed=2) yields "A*x-2=B-2"

combineLikeTerms

  • example
    given "A*x=B",

solveForX

factorOutX

  • example
    given "A*x=B",

factorOutXfromLHS

  • example
    given "A*k+B*k+C=D", factorOutXfromLHS(feed=k) yields "k*(A+B)+C=D"

factorOutXfromRHS

  • example: given "A*x=B",

calculus

indefIntOver

indefIntegration

indefIntLHSOver

indefIntRHSOver

IntOverFromTo

EvaluateDefiniteIntegral

expandIntegrand

unsorted

simplify

  • example
    given "A*x=B",

makeEqPower

expandLHS

expandRHS

EqXisTrueUnderconditionEqY

raiseBothSidesToPower

  • example: 
    given "A*x=B",

claimEqXequalsEqY

  • example: 
    given "A*x=B",

selectRealParts

  • example: 
    given "A*x=B",

selectImagParts

  • example: 
    given "A*x=B",

AssumeNdimensions

ReplaceCurlWithLeviCevitaSummationContravariant

ReplaceSummationNotationWithVectorNotation

replaceScalarWithVector

conjugateFunctionX

conjugateBothSides

conjugateTransposeBothSides

distributeConjugateTransposeToFactors

distributeConjugateToFactors

expandMagnitudeToConjugate

takeCurlofBothSides

applyGradientToScalarFunction

applyDivergence

differentiateWRT

partialDiffWRT

Xcrossbothsidesby

bothsidescrossX

Xdotbothsides

bothsidesdotX

normalizationCondition

boundaryCondition

quantum

applyOperatorToKet

applyOperatorToBra

Clone this wiki locally