Function Repository Resource:

MetamathImport

Source Notebook

Import and work with a Metamath database

Contributed by: Mario Carneiro and Nikolay Murzin

ResourceFunction["MetamathImport"][src]

imports Metamath source code from src and returns a MetamathObject.

Details and Options

The src can be a File, URL or String.

Options for ResourceFunction["MetamathImport"] may be one of the following:

"Verify"

False

whether to verify theorem proofs or not

MetamathObject has the following properties:

"Symbols"

list of symbols

"Constants"

list of constants

"Variables"

list of variables

"Statements"

list of statements

"Axioms"

list of axioms

"Theorems"

list of theorems

"Definitions"

list of definitions

"DependencyGraph"

theorem proof dependency graph

{"SyntaxTree", stmt}

syntax breakdown tree of a statement

{"SyntaxDependencyTree", stmt}

syntax dependency tree of a statement

{"SimpleSyntaxTree", stmt}

simplified syntax tree

{"ProofTree", thm}

proof tree of a theorem

{"ProofGraph", thm}

proof graph of a theorem

{"TokenEventGraph", thm}

token event proof graph of a theorem

ResourceFunction["MetamathImport"] special inputs:

"SetMM"

setmm database

"NormMegillWolframAxioms"

Norm Megill's proofs of the Wolfram Axioms

"ASCIITable"

ASCII replacement rules

Examples

Basic Examples (6)

Import Metamath source code with several constants and a simple axiom:

In[1]:=

ResourceFunction["MetamathImport"]["
$c = 0 S 1 $.
wp $a = 0 S 1 $.
"]

Out[1]=

Import a basic Metamath source code sample with 4 constants, 5 variables, 5 floating hypotheses, 1 axiom and 2 proved theorems:

In[2]:=

ResourceFunction["MetamathImport"]["
$c ( ) -> wff $.
$v p q r s t $.
wp $f wff p $.
wq $f wff q $.
wr $f wff r $.
ws $f wff s $.
wt $f wff t $.
w-> $a wff ( p -> q ) $.
w->(->) $p wff ( r -> ( s -> t ) ) $= wr ws wt w-> w-> $.
w(->)-> $p wff ( ( r -> s ) -> t ) $= wr ws w-> wt w-> $.
"]

Out[2]=

Construct a proof tree:

In[3]:=

$ResourceFunction[ InterpretationBox[ TagBox[ DynamicModuleBox[{Typeset`open = False}, FrameBox[ PaneSelectorBox[{False -> GridBox[{{ PaneBox[ GridBox[{{ AdjustmentBox[ StyleBox[ StyleBox[ StyleBox[ "\"[\[FilledSmallSquare]]\"", FontColor -> RGBColor[ 0.8745098039215686, 0.2784313725490196, 0.03137254901960784]], "ResourceFunctionIcon"], FontFamily -> "Source Sans Pro Black", FontWeight -> "Heavy", PrivateFontOptions -> {"OperatorSubstitution" -> False}, FontSize -> 0.6538461538461539 Inherited, ShowStringCharacters -> False], BoxBaselineShift -> -0.25, BoxMargins -> {{0, 0}, {-1, -1}}], StyleBox[ RowBox[{ StyleBox["MetamathImport", "ResourceFunctionLabel"], " "}], FontColor -> GrayLevel[0.1], FontSize -> Rational[12, 13] Inherited, ShowStringCharacters -> False, ShowAutoStyles -> False]}}, GridBoxSpacings -> {"Columns" -> {{0.25}}}], Alignment -> Left, FrameMargins -> {{3, 0}, {0, 0}}, BaselinePosition -> Baseline, BaseStyle -> {LineSpacing -> {0, 0}, LineBreakWithin -> False}], ItemBox[ PaneBox[ TogglerBox[ Dynamic[Typeset`open], {True -> DynamicBox[ FEPrivate`FrontEndResource["FEBitmaps", "IconizeCloser"]], False -> DynamicBox[ FEPrivate`FrontEndResource["FEBitmaps", "IconizeOpener"]]}, BaselinePosition -> Baseline, Appearance -> None, ContentPadding -> False, FrameMargins -> 0], Alignment -> Left, FrameMargins -> {{1, 1}, {0, 0}}, BaselinePosition -> Baseline], Frame -> {{ RGBColor[ 0.8313725490196079, 0.8470588235294118, 0.8509803921568627, 0.5], False}, {False, False}}]}}, GridBoxAlignment -> {"Columns" -> {{Left}}, "Rows" -> {{Baseline}}}, GridBoxItemSize -> {"Columns" -> {{Automatic}}, "Rows" -> {{Automatic}}}, GridBoxSpacings -> {"Columns" -> {{0}}, "Rows" -> {{0}}}, BaselinePosition -> {1, 1}], True -> GridBox[{{ GridBox[{{ PaneBox[ GridBox[{{ AdjustmentBox[ StyleBox[ StyleBox[ StyleBox[ "\"[\[FilledSmallSquare]]\"", FontColor -> RGBColor[ 0.8745098039215686, 0.2784313725490196, 0.03137254901960784]], "ResourceFunctionIcon"], FontFamily -> "Source Sans Pro Black", FontWeight -> "Heavy", PrivateFontOptions -> {"OperatorSubstitution" -> False}, FontSize -> 0.6538461538461539 Inherited, ShowStringCharacters -> False], BoxBaselineShift -> -0.25, BoxMargins -> {{0, 0}, {-1, -1}}], StyleBox[ RowBox[{ StyleBox["MetamathImport", "ResourceFunctionLabel"], " "}], FontColor -> GrayLevel[0.1], FontSize -> Rational[12, 13] Inherited, ShowStringCharacters -> False, ShowAutoStyles -> False]}}, GridBoxSpacings -> {"Columns" -> {{0.25}}}], Alignment -> Left, FrameMargins -> {{3, 0}, {0, 0}}, BaselinePosition -> Baseline, BaseStyle -> {LineSpacing -> {0, 0}, LineBreakWithin -> False}], ItemBox[ PaneBox[ TogglerBox[ Dynamic[Typeset`open], {True -> DynamicBox[ FEPrivate`FrontEndResource["FEBitmaps", "IconizeCloser"]], False -> DynamicBox[ FEPrivate`FrontEndResource["FEBitmaps", "IconizeOpener"]]}, BaselinePosition -> Baseline, Appearance -> None, ContentPadding -> False, FrameMargins -> 0], Alignment -> Left, FrameMargins -> {{1, 1}, {0, 0}}, BaselinePosition -> Baseline], Frame -> {{ RGBColor[ 0.8313725490196079, 0.8470588235294118, 0.8509803921568627, 0.5], False}, {False, False}}]}}, GridBoxAlignment -> {"Columns" -> {{Left}}, "Rows" -> {{Baseline}}}, GridBoxItemSize -> {"Columns" -> {{Automatic}}, "Rows" -> {{Automatic}}}, GridBoxSpacings -> {"Columns" -> {{0}}, "Rows" -> {{0}}}, BaselinePosition -> {1, 1}]}, { StyleBox[ PaneBox[ GridBox[{{ RowBox[{ TagBox["\"Version (latest): \"", "IconizedLabel"], " ", TagBox["\"2.0.0\"", "IconizedItem"]}]}, { TagBox[ TemplateBox[{"\"Documentation »\"", "https://resources.wolframcloud.com/FunctionRepository/resources/b78a92a5-6ec3-462b-bcdc-a0971c7ea539/"}, "HyperlinkURL"], "IconizedItem"]}}, GridBoxAlignment -> {"Columns" -> {{Left}}}, DefaultBaseStyle -> "Column", GridBoxItemSize -> {"Columns" -> {{Automatic}}, "Rows" -> {{Automatic}}}], Alignment -> Left, FrameMargins -> {{5, 4}, {0, 4}}, BaselinePosition -> Baseline], "DialogStyle", FontFamily -> "Roboto", FontSize -> 11]}}, GridBoxAlignment -> {"Columns" -> {{Left}}, "Rows" -> {{Baseline}}}, GridBoxItemSize -> {"Columns" -> {{Automatic}}, "Rows" -> {{Automatic}}}, BaselinePosition -> {1, 1}, GridBoxDividers -> {"Columns" -> {{None}}, "Rows" -> {False, { GrayLevel[0.8]}, False}}]}, Dynamic[Typeset`open], BaselinePosition -> Baseline, ImageSize -> Automatic], BaselinePosition -> Baseline, FrameMargins -> {{0, 0}, {1, 0}}, FrameStyle -> RGBColor[ 0.8313725490196079, 0.8470588235294118, 0.8509803921568627], Background -> RGBColor[ 0.9686274509803922, 0.9764705882352941, 0.984313725490196], RoundingRadius -> 4, DefaultBaseStyle -> {}]], {"FunctionResourceBox", RGBColor[0.8745098039215686, 0.2784313725490196, 0.03137254901960784], "MetamathImport"}, TagBoxNote -> "FunctionResourceBox"], ResourceFunction["MetamathImport"], BoxID -> "MetamathImport", Selectable -> False]][<|"Symbols" -> <|"(" -> "Constant"["("], ")" -> "Constant"[")"], "->" -> "Constant"["->"], "wff" -> "Constant"["wff"], "p" -> "Variable"["p"], "q" -> "Variable"["q"], "r" -> "Variable"["r"], "s" -> "Variable"["s"], "t" -> "Variable"["t"]|>, "Statements" -> <|"wp" -> "Hypothesis"["wp", {"wff", "p"}], "wq" -> "Hypothesis"["wq", {"wff", "q"}], "wr" -> "Hypothesis"["wr", {"wff", "r"}], "ws" -> "Hypothesis"["ws", {"wff", "s"}], "wt" -> "Hypothesis"["wt", {"wff", "t"}], "w->" -> "Axiom"["w->", {"wff", "(", "p", "->", "q", ")"}, {{}, { "Hypothesis"["wp", {"wff", "p"}], "Hypothesis"["wq", {"wff", "q"}]}, {}}], "w->(->)" -> "Theorem"[ "w->(->)", {"wff", "(", "r", "->", "(", "s", "->", "t", ")", ")"}, {{}, { "Hypothesis"["wr", {"wff", "r"}], "Hypothesis"["ws", {"wff", "s"}], "Hypothesis"["wt", {"wff", "t"}]}, {}}, {"wr", "ws", "wt", "w->", "w->"}], "w(->)->" -> "Theorem"[ "w(->)->", {"wff", "(", "(", "r", "->", "s", ")", "->", "t", ")"}, {{}, { "Hypothesis"["wr", {"wff", "r"}], "Hypothesis"["ws", {"wff", "s"}], "Hypothesis"["wt", {"wff", "t"}]}, {}}, {"wr", "ws", "w->", "wt", "w->"}]|>|>]["ProofTree", "w(->)->"]$

Out[3]=

Construct a proof graph:

In[4]:=

Out[4]=

Construct a detailed syntax tree breakdown:

In[5]:=

Out[5]=

Construct a simplified syntax tree:

In[6]:=

Out[6]=

Options (1)

Verify (1)

Verifying theorems expands proofs with more information:

In[7]:=

$Cases[ResourceFunction["MetamathImport"][ "\n$c ( ) -> wff $.\n$v p q r s t $.\nwp $f wff p $.\nwq $f wff q $.\nwr $f wff r $.\nws $f wff s $.\nwt $f wff t $.\nw-> $a wff ( p -> q ) $.\nw->(->) $p wff ( r -> ( s -> t ) ) $= wr ws wt w-> w-> $.\nw(->)-> $p wff ( ( r -> s ) -> t ) $= wr ws w-> wt w-> $.\n", "Verify" -> False]["Statements"], "Theorem"[label_, _, _, proof_] :> label -> proof]$

Out[7]=

In[8]:=

$Cases[ResourceFunction["MetamathImport"][ "\n$c ( ) -> wff $.\n$v p q r s t $.\nwp $f wff p $.\nwq $f wff q $.\nwr $f wff r $.\nws $f wff s $.\nwt $f wff t $.\nw-> $a wff ( p -> q ) $.\nw->(->) $p wff ( r -> ( s -> t ) ) $= wr ws wt w-> w-> $.\nw(->)-> $p wff ( ( r -> s ) -> t ) $= wr ws w-> wt w-> $.\n", "Verify" -> True]["Statements"], "Theorem"[label_, _, _, proof_] :> label -> proof]$