Parsing is a proof obligation which is kind of cool / insane. since fol is embedded, the distinction between sets and predicates is interestingly flimsy? Tarski S2 Disjointness and nominal logic? A directed prolog of sorts. Proof checking as computation. You write which rules to resolve on, it adds the requirements to the goal stack

d(X,Y) :- dif(X,Y).
a(axname, [path, X, Y]) :- d(), f(), f(), e(), e().
f(name, TypeCode, Var) --> []

a(nam, )

The RPN nature means we describe proof trees in a depth first manner. This is similar to bussproofs.

l1 $e stuff1
l2 $e stuff2
myax $a$ mydude

is like asserting an inference rule

l1 stuff      l2 stuff
----------------------- myax
      mydude

hoare in metamath

path proofs in metamath

$c vert path edge a b c d e f $.
$v x y z $.
$f vert x $.
$f vert y $.
$f vert z $.

min $e edge x y $.
base-path $a path x y $.

maj $e path y z $.
trans-path $a path x z $.

verta $a vert a $.
vertb $a vert b $.
vertc $a vert c $.
$a vert d $.
$a vert e $.

edgeab $a edge a b $.
edgebc $a edge b c $.

pathac $p path a c $.

echo '
$c path edge vert 1 2 3 4 $.
$v x y z $.
vert1 $a vert 1 $.
vert2 $a vert 2 $.
vert3 $a vert 3 $.
edge12 $a edge 1 2 $.
edge23 $a edge 2 3 $.
vertx $f vert x $.
verty $f vert y $.
vertz $f vert z $.
edgexy $e edge x y $.
basepath $a path x y $.
path12 $p path 1 2 $=
  vert1 vert2 edge12 basepath $.
path23 $p path 2 3 $=
  vert2 vert3 edge23 basepath $.
pathyz $e path y z $.
transpath $a path x z $.
path13 $p path 1 3 $=
  edge12 vert1 vert2 vert3 path23 transpath $.

' > /tmp/path.mm
metamath 'read "/tmp/path.mm"' "verify proof *" "exit"

https://drops.dagstuhl.de/opus/volltexte/2023/18384/pdf/LIPIcs-ITP-2023-9.pdf automated theorem proving for metamath

metamath 0

https://github.com/digama0/mm0

metamath-lamp https://github.com/digama0/mm0

metamath book

metamath pcc drat datalog prolog congruence closure

Metamath exe

Chapter 6 of the book

metamath

Commands: They have modifiers

read
write
verify proof *
exit
open log close log
erase
submit
beep
search
show proof
open tex close tex

Proof commands

prove
sanity set unification_timout set empty_substition
assign step laebel [/ no_unify] delete step

import subprocess

class Connection():
    def __init__(self, path="metamath"):
        self.path = path
        self.proc = subprocess.Popen(path, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.PIPE)
    def cmd(self, str):
        self.proc.stdin.write(f"{str}")
        self.proc.stdin.flush()
        return self.proc.stdout.readline()
    def read(self, path):
        return self.cmd(f"read {path}\n")
    def write(self, path):
        self.proc.stdin.write(f"write {path}\n")
        self.proc.stdin.flush()
        return self.proc.stdout.readline()
    def prove(self, label):
        self.proc.stdin.write(f"prove {path}\n")
        self.proc.stdin.flush()
        return self.proc.stdout.readline()        

import cmd

class Metamath(cmd.Cmd):
    prompt = "MM> "

    def do_prove(self,arg):
        print("Proving", arg)
        self.connection.prove(arg)
    def do_verify(self,arg):

Metamath.cmdloop()

Python Checker

metamath python checker

# some excerpts from the above checker

# Tell me the types and I don't need the code
Label = str
Var = str
Const = str
Stmttype = typing.Literal["$c", "$v", "$f", "$e", "$a", "$p", "$d", "$="]
StringOption = typing.Optional[str]
Symbol = typing.Union[Var, Const]
Stmt = list[Symbol]
Ehyp = Stmt
Fhyp = tuple[Var, Const]
Dv = tuple[Var, Var]
Assertion = tuple[set[Dv], list[Fhyp], list[Ehyp], Stmt]
FullStmt = tuple[Stmttype, typing.Union[Stmt, Assertion]]


class Frame:
    """Class of frames, keeping track of the environment."""

    def __init__(self) -> None:
        """Construct an empty frame."""
        self.v: set[Var] = set()
        self.d: set[Dv] = set()
        self.f: list[Fhyp] = []
        self.f_labels: dict[Var, Label] = {}
        self.e: list[Ehyp] = []
        self.e_labels: dict[tuple[Symbol, ...], Label] = {}
        # Note: both self.e and self.e_labels are needed since the keys of
        # self.e_labels form a set, but the order and repetitions of self.e
        # are needed.

class FrameStack(list[Frame]):
    """Class of frame stacks, which extends lists (considered and used as
    stacks).
    """
    # ... .stuff ...
    pass

def apply_subst(stmt: Stmt, subst: dict[Var, Stmt]) -> Stmt:
    """Return the token list resulting from the given substitution
    (dictionary) applied to the given statement (token list).
    """
    result = []
    for tok in stmt:
        if tok in subst:
            result += subst[tok]
        else:
            result.append(tok)
    vprint(20, 'Applying subst', subst, 'to stmt', stmt, ':', result)
    return result

class MM:
    """Class of ("abstract syntax trees" describing) Metamath databases."""

    def __init__(self, begin_label: Label, stop_label: Label) -> None:
        """Construct an empty Metamath database."""
        self.constants: set[Const] = set()
        self.fs = FrameStack()
        self.labels: dict[Label, FullStmt] = {}
        self.begin_label = begin_label
        self.stop_label = stop_label
        self.verify_proofs = not self.begin_label

    # ... stuff ....

    def treat_step(self,
                   step: FullStmt,
                   stack: list[Stmt]) -> None:
        """Carry out the given proof step (given the label to treat and the
        current proof stack).  This modifies the given stack in place.
        """
        vprint(10, 'Proof step:', step)
        if is_hypothesis(step):
            _steptype, stmt = step
            stack.append(stmt)
        elif is_assertion(step):
            _steptype, assertion = step
            dvs0, f_hyps0, e_hyps0, conclusion0 = assertion
            npop = len(f_hyps0) + len(e_hyps0)
            sp = len(stack) - npop
            if sp < 0:
                raise MMError(
                    ("Stack underflow: proof step {} requires too many " +
                     "({}) hypotheses.").format(
                        step,
                        npop))
            subst: dict[Var, Stmt] = {}
            for typecode, var in f_hyps0:
                entry = stack[sp]
                if entry[0] != typecode:
                    raise MMError(
                        ("Proof stack entry {} does not match floating " +
                         "hypothesis ({}, {}).").format(entry, typecode, var))
                subst[var] = entry[1:]
                sp += 1
            vprint(15, 'Substitution to apply:', subst)
            for h in e_hyps0:
                entry = stack[sp]
                subst_h = apply_subst(h, subst)
                if entry != subst_h:
                    raise MMError(("Proof stack entry {} does not match " +
                                   "essential hypothesis {}.")
                                  .format(entry, subst_h))
                sp += 1
            for x, y in dvs0:
                vprint(16, 'dist', x, y, subst[x], subst[y])
                x_vars = self.fs.find_vars(subst[x])
                y_vars = self.fs.find_vars(subst[y])
                vprint(16, 'V(x) =', x_vars)
                vprint(16, 'V(y) =', y_vars)
                for x0, y0 in itertools.product(x_vars, y_vars):
                    if x0 == y0 or not self.fs.lookup_d(x0, y0):
                        raise MMError("Disjoint variable violation: " +
                                      "{} , {}".format(x0, y0))
            del stack[len(stack) - npop:]
            stack.append(apply_subst(conclusion0, subst))
        vprint(12, 'Proof stack:', stack)

Metamath exe

assign step laebel [/ no_unify] delete step

Python Checker

`assign step laebel [/ no_unify]` `delete step`