127 lines
4.2 KiB
Groff
127 lines
4.2 KiB
Groff
.\" t -*- coding: UTF-8 -*-
|
|
.\" Man page for metamath
|
|
.\"
|
|
.\" Copyright (C) 2018 Aaron Puchert.
|
|
.\"
|
|
.\" This program is free software; you can redistribute it and/or modify
|
|
.\" it under the terms of the GNU General Public License as published by
|
|
.\" the Free Software Foundation; either version 2 of the License, or
|
|
.\" (at your option) any later version.
|
|
.\"
|
|
.\" This program is distributed in the hope that it will be useful,
|
|
.\" but WITHOUT ANY WARRANTY; without even the implied warranty of
|
|
.\" MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
|
|
.\" GNU General Public License for more details.
|
|
.\"
|
|
.\" You should have received a copy of the GNU General Public License
|
|
.\" along with this program; if not, write to the Free Software
|
|
.\" Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
|
|
.\"
|
|
.TH metamath 1 "2018-02-04" Metamath "User Manuals"
|
|
.SH NAME
|
|
metamath \- Formal proof verifier and proof assistant
|
|
.SH SYNOPSIS
|
|
.BI "metamath [ " "commands" " | " "file" " ]"
|
|
.SH DESCRIPTION
|
|
.B metamath
|
|
is a formal proof verifier and proof assistant for the Metamath language.
|
|
It can be initialized via a series of
|
|
.I commands
|
|
or with a data base
|
|
.IR file ,
|
|
which can then be explored interactively.
|
|
.PP
|
|
For details about the Metamath language and the command-line interface, type
|
|
.B help
|
|
into the command prompt, or read the Metamath book [1], which should have been
|
|
installed along with the package.
|
|
.SH 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
|
|
.BR ${ ", " $} ", " $c ", " $v ", " $f ", " $e ", " $d ", " $a ", " $p ", "
|
|
.BR $. ", " $= ", " $( ", " $) ", " $[ ", and " $] .
|
|
The latter four are called auxiliary or preprocessing keywords. A
|
|
.I 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
|
|
.I symbol
|
|
token may consist of any combination of the 93 printable
|
|
.BR ascii (7)
|
|
characters other than
|
|
.BR $ .
|
|
All tokens are case-sensitive.
|
|
.TP
|
|
.BI $( " comment " $)
|
|
Comments are ignored.
|
|
.TP
|
|
.BI $[ " file " $]
|
|
Include the contents of a
|
|
.IR file .
|
|
.TP
|
|
.BI ${ " 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.
|
|
.TP
|
|
.BI $v " symbols " $.
|
|
Declare
|
|
.I 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.
|
|
.TP
|
|
.BI $c " symbols " $.
|
|
Declare
|
|
.I symbols
|
|
as constants. A constant must be declared in the outermost block and may not be
|
|
declared a second time.
|
|
.TP
|
|
.IB "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
|
|
.B $f
|
|
statement before it may be used in a
|
|
.BR $e ", " $a ", or " $p
|
|
statement. There may not be two active
|
|
.B $f
|
|
statements containing the same variable.
|
|
.TP
|
|
.IB "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.
|
|
.TP
|
|
.BI $d " variables " $.
|
|
Disjoint variable restriction. For distinct active
|
|
.IR variables ,
|
|
it forbids the substitution of one variable with another.
|
|
.TP
|
|
.IB "label " $a " constant symbols " $.
|
|
Axiomatic assertion.
|
|
.TP
|
|
.IB "label " $p " constant symbols " $= " proof " $.
|
|
Provable assertion. The
|
|
.I proof
|
|
is a sequence of statement
|
|
.IR label s.
|
|
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
|
|
.BR $p " and " $=
|
|
keywords of the
|
|
.B $p
|
|
statement. For details, see section 4.3 in [1].
|
|
Proofs are most easily written using the interactive prompt in
|
|
.BR metamath .
|
|
.SH FILES
|
|
.I /usr/share/metamath
|
|
.RS
|
|
Data base files for several formal theories.
|
|
.SH SEE ALSO
|
|
.B "[1]"
|
|
Norman Megill:
|
|
.UR http://us.metamath.org/downloads/metamath.pdf
|
|
Metamath, A Computer Language for Pure Mathematics
|
|
.UE .
|