In this tutorial, we build an implementation of first-order logic (FOL) in MMT.
It assumes that
CONTENT,The MMT installer should take care of this
Actually, we will skip this step for now because only advanced users need to define their own meta-logic.
Instead, we can choose one of the meta-logics already defined in MMT.
The most important example is the logical framework LF, whose MMT URI is
This theory is defined in the archive MMT/urtheories, which is automatically cloned into the folder CONTENT when setting up MMT.
Other important meta-logics defined in this archive include
http://cds.omdoc.org/urtheories?PLFextends LF with shallow polymorphism
http://cds.omdoc.org/urtheories?LFModulo, which extends LF with a rewrite system
These can also be combined.
For FOL, LF is sufficient as a meta-logic.
We create a new file
fol.mmt, in which we will define FOL.
It does not matter where this file is located. But to allow for running MMT build targets over it later, it is convenient to place it in a new MMT archive:
create a file
MANIFEST.MF in it containing (at least) the lines
id: myarchive narration-base: http://mydomain.org/myarchive
The id is some string that is used to refer to the archive. The narration base is some URI that is used as the default namespace for forming unique identifiers for the content of the archive.
Open the file in jEdit and create an empty theory:
namespace http://mydomain.org/mmt-example [GS] theory FOL : http://cds.omdoc.org/urtheories?LF = [GS]
namespacedeclaration defines a unique namespace (a URI) for our example.The URI does not have to be a URL, i.e., it does not have to point to a physical location. It only acts as a unique identifier.
theoryintroduces an MMT theory called
http://cds.omdoc.org/urtheories?LF.Alternatively, we can write
ur:?LFbecause the namespace prefix definition
import ur http://cds.omdoc.org/urtheories [GS]is implicitly present.
[GS]refers to ASCII 29, the toplevel delimiter used by MMT. In jEdit, it can be inserted via the symbol button for it or by typing
From this point on forwards, defining a language proceeds according to LF.
The details of doing so are given in the self-documenting mmt files in the archive
CONTENT/MMT/examples, which has been cloned automatically when setting up MMT.
It contains the full definition of
FOL in the file
To complete this step of the tutorial, copy over the declarations in this file step by step.
(Note that this tutorial makes you use a different namespace than the that file. That’s important to make sure all declarations have unique URIs.)
To insert Unicode symbols, you can use LaTeX commands with j instead of .
\rightarrow. And because that one is so important,
jra is a shortcut for it.
The complete list of preconfigured abbreviations can be found in the section
Abbreviations of the jEdit settings.
We can start the MMT web server from within jEdit to view our definition in the browser:
mmtas the console language
server on 8080in the console (or some other port number)
To build your archive, use the command
build myarchive mmt-omdoc fol.mmt. This will build all
mmt files in your archive and convert them into
omdoc (which is the XML format that MMT uses internally, corresponding to the binary files produced by a compiler).
omdoc files are put into the folders
omdoc file per source file) and
omdoc file per module in those source files).
Additionally, index files for fast querying are placed in the folder
You can build the archive from within jEdit (by using the jEdit console as above).
Alternatively, you can build it directly from the MMT shell without involving jEdit.
Start the shell by running
build myarchive mmt-omdoc fol.mmt server on 8081
The shell is completely independent from jEdit (but works with the same archives). Therefore, we use a different port number above.
Eventually, you can leave the shell by typing
We can now apply our defined system to formalize some knowledge. We pick algebra as an example.
Create a file
algebra.mmt in your archive and put
namespace http://mydomain.org/mmt-example [GS] theory Semigroup : ?FOL = [GS]
This creates a new theory for semigroups, this time using our new theory
FOL as the meta-theory.
Because both theories are in the same namespace, we can use a relative URI to refer to
FOL, we do not give the details of the formalization here.
Instead, we refer to the self-documenting file
tutorial/2-algebra.mmt in the archive
Like before, you can now
build myarchive mmt-omdoc algebra.mmt
server on 8081.