Metamath
2018-02-04
metamath
Formal proof verifier and proof assistant
NAME
metamath - Formal proof verifier and proof assistant
SYNOPSIS
metamath [ commands | file ]
DESCRIPTION
metamath is a formal proof verifier and proof assistant for the Metamath language. It can be initialized via a series of commands or with a data base file, which can then be explored interactively.
For details about the Metamath language and the command-line interface, type help into the command prompt, or read the Metamath book [1], which should have been installed along with the package.
LANGUAGE
A Metamath database consists of a sequence of three kinds of tokens separated by white space (which is any sequence of one or more white space characters). The set of keyword tokens is ${, $}, $c, $v, $f, $e, $d, $a, $p, $., $=, $(, $), $[, and $]. The latter four are called auxiliary or preprocessing keywords. A label token consists of any combination of letters, digits, and the characters hyphen, underscore, and period. The label of an assertion is used to refer to it in a proof. A math symbol token may consist of any combination of the 93 printable ascii(7) characters other than $. All tokens are case-sensitive.
$( comment $) | |
Comments are ignored. | |
$[ file $] | |
Include the contents of a file. | |
${ statements $} | |
Scoped block of statements. A math symbol becomes active when declared and stays active until the end of the block in which it is declared. | |
$v symbols $. | |
Declare symbols as variables. A variable may not be declared a second time while it is active, but it may be declared again (as a variable, but not as a constant) after it becomes inactive. | |
$c symbols $. | |
Declare symbols as constants. A constant must be declared in the outermost block and may not be declared a second time. | |
label $f constant variable $. | |
Variable-type hypothesis to specify the nature or type of a variable (such as ‘let x be an integer.’). A variable must have its type specified in a $f statement before it may be used in a $e, $a, or $p statement. There may not be two active $f statements containing the same variable. | |
label $e constant symbols $. | |
Logical hypothesis, expressing a logical truth (such as ‘assume x is prime’) that must be established in order for an assertion requiring it to also be true. | |
$d variables $. | |
Disjoint variable restriction. For distinct active variables, it forbids the substitution of one variable with another. | |
label $a constant symbols $. | |
Axiomatic assertion. | |
label $p constant symbols $= proof $. | |
Provable assertion. The proof is a sequence of statement labels. This label sequence serves as a set of instructions that the Metamath program uses to construct a series of math symbol sequences. The construction must ultimately result in the math symbol sequence contained between the $p and $= keywords of the $p statement. For details, see section 4.3 in [1]. Proofs are most easily written using the interactive prompt in metamath. |
FILES
/usr/share/metamath
Data base files for several formal theories.
SEE ALSO
[1] Norman Megill: Metamath, A Computer Language for Pure Mathematics