让规则说明从docstring自动生成[#121]

curl-curl-identity

Replace the curl of a curl by the gradient of the divergence minus the vector Laplacian. The field must be C2; declaring it divergence-free is a separate premise and a separate rewrite.

\frac{c2 (field) field : vector}{\nabla \times (\nabla \times field) \to \nabla (\nabla \cdot field) - Δ field} [curl-curl-identity]

Group: vector-calculus. Modes: (forward backward check). Declarative RuleSpec; metavariables denote terms. Condition: assumptions declare vector(E) and c2(E)

Exact scalar-algebra check: unsupported.

divergence-free

\frac{\nabla \cdot field = 0 field : vector}{\nabla (\nabla \cdot field) \to \vec{0}} [divergence-free]

Group: vector-calculus. Modes: (forward backward check). Declarative RuleSpec; metavariables denote terms. Condition: vector(E) and the matching fact div(E) = 0

Exact scalar-algebra check: unsupported.

div-curl-zero

\frac{c2 (field) field : vector}{\nabla \cdot (\nabla \times field) \to 0} [div-curl-zero]

Group: vector-calculus. Modes: (forward backward check). Declarative RuleSpec; metavariables denote terms. Condition: assumptions declare vector(E) and c2(E)

Exact scalar-algebra check: unsupported.

curl-grad-zero

\frac{c2 (field) field : scalar}{\nabla \times (\nabla field) \to \vec{0}} [curl-grad-zero]

Group: vector-calculus. Modes: (forward backward check). Declarative RuleSpec; metavariables denote terms. Condition: assumptions declare scalar(f) and c2(f)

Exact scalar-algebra check: unsupported.

div-grad-laplacian

\frac{c2 (field) field : scalar}{\nabla \cdot (\nabla field) \to Δ field} [div-grad-laplacian]

Group: vector-calculus. Modes: (forward backward check). Declarative RuleSpec; metavariables denote terms. Condition: assumptions declare scalar(f) and c2(f)

Exact scalar-algebra check: unsupported.

grad-product

Differentiate the product of two scalar fields with the gradient product rule. C1 regularity suffices; no second derivatives or smoothness assumptions are required.

\frac{differentiable (f) differentiable (g) f : scalar g : scalar}{\nabla (f \times g) \to g \times \nabla f + f \times \nabla g} [grad-product]

Group: vector-calculus. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: scalar C1 fields in Cartesian space

Exact scalar-algebra check: unsupported.

div-product

\frac{differentiable (f) differentiable (e) f : scalar e : vector}{\nabla \cdot (f \times e) \to \nabla f \cdot e + f \times \nabla \cdot e} [div-product]

Group: vector-calculus. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: scalar and vector C1 fields in Cartesian space

Exact scalar-algebra check: unsupported.

curl-product

Expand the curl of a scalar times a vector field in oriented Cartesian space. The cross product is grad(f) cross E, in that order; reversing it changes the sign. Both factors need C1 regularity.

\frac{differentiable (f) differentiable (e) f : scalar e : vector}{\nabla \times (f \times e) \to \nabla f \times e + f \times \nabla \times e} [curl-product]

Group: vector-calculus. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: scalar and vector C1 fields in oriented Cartesian space

Exact scalar-algebra check: unsupported.

subtract-zero

\frac{(math-typeo facts term type); executable guards apply}{zero - term \to - term} [subtract-zero]

Group: identity. Modes: (forward backward check). Declarative RuleSpec; metavariables denote terms. Condition: matching scalar or vector types

Exact scalar-algebra check: semantically-checked.

Executable guards

((zeroo type zero))

add-zero

\frac{(math-typeo facts term type); executable guards apply}{term + zero \to term} [add-zero]

Group: identity. Modes: (forward backward check). Declarative RuleSpec; metavariables denote terms. Condition: matching scalar or vector types

Exact scalar-algebra check: semantically-checked.

Executable guards

((zeroo type zero))

zero-add

\frac{(math-typeo facts term type); executable guards apply}{zero + term \to term} [zero-add]

Group: identity. Modes: (forward backward check). Declarative RuleSpec; metavariables denote terms. Condition: matching scalar or vector types

Exact scalar-algebra check: semantically-checked.

Executable guards

((zeroo type zero))

subtract-right-zero

\frac{(math-typeo facts term type); executable guards apply}{term - zero \to term} [subtract-right-zero]

Group: identity. Modes: (forward backward check). Declarative RuleSpec; metavariables denote terms. Condition: matching scalar or vector types

Exact scalar-algebra check: semantically-checked.

Executable guards

((zeroo type zero))

double-negation

\frac{(math-typeo facts term type); executable guards apply}{- (- term) \to term} [double-negation]

Group: identity. Modes: (forward backward check). Declarative RuleSpec; metavariables denote terms. Condition: X is scalar or vector

Exact scalar-algebra check: semantically-checked.

Executable guards

((conde ((== type (quote scalar))) ((== type (quote vector)))))

multiply-one

\frac{(math-typeo facts term type); executable guards apply}{term \times 1 \to term} [multiply-one]

Group: identity. Modes: (forward backward check). Declarative RuleSpec; metavariables denote terms. Condition: X is scalar or vector

Exact scalar-algebra check: semantically-checked.

Executable guards

((conde ((== type (quote scalar))) ((== type (quote vector)))))

one-multiply

\frac{(math-typeo facts term type); executable guards apply}{1 term \to term} [one-multiply]

Group: identity. Modes: (forward backward check). Declarative RuleSpec; metavariables denote terms. Condition: X is scalar or vector

Exact scalar-algebra check: semantically-checked.

Executable guards

((conde ((== type (quote scalar))) ((== type (quote vector)))))

multiply-zero

\frac{term : scalar}{term \times 0 \to 0} [multiply-zero]

Group: identity. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: X is scalar

Exact scalar-algebra check: semantically-checked.

zero-multiply

\frac{term : scalar}{0 term \to 0} [zero-multiply]

Group: identity. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: X is scalar

Exact scalar-algebra check: semantically-checked.

power-one

\frac{term : scalar}{{term}^{1} \to term} [power-one]

Group: identity. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: X is scalar

Exact scalar-algebra check: semantically-checked.

power-zero

\frac{term : scalar}{{term}^{0} \to 1} [power-zero]

Group: identity. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: polynomial power convention

Exact scalar-algebra check: semantically-checked.

add-commutative

\frac{left : scalar right : scalar}{left + right \to right + left} [add-commutative]

Group: polynomial-algebra. Modes: (check). Declarative RuleSpec; metavariables denote terms. Condition: scalar terms

Exact scalar-algebra check: semantically-checked.

multiply-associative

\frac{left : scalar middle : scalar right : scalar}{left \times middle \times right \to left \times middle \times right} [multiply-associative]

Group: polynomial-algebra. Modes: (check). Declarative RuleSpec; metavariables denote terms. Condition: scalar terms

Exact scalar-algebra check: semantically-checked.

add-associative

\frac{left : scalar middle : scalar right : scalar}{left + middle + right \to left + middle + right} [add-associative]

Group: polynomial-algebra. Modes: (check). Declarative RuleSpec; metavariables denote terms. Condition: scalar terms

Exact scalar-algebra check: semantically-checked.

multiply-commutative

\frac{left : scalar right : scalar}{left \times right \to right \times left} [multiply-commutative]

Group: polynomial-algebra. Modes: (check). Declarative RuleSpec; metavariables denote terms. Condition: scalar terms

Exact scalar-algebra check: semantically-checked.

differentiate-constant

\frac{(unquote (quasiquote (unquote expression))) : scalar (unquote (quasiquote (var (unquote coordinate)))) : scalar; executable guards apply}{\frac{d}{d coordinate} (expression) \to 0} [differentiate-constant]

Group: differentiate. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: real scalar expression in independent scalar coordinates

Exact scalar-algebra check: unsupported.

Executable guards

((project (facts expression coordinate) (if (differentiable-term? (quasiquote (unquote expression)) facts) succeed fail)) (project (facts coordinate) (if (eq? (math-variable-role facts (quasiquote (var (unquote coordinate)))) (quote parameter)) fail succeed)) (project (expression) (if (math-number-value expression) succeed fail)))

differentiate-variable

\frac{(unquote (quasiquote (var (unquote coordinate)))) : scalar (unquote (quasiquote (var (unquote coordinate)))) : scalar; executable guards apply}{\frac{d}{d coordinate} (coordinate) \to 1} [differentiate-variable]

Group: differentiate. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: real scalar expression in independent scalar coordinates

Exact scalar-algebra check: unsupported.

Executable guards

((project (facts coordinate) (if (differentiable-term? (quasiquote (var (unquote coordinate))) facts) succeed fail)) (project (facts coordinate) (if (eq? (math-variable-role facts (quasiquote (var (unquote coordinate)))) (quote parameter)) fail succeed)))

differentiate-independent

\frac{(unquote (quasiquote (var (unquote other)))) : scalar (unquote (quasiquote (var (unquote coordinate)))) : scalar; executable guards apply}{\frac{d}{d coordinate} (other) \to 0} [differentiate-independent]

Group: differentiate. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: real scalar expression in independent scalar coordinates

Exact scalar-algebra check: unsupported.

Executable guards

((project (facts other coordinate) (if (differentiable-term? (quasiquote (var (unquote other))) facts) succeed fail)) (project (facts coordinate) (if (eq? (math-variable-role facts (quasiquote (var (unquote coordinate)))) (quote parameter)) fail succeed)) (=/= other coordinate))

differentiate-negation

\frac{(unquote (quasiquote (- (unquote operand)))) : scalar (unquote (quasiquote (var (unquote coordinate)))) : scalar; executable guards apply}{\frac{d}{d coordinate} (- operand) \to - (\frac{d}{d coordinate} (operand))} [differentiate-negation]

Group: differentiate. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: real scalar expression in independent scalar coordinates

Exact scalar-algebra check: unsupported.

Executable guards

((project (facts operand coordinate) (if (differentiable-term? (quasiquote (- (unquote operand))) facts) succeed fail)) (project (facts coordinate) (if (eq? (math-variable-role facts (quasiquote (var (unquote coordinate)))) (quote parameter)) fail succeed)))

differentiate-sum

\frac{(unquote (quasiquote (+ (unquote left) (unquote right)))) : scalar (unquote (quasiquote (var (unquote coordinate)))) : scalar; executable guards apply}{\frac{d}{d coordinate} (left + right) \to \frac{d}{d coordinate} (left) + \frac{d}{d coordinate} (right)} [differentiate-sum]

Group: differentiate. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: real scalar expression in independent scalar coordinates

Exact scalar-algebra check: unsupported.

Executable guards

((project (facts left right coordinate) (if (differentiable-term? (quasiquote (+ (unquote left) (unquote right))) facts) succeed fail)) (project (facts coordinate) (if (eq? (math-variable-role facts (quasiquote (var (unquote coordinate)))) (quote parameter)) fail succeed)))

differentiate-difference

\frac{(unquote (quasiquote (- (unquote left) (unquote right)))) : scalar (unquote (quasiquote (var (unquote coordinate)))) : scalar; executable guards apply}{\frac{d}{d coordinate} (left - right) \to \frac{d}{d coordinate} (left) - \frac{d}{d coordinate} (right)} [differentiate-difference]

Group: differentiate. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: real scalar expression in independent scalar coordinates

Exact scalar-algebra check: unsupported.

Executable guards

((project (facts left right coordinate) (if (differentiable-term? (quasiquote (- (unquote left) (unquote right))) facts) succeed fail)) (project (facts coordinate) (if (eq? (math-variable-role facts (quasiquote (var (unquote coordinate)))) (quote parameter)) fail succeed)))

differentiate-product

Generate the derivative of each factor separately and sum the two products. This rule constructs derivative terms; subsequent differentiation and simplification steps compute and reduce them.

\frac{(unquote (quasiquote (* (unquote left) (unquote right)))) : scalar (unquote (quasiquote (var (unquote coordinate)))) : scalar; executable guards apply}{\frac{d}{d coordinate} (left \times right) \to \frac{d}{d coordinate} (left) \times right + left \times \frac{d}{d coordinate} (right)} [differentiate-product]

Group: differentiate. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: real scalar expression in independent scalar coordinates

Exact scalar-algebra check: unsupported.

Executable guards

((project (facts left right coordinate) (if (differentiable-term? (quasiquote (* (unquote left) (unquote right))) facts) succeed fail)) (project (facts coordinate) (if (eq? (math-variable-role facts (quasiquote (var (unquote coordinate)))) (quote parameter)) fail succeed)))

differentiate-power

\frac{(unquote (quasiquote (^ (unquote base) (num (unquote exponent))))) : scalar (unquote (quasiquote (var (unquote coordinate)))) : scalar; executable guards apply}{\frac{d}{d coordinate} ({base}^{exponent}) \to result} [differentiate-power]

Group: differentiate. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: real scalar expression in independent scalar coordinates

Exact scalar-algebra check: unsupported.

Executable guards

((project (facts base exponent result coordinate) (if (differentiable-term? (quasiquote (^ (unquote base) (num (unquote exponent)))) facts) succeed fail)) (project (facts coordinate) (if (eq? (math-variable-role facts (quasiquote (var (unquote coordinate)))) (quote parameter)) fail succeed)) (project (exponent base coordinate) (let ((n (natural-value exponent))) (if (= n 0) (== result (quote (num "0"))) (== result (quasiquote (* (* (num (unquote exponent)) (^ (unquote base) (num (unquote (number->string (- n 1)))))) (differentiate (unquote base) (var (unquote coordinate))))))))))

differentiate-quotient

Apply the quotient rule on the domain where the denominator is nonzero. The derivative remains a symbolic term until later passes process its operands and simplify the result.

\frac{(unquote (quasiquote (/ (unquote left) (unquote right)))) : scalar (unquote (quasiquote (var (unquote coordinate)))) : scalar; executable guards apply}{\frac{d}{d coordinate} (\frac{left}{right}) \to \frac{\frac{d}{d coordinate} (left) \times right - left \times \frac{d}{d coordinate} (right)}{{right}^{2}}} [differentiate-quotient]

Group: differentiate. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: real scalar expression in independent scalar coordinates

Exact scalar-algebra check: unsupported.

Executable guards

((project (facts left right coordinate) (if (differentiable-term? (quasiquote (/ (unquote left) (unquote right))) facts) succeed fail)) (project (facts coordinate) (if (eq? (math-variable-role facts (quasiquote (var (unquote coordinate)))) (quote parameter)) fail succeed)) (math-factso facts (quasiquote ((nonzero (unquote right))))))

differentiate-sin

\frac{(unquote (quasiquote (sin (unquote operand)))) : scalar (unquote (quasiquote (var (unquote coordinate)))) : scalar; executable guards apply}{\frac{d}{d coordinate} (\sin (operand)) \to \frac{d}{d coordinate} (operand) \times \cos (operand)} [differentiate-sin]

Group: differentiate. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: real scalar expression in independent scalar coordinates

Exact scalar-algebra check: unsupported.

Executable guards

((project (facts operand coordinate) (if (differentiable-term? (quasiquote (sin (unquote operand))) facts) succeed fail)) (project (facts coordinate) (if (eq? (math-variable-role facts (quasiquote (var (unquote coordinate)))) (quote parameter)) fail succeed)))

differentiate-cos

\frac{(unquote (quasiquote (cos (unquote operand)))) : scalar (unquote (quasiquote (var (unquote coordinate)))) : scalar; executable guards apply}{\frac{d}{d coordinate} (\cos (operand)) \to - (\frac{d}{d coordinate} (operand) \times \sin (operand))} [differentiate-cos]

Group: differentiate. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: real scalar expression in independent scalar coordinates

Exact scalar-algebra check: unsupported.

Executable guards

((project (facts operand coordinate) (if (differentiable-term? (quasiquote (cos (unquote operand))) facts) succeed fail)) (project (facts coordinate) (if (eq? (math-variable-role facts (quasiquote (var (unquote coordinate)))) (quote parameter)) fail succeed)))

differentiate-exp

\frac{(unquote (quasiquote (exp (unquote operand)))) : scalar (unquote (quasiquote (var (unquote coordinate)))) : scalar; executable guards apply}{\frac{d}{d coordinate} (\exp (operand)) \to \frac{d}{d coordinate} (operand) \times \exp (operand)} [differentiate-exp]

Group: differentiate. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: real scalar expression in independent scalar coordinates

Exact scalar-algebra check: unsupported.

Executable guards

((project (facts operand coordinate) (if (differentiable-term? (quasiquote (exp (unquote operand))) facts) succeed fail)) (project (facts coordinate) (if (eq? (math-variable-role facts (quasiquote (var (unquote coordinate)))) (quote parameter)) fail succeed)))

differentiate-log

\frac{(unquote (quasiquote (log (unquote operand)))) : scalar (unquote (quasiquote (var (unquote coordinate)))) : scalar; executable guards apply}{\frac{d}{d coordinate} (\log (operand)) \to \frac{\frac{d}{d coordinate} (operand)}{operand}} [differentiate-log]

Group: differentiate. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: real scalar expression in independent scalar coordinates

Exact scalar-algebra check: unsupported.

Executable guards

((project (facts operand coordinate) (if (differentiable-term? (quasiquote (log (unquote operand))) facts) succeed fail)) (project (facts coordinate) (if (eq? (math-variable-role facts (quasiquote (var (unquote coordinate)))) (quote parameter)) fail succeed)) (math-factso facts (quasiquote ((positive (unquote operand))))))

differentiate-function

Apply the shared function chain rule using one-based argument positions. C1 permits one derivative, C2 permits two, and smooth permits higher derivatives.

\frac{Declared scalar function and sufficient regularity for the next derivative; algorithm applicability checked}{Derivative of f(u_1,...,u_n) = sum_i partial_i f(u_1,...,u_n) derivative of u_i} [differentiate-function]

Group: differentiate. Modes: (forward check). Algorithm rule; this description has no fixed RuleSpec. Condition: Declared scalar function and sufficient regularity for the next derivative

Exact scalar-algebra check: unsupported.

evaluate-constant

\frac{exact scalar arithmetic; algorithm applicability checked}{exact constant arithmetic} [evaluate-constant]

Group: calculate. Modes: (forward check). Algorithm rule; this description has no fixed RuleSpec. Condition: exact scalar arithmetic

Exact scalar-algebra check: unsupported.

collect-like-terms

\frac{exact scalar arithmetic; algorithm applicability checked}{a*X + b*X = (a+b)*X} [collect-like-terms]

Group: collect. Modes: (forward check). Algorithm rule; this description has no fixed RuleSpec. Condition: exact scalar arithmetic

Exact scalar-algebra check: unsupported.

combine-coefficients

\frac{exact scalar arithmetic; algorithm applicability checked}{a*(b*X) = (a*b)*X} [combine-coefficients]

Group: collect. Modes: (forward check). Algorithm rule; this description has no fixed RuleSpec. Condition: exact scalar arithmetic

Exact scalar-algebra check: unsupported.

normalize-scalar

\frac{real scalar algebra; algorithm applicability checked}{normalize-scalar} [normalize-scalar]

Group: normalize. Modes: (forward check). Algorithm rule; this description has no fixed RuleSpec. Condition: real scalar algebra

Exact scalar-algebra check: unsupported.

cancel-scalar-factors

\frac{real scalar algebra; algorithm applicability checked}{cancel-scalar-factors} [cancel-scalar-factors]

Group: cancel. Modes: (forward check). Algorithm rule; this description has no fixed RuleSpec. Condition: real scalar algebra

Exact scalar-algebra check: unsupported.

cancel-common-factor

A check-only cancellation theorem. Its denominator side condition is explicit in the premise and must remain in the surrounding domain requirements.

\frac{nonzero (factor) value : scalar factor : scalar}{\frac{value \times factor}{factor} \to value} [cancel-common-factor]

Group: cancel. Modes: (check). Declarative RuleSpec; metavariables denote terms. Condition: real scalar terms; A is nonzero

Exact scalar-algebra check: semantically-checked.

expand-scalar-product

\frac{real scalar algebra; algorithm applicability checked}{expand-scalar-product} [expand-scalar-product]

Group: expand. Modes: (forward check). Algorithm rule; this description has no fixed RuleSpec. Condition: real scalar algebra

Exact scalar-algebra check: unsupported.

normalize-function-prime

\frac{differentiable (name) (unquote (quasiquote (prime (var (unquote name)) (unquote argument)))) : scalar}{{name}^{'} (argument) \to (darg ((unquote name) (unquote argument)) (num "1"))} [normalize-function-prime]

Group: normalize. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: Declared unary scalar function with one derivative

Exact scalar-algebra check: unsupported.

partial-constant

\frac{coordinate (coordinate) differentiable (expression) (unquote (quasiquote (unquote expression))) : scalar (unquote (quasiquote (var (unquote coordinate)))) : scalar; executable guards apply}{\frac{\partial}{\partial coordinate} (expression) \to 0} [partial-constant]

Group: partial. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: C1 scalar expression in explicitly declared independent coordinates

Exact scalar-algebra check: unsupported.

Executable guards

((project (facts expression coordinate) (if (differentiable-term? (quasiquote (unquote expression)) facts) succeed fail)) (project (facts coordinate) (if (eq? (math-variable-role facts (quasiquote (var (unquote coordinate)))) (quote parameter)) fail succeed)) (project (expression) (if (math-number-value expression) succeed fail)))

partial-variable

\frac{coordinate (coordinate) differentiable (coordinate) (unquote (quasiquote (var (unquote coordinate)))) : scalar (unquote (quasiquote (var (unquote coordinate)))) : scalar; executable guards apply}{\frac{\partial}{\partial coordinate} (coordinate) \to 1} [partial-variable]

Group: partial. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: C1 scalar expression in explicitly declared independent coordinates

Exact scalar-algebra check: unsupported.

Executable guards

((project (facts coordinate) (if (differentiable-term? (quasiquote (var (unquote coordinate))) facts) succeed fail)) (project (facts coordinate) (if (eq? (math-variable-role facts (quasiquote (var (unquote coordinate)))) (quote parameter)) fail succeed)))

partial-independent

\frac{coordinate (coordinate) differentiable (other) (unquote (quasiquote (var (unquote other)))) : scalar (unquote (quasiquote (var (unquote coordinate)))) : scalar; executable guards apply}{\frac{\partial}{\partial coordinate} (other) \to 0} [partial-independent]

Group: partial. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: C1 scalar expression in explicitly declared independent coordinates

Exact scalar-algebra check: unsupported.

Executable guards

((project (facts other coordinate) (if (differentiable-term? (quasiquote (var (unquote other))) facts) succeed fail)) (project (facts coordinate) (if (eq? (math-variable-role facts (quasiquote (var (unquote coordinate)))) (quote parameter)) fail succeed)) (=/= other coordinate) (project (facts input) (if (independent-variable? facts input) succeed fail)))

partial-negation

\frac{coordinate (coordinate) differentiable (- operand) (unquote (quasiquote (- (unquote operand)))) : scalar (unquote (quasiquote (var (unquote coordinate)))) : scalar; executable guards apply}{\frac{\partial}{\partial coordinate} (- operand) \to - (\frac{\partial}{\partial coordinate} (operand))} [partial-negation]

Group: partial. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: C1 scalar expression in explicitly declared independent coordinates

Exact scalar-algebra check: unsupported.

Executable guards

((project (facts operand coordinate) (if (differentiable-term? (quasiquote (- (unquote operand))) facts) succeed fail)) (project (facts coordinate) (if (eq? (math-variable-role facts (quasiquote (var (unquote coordinate)))) (quote parameter)) fail succeed)))

partial-sum

\frac{coordinate (coordinate) differentiable (left + right) (unquote (quasiquote (+ (unquote left) (unquote right)))) : scalar (unquote (quasiquote (var (unquote coordinate)))) : scalar; executable guards apply}{\frac{\partial}{\partial coordinate} (left + right) \to \frac{\partial}{\partial coordinate} (left) + \frac{\partial}{\partial coordinate} (right)} [partial-sum]

Group: partial. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: C1 scalar expression in explicitly declared independent coordinates

Exact scalar-algebra check: unsupported.

Executable guards

((project (facts left right coordinate) (if (differentiable-term? (quasiquote (+ (unquote left) (unquote right))) facts) succeed fail)) (project (facts coordinate) (if (eq? (math-variable-role facts (quasiquote (var (unquote coordinate)))) (quote parameter)) fail succeed)))

partial-difference

\frac{coordinate (coordinate) differentiable (left - right) (unquote (quasiquote (- (unquote left) (unquote right)))) : scalar (unquote (quasiquote (var (unquote coordinate)))) : scalar; executable guards apply}{\frac{\partial}{\partial coordinate} (left - right) \to \frac{\partial}{\partial coordinate} (left) - \frac{\partial}{\partial coordinate} (right)} [partial-difference]

Group: partial. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: C1 scalar expression in explicitly declared independent coordinates

Exact scalar-algebra check: unsupported.

Executable guards

((project (facts left right coordinate) (if (differentiable-term? (quasiquote (- (unquote left) (unquote right))) facts) succeed fail)) (project (facts coordinate) (if (eq? (math-variable-role facts (quasiquote (var (unquote coordinate)))) (quote parameter)) fail succeed)))

partial-product

\frac{coordinate (coordinate) differentiable (left \times right) (unquote (quasiquote (* (unquote left) (unquote right)))) : scalar (unquote (quasiquote (var (unquote coordinate)))) : scalar; executable guards apply}{\frac{\partial}{\partial coordinate} (left \times right) \to \frac{\partial}{\partial coordinate} (left) \times right + left \times \frac{\partial}{\partial coordinate} (right)} [partial-product]

Group: partial. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: C1 scalar expression in explicitly declared independent coordinates

Exact scalar-algebra check: unsupported.

Executable guards

((project (facts left right coordinate) (if (differentiable-term? (quasiquote (* (unquote left) (unquote right))) facts) succeed fail)) (project (facts coordinate) (if (eq? (math-variable-role facts (quasiquote (var (unquote coordinate)))) (quote parameter)) fail succeed)))

partial-power

\frac{coordinate (coordinate) differentiable ({base}^{exponent}) (unquote (quasiquote (^ (unquote base) (num (unquote exponent))))) : scalar (unquote (quasiquote (var (unquote coordinate)))) : scalar; executable guards apply}{\frac{\partial}{\partial coordinate} ({base}^{exponent}) \to result} [partial-power]

Group: partial. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: C1 scalar expression in explicitly declared independent coordinates

Exact scalar-algebra check: unsupported.

Executable guards

((project (facts base exponent result coordinate) (if (differentiable-term? (quasiquote (^ (unquote base) (num (unquote exponent)))) facts) succeed fail)) (project (facts coordinate) (if (eq? (math-variable-role facts (quasiquote (var (unquote coordinate)))) (quote parameter)) fail succeed)) (project (exponent base coordinate) (let ((n (natural-value exponent))) (if (= n 0) (== result (quote (num "0"))) (== result (quasiquote (* (* (num (unquote exponent)) (^ (unquote base) (num (unquote (number->string (- n 1)))))) (partial (unquote base) (var (unquote coordinate))))))))))

partial-quotient

\frac{coordinate (coordinate) differentiable (\frac{left}{right}) (unquote (quasiquote (/ (unquote left) (unquote right)))) : scalar (unquote (quasiquote (var (unquote coordinate)))) : scalar; executable guards apply}{\frac{\partial}{\partial coordinate} (\frac{left}{right}) \to \frac{\frac{\partial}{\partial coordinate} (left) \times right - left \times \frac{\partial}{\partial coordinate} (right)}{{right}^{2}}} [partial-quotient]

Group: partial. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: C1 scalar expression in explicitly declared independent coordinates

Exact scalar-algebra check: unsupported.

Executable guards

((project (facts left right coordinate) (if (differentiable-term? (quasiquote (/ (unquote left) (unquote right))) facts) succeed fail)) (project (facts coordinate) (if (eq? (math-variable-role facts (quasiquote (var (unquote coordinate)))) (quote parameter)) fail succeed)) (math-factso facts (quasiquote ((nonzero (unquote right))))))

partial-sin

\frac{coordinate (coordinate) differentiable (\sin (operand)) (unquote (quasiquote (sin (unquote operand)))) : scalar (unquote (quasiquote (var (unquote coordinate)))) : scalar; executable guards apply}{\frac{\partial}{\partial coordinate} (\sin (operand)) \to \frac{\partial}{\partial coordinate} (operand) \times \cos (operand)} [partial-sin]

Group: partial. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: C1 scalar expression in explicitly declared independent coordinates

Exact scalar-algebra check: unsupported.

Executable guards

((project (facts operand coordinate) (if (differentiable-term? (quasiquote (sin (unquote operand))) facts) succeed fail)) (project (facts coordinate) (if (eq? (math-variable-role facts (quasiquote (var (unquote coordinate)))) (quote parameter)) fail succeed)))

partial-cos

\frac{coordinate (coordinate) differentiable (\cos (operand)) (unquote (quasiquote (cos (unquote operand)))) : scalar (unquote (quasiquote (var (unquote coordinate)))) : scalar; executable guards apply}{\frac{\partial}{\partial coordinate} (\cos (operand)) \to - (\frac{\partial}{\partial coordinate} (operand) \times \sin (operand))} [partial-cos]

Group: partial. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: C1 scalar expression in explicitly declared independent coordinates

Exact scalar-algebra check: unsupported.

Executable guards

((project (facts operand coordinate) (if (differentiable-term? (quasiquote (cos (unquote operand))) facts) succeed fail)) (project (facts coordinate) (if (eq? (math-variable-role facts (quasiquote (var (unquote coordinate)))) (quote parameter)) fail succeed)))

partial-exp

\frac{coordinate (coordinate) differentiable (\exp (operand)) (unquote (quasiquote (exp (unquote operand)))) : scalar (unquote (quasiquote (var (unquote coordinate)))) : scalar; executable guards apply}{\frac{\partial}{\partial coordinate} (\exp (operand)) \to \frac{\partial}{\partial coordinate} (operand) \times \exp (operand)} [partial-exp]

Group: partial. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: C1 scalar expression in explicitly declared independent coordinates

Exact scalar-algebra check: unsupported.

Executable guards

((project (facts operand coordinate) (if (differentiable-term? (quasiquote (exp (unquote operand))) facts) succeed fail)) (project (facts coordinate) (if (eq? (math-variable-role facts (quasiquote (var (unquote coordinate)))) (quote parameter)) fail succeed)))

partial-log

\frac{coordinate (coordinate) differentiable (\log (operand)) (unquote (quasiquote (log (unquote operand)))) : scalar (unquote (quasiquote (var (unquote coordinate)))) : scalar; executable guards apply}{\frac{\partial}{\partial coordinate} (\log (operand)) \to \frac{\frac{\partial}{\partial coordinate} (operand)}{operand}} [partial-log]

Group: partial. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: C1 scalar expression in explicitly declared independent coordinates

Exact scalar-algebra check: unsupported.

Executable guards

((project (facts operand coordinate) (if (differentiable-term? (quasiquote (log (unquote operand))) facts) succeed fail)) (project (facts coordinate) (if (eq? (math-variable-role facts (quasiquote (var (unquote coordinate)))) (quote parameter)) fail succeed)) (math-factso facts (quasiquote ((positive (unquote operand))))))

partial-function-chain

Apply the shared function chain rule using one-based argument positions. C1 permits one derivative, C2 permits two, and smooth permits higher derivatives.

\frac{Declared scalar function and sufficient regularity for the next derivative; algorithm applicability checked}{Derivative of f(u_1,...,u_n) = sum_i partial_i f(u_1,...,u_n) derivative of u_i} [partial-function-chain]

Group: partial. Modes: (forward check). Algorithm rule; this description has no fixed RuleSpec. Condition: Declared scalar function and sufficient regularity for the next derivative

Exact scalar-algebra check: unsupported.

partial-coordinate-symmetry

\frac{C2 operand; coordinate names and argument positions have separate orders; algorithm applicability checked}{Exchange mixed derivatives into ascending order} [partial-coordinate-symmetry]

Group: normalize. Modes: (forward check). Algorithm rule; this description has no fixed RuleSpec. Condition: C2 operand; coordinate names and argument positions have separate orders

Exact scalar-algebra check: unsupported.

partial-argument-symmetry

\frac{C2 operand; coordinate names and argument positions have separate orders; algorithm applicability checked}{Exchange mixed derivatives into ascending order} [partial-argument-symmetry]

Group: normalize. Modes: (forward check). Algorithm rule; this description has no fixed RuleSpec. Condition: C2 operand; coordinate names and argument positions have separate orders

Exact scalar-algebra check: unsupported.

components-sum

\frac{Cartesian scalar entries}{(\begin{matrix} a \\ b \\ c \end{matrix}) + (\begin{matrix} d \\ e \\ f \end{matrix}) \to (\begin{matrix} a + d \\ b + e \\ c + f \end{matrix})} [components-sum]

Group: components. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: Cartesian scalar entries

Exact scalar-algebra check: unsupported.

components-difference

\frac{Cartesian scalar entries}{(\begin{matrix} a \\ b \\ c \end{matrix}) - (\begin{matrix} d \\ e \\ f \end{matrix}) \to (\begin{matrix} a - d \\ b - e \\ c - f \end{matrix})} [components-difference]

Group: components. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: Cartesian scalar entries

Exact scalar-algebra check: unsupported.

components-negation

\frac{Cartesian scalar entries}{- ((\begin{matrix} a \\ b \\ c \end{matrix})) \to (\begin{matrix} - a \\ - b \\ - c \end{matrix})} [components-negation]

Group: components. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: Cartesian scalar entries

Exact scalar-algebra check: unsupported.

components-scale-left

\frac{s : scalar}{s \times (\begin{matrix} a \\ b \\ c \end{matrix}) \to (\begin{matrix} s \times a \\ s \times b \\ s \times c \end{matrix})} [components-scale-left]

Group: components. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: Cartesian scalar entries

Exact scalar-algebra check: unsupported.

components-scale-right

\frac{s : scalar}{(\begin{matrix} a \\ b \\ c \end{matrix}) \times s \to (\begin{matrix} s \times a \\ s \times b \\ s \times c \end{matrix})} [components-scale-right]

Group: components. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: Cartesian scalar entries

Exact scalar-algebra check: unsupported.

components-quotient

\frac{s : scalar}{\frac{(\begin{matrix} a \\ b \\ c \end{matrix})}{s} \to (\begin{matrix} \frac{a}{s} \\ \frac{b}{s} \\ \frac{c}{s} \end{matrix})} [components-quotient]

Group: components. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: Cartesian scalar entries

Exact scalar-algebra check: unsupported.

components-dot

\frac{Cartesian scalar entries}{(\begin{matrix} a \\ b \\ c \end{matrix}) \cdot (\begin{matrix} d \\ e \\ f \end{matrix}) \to a \times d + b \times e + c \times f} [components-dot]

Group: components. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: Cartesian scalar entries

Exact scalar-algebra check: unsupported.

components-cross

\frac{Cartesian scalar entries}{(\begin{matrix} a \\ b \\ c \end{matrix}) \times (\begin{matrix} d \\ e \\ f \end{matrix}) \to (\begin{matrix} b \times f - c \times e \\ c \times d - a \times f \\ a \times e - b \times d \end{matrix})} [components-cross]

Group: components. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: Cartesian scalar entries

Exact scalar-algebra check: unsupported.

components-zero

\frac{Cartesian scalar entries}{\vec{0} \to (\begin{matrix} 0 \\ 0 \\ 0 \end{matrix})} [components-zero]

Group: components. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: Cartesian scalar entries

Exact scalar-algebra check: unsupported.

gradient-components

\frac{differentiable (f) f : scalar; executable guards apply}{\nabla f \to (\begin{matrix} \frac{\partial}{\partial x} (f) \\ \frac{\partial}{\partial y} (f) \\ \frac{\partial}{\partial z} (f) \end{matrix})} [gradient-components]

Group: spatial. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: C1 scalar field in an ordered Cartesian basis

Exact scalar-algebra check: unsupported.

Executable guards

((basiso facts x y z))

divergence-components

\frac{differentiable ((\begin{matrix} a \\ b \\ c \end{matrix})); executable guards apply}{\nabla \cdot ((\begin{matrix} a \\ b \\ c \end{matrix})) \to \frac{\partial}{\partial x} (a) + \frac{\partial}{\partial y} (b) + \frac{\partial}{\partial z} (c)} [divergence-components]

Group: spatial. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: C1 components in an ordered Cartesian basis

Exact scalar-algebra check: unsupported.

Executable guards

((basiso facts x y z))

curl-components

\frac{differentiable ((\begin{matrix} a \\ b \\ c \end{matrix})); executable guards apply}{\nabla \times ((\begin{matrix} a \\ b \\ c \end{matrix})) \to (\begin{matrix} \frac{\partial}{\partial y} (c) - \frac{\partial}{\partial z} (b) \\ \frac{\partial}{\partial z} (a) - \frac{\partial}{\partial x} (c) \\ \frac{\partial}{\partial x} (b) - \frac{\partial}{\partial y} (a) \end{matrix})} [curl-components]

Group: spatial. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: C1 components in an oriented ordered Cartesian basis

Exact scalar-algebra check: unsupported.

Executable guards

((basiso facts x y z))

laplacian-scalar-components

\frac{c2 (f) f : scalar}{Δ f \to \nabla \cdot (\nabla f)} [laplacian-scalar-components]

Group: spatial. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: C2 scalar field in Cartesian space

Exact scalar-algebra check: unsupported.

laplacian-vector-components

\frac{c2 ((\begin{matrix} a \\ b \\ c \end{matrix}))}{Δ ((\begin{matrix} a \\ b \\ c \end{matrix})) \to (\begin{matrix} Δ a \\ Δ b \\ Δ c \end{matrix})} [laplacian-vector-components]

Group: spatial. Modes: (forward check). Declarative RuleSpec; metavariables denote terms. Condition: C2 Cartesian components

Exact scalar-algebra check: unsupported.

integrate-polynomial

\frac{Exact polynomials in independent coordinates and constant parameters; bounded sparse expansion; algorithm applicability checked}{The unique polynomial primitive with zero value at the integration coordinate's origin} [integrate-polynomial]

Group: polynomial-calculus. Modes: (forward check). Algorithm rule; this description has no fixed RuleSpec. Condition: Exact polynomials in independent coordinates and constant parameters; bounded sparse expansion

Exact scalar-algebra check: unsupported.

solve-polynomial-poisson

\frac{Exact polynomials in independent coordinates and constant parameters; bounded sparse expansion; algorithm applicability checked}{A polynomial particular solution of Delta u = f, with zero initial value and first derivative in the selected axis} [solve-polynomial-poisson]

Exact scalar-algebra check: unsupported.

expand-polynomial

\frac{Exact polynomials in explicit coordinates/parameters; bounded expansion; algorithm applicability checked}{Exact sparse polynomial expansion} [expand-polynomial]

Group: polynomial-calculus. Modes: (forward check). Algorithm rule; this description has no fixed RuleSpec. Condition: Exact polynomials in explicit coordinates/parameters; bounded expansion

Exact scalar-algebra check: unsupported.

math-rule->content把指定规则名转成文章内容：包括其结构化模式和可用说明。因此上面的规则卡片和运行时目录来自同一份定义，不会各自漂移。

若想只看写过说明的规则，可以约束documentation不等于#f：

((curl-curl-identity "Replace the curl of a curl by the gradient of the divergence minus the vector Laplacian. The field must be C2; declaring it divergence-free is a separate premise and a separate rewrite.") (grad-product "Differentiate the product of two scalar fields with the gradient product rule. C1 regularity suffices; no second derivatives or smoothness assumptions are required.") (curl-product "Expand the curl of a scalar times a vector field in oriented Cartesian space. The cross product is grad(f) cross E, in that order; reversing it changes the sign. Both factors need C1 regularity.") (differentiate-product "Generate the derivative of each factor separately and sum the two products. This rule constructs derivative terms; subsequent differentiation and simplification steps compute and reduce them.") (differentiate-quotient "Apply the quotient rule on the domain where the denominator is nonzero. The derivative remains a symbolic term until later passes process its operands and simplify the result.") (differentiate-function "Apply the shared function chain rule using one-based argument positions. C1 permits one derivative, C2 permits two, and smooth permits higher derivatives.") (cancel-common-factor "A check-only cancellation theorem. Its denominator side condition is explicit in the premise and must remain in the surrounding domain requirements.") (partial-function-chain "Apply the shared function chain rule using one-based argument positions. C1 permits one derivative, C2 permits two, and smooth permits higher derivatives."))

规则docstring解释其数学含义、适用条件或容易误解的细节，不会被当作新前提，也不会更改规则逻辑。这让说明可用于程序查询，同时保留普通Scheme函数的简单定义方式。