Metamathとは 意味・読み方・使い方

Metamath is a computer-assisted proof checker. It has no specific logic embedded and can simply be regarded as a device to apply inference rules to formulas. Simplicity is the master concept in the design of Metamath: the language of Metamath, employed to state the definitions, axioms, inference rules and theorems is only composed of a handful of keywords and all the proofs are checked using one simple algorithm based on the substitution of variables (with optional provisos for what variables must remain distinct after a substitution is made). This "substitution" is just the simple replacement of a variable with an expression and not the proper substitution described in works on predicate calculus.