Skip to content
/ mai Public

mai: MAth Interpreter with Standard Foundations

License

Notifications You must be signed in to change notification settings

amka66/mai

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

34 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

mai: MAth Interpreter with Standard Foundations

Abstract

mai is an educational tool for computer-assisted mathematics. In this repository, the language of mathematics is defined from first principles. Using horc (see here), a fully operational implementation of the language of mathematics is obtained at no additional cost. The implementation spans all elements of the language and may particularly serve as a language parser and a proof assistant.

A unique feature of mai is its simplicity – its entire foundations are implemented as a set of rules of inference in the minimalist meta-language horc (see here). This implementation directly parallels textbook definitions of the 'standard' foundations of mathematics including first-order logic and set theory. Accordingly, mai may accompany courses in logic and set theory, and may serve as a reference implementation that can be executed, scrutinized, and experimented with.

To illustrate how mai can be used, a formal mathematical exposition of set theory is included, with emphasis on building a powerful toolset for the working mathematician (work in progress). It is easy to try mai and examine the foundations of mathematics on any computer preinstalled with Docker, by running:

docker run --rm amka66/mai set-theory.pl

Features

  • Free and open-source interpreter for computer-assisted mathematics, called mai, currently for educational use. It includes:

    • Shell for writing formal mathematics.
    • The capability of keeping track of theorems and definitions and verifying their validity.
    • Comprehensive coverage of the language of mathematics and its foundations.
  • mai includes a formal and executable definition of the 'standard' foundations of mathematics, including:

  • These foundations are implemented in their entirety as a set of rules of inference in a minimalist logical framework called horc (see here).

    • This implementation directly parallels textbook definitions of logic and set theory, and thus may serve as a reference definition of those topics that can be executed, scrutinized, and used in practice.

    • Technically, horc is implemented in Prolog and operates within the SWI-Prolog ecosystem, and so is mai.

  • mai is available as a Docker image hosted in Docker Hub. It requires no installation and can be downloaded and executed with a single command on any computer preinstalled with Docker.

  • Via Prolog, mai supports the implementation of higher layers of automation – namely, proof tactics – aimed to speed up proof search without compromising the logic.

  • At this point, mai should be considered an educational tool and proof-of-concept due to the limited number of tactics that are currently implemented.

How to Execute?

mai can be automatically downloaded and executed with no need for local installation (nor cloning the project repository) on any computer preinstalled with Docker. In the command prompt, enter:

$ docker run [-it] [--rm] [-v <local_dir>:<mount_dir>] amka66/mai [<prolog_file>]

  • <prolog_file> (optional): Path to a Prolog script file (optionally ending with the extension .pl), written in ISO-compliant or SWI-Prolog-compliant Prolog. If present, it is to contain a formal mathematical exposition in the form of Prolog queries to be verified in mai. It may possibly include other content too, intended to extend the shell, initialize an interactive Prolog session with the user, etc. The provided path is within the container (consider option -v to access the host machine). A script included in mai that may be used here is set-theory.pl, containing a formal mathematical exposition of set theory.

  • -it (optional): Option for docker run, which, in our case, sets an interactive Prolog session with the user after loading and executing <prolog_file> (if present).

  • -v <local_dir>:<mount_dir> (optional): Option for docker run, which mounts a local directory <local_dir> within the host machine to a specified mount point (a directory) <mount_dir> within the container. The mount point may be used to refer to Prolog scripts in the host machine.

  • --rm (optional): Option for docker run, which purges the container once it has stopped running. Unless one would like to examine the container after it has stopped running, it is safe to use this option to purge obsolete containers at once.

Examples

$ docker run --rm amka66/mai set-theory.pl
Load and execute the included Prolog script set-theory.pl, containing a formal mathematical exposition of set theory to be verified with mai.

$ docker run -it --rm amka66/mai
Start an interactive Prolog session with the user.

$ docker run -it --rm -v ~/myfiles:/mnt amka66/mai /mnt/linear-algebra.pl
Load and execute a Prolog script stored locally in ~/myfiles/linear-algebra.pl, and then start an interactive Prolog session with the user.

Getting Started

  • Read through README.md (this file).
  • Install Docker (if missing).
  • To make sure it works, have mai verify the included exposition of set theory by executing: docker run --rm amka66/mai set-theory.pl.
  • As in common mathematical practice, only a fragment of the mathematical foundations underlying mai is typically used in formal mathematical expositions.
    • To gain working knowledge with mai, examine the mathematical exposition of set theory included in set-theory.pl. The steps in the exposition consist of shell functions (defined in zfc-shell.pl) and the arguments of those functions consist of the concrete syntax of logical formulae (defined in zfc-concrete.pl).
    • Read through set-theory.pl for the development of powerful set-theoretical tools for the working mathematician (work in progress).
  • For a comprehensive understanding of mai and its mathematical foundations start by learning horc (see Where to Begin?). Then:

Overview of Source Code (for developers)

We invite those who share our vision to join us in making this into an industrial-strength free and open-source framework for computer-assisted mathematics.

The following is an account of the files included in the repository.

File Directory Description
fol-1.hn src/horn Horn knowledge base (see <horn_file> in here) defining classical first-order logic with equality (FOL) -- both syntax, operations on syntax, and a proof system called natural deduction.
fol-2.hn src/horn Horn knowledge base introducing a set of admissible (derived) rules that can be used for proving theorems. Some of these are intended to support the extension of FOL theories with theorems and definitions, per fol-3.hn and fol-4.hn.
fol-3.hn src/horn Horn knowledge base defining a FOL theory (including a subset the language, and axioms) and the proper way to extend theories with theorems and definitions -- in case of a finite number of axioms (mathematical expositions of 'type I').
fol-4.hn src/horn Horn knowledge base defining the proper way to extend FOL theories with theorems and definitions -- in case of a possibly infinite number of axioms (mathematical expositions of 'type II').
zfc.hn src/horn Horn knowledge base defining the primitive language and axioms of the Zermelo-Fraenkel set theory with Choice (ZFC). It is a starting point for mathematical expositions of type II (per fol-4.hn).
zfc-concrete.pl src/prolog Prolog script defining concrete syntax and syntactic sugar for FOL and ZFC, and the conversion to and from abstract syntax.
zfc-shell.pl src/prolog Prolog script defining several shell (top-level) functions to support for mathematical expositions of type II (per fol-4.hn).
set-theory.pl src/prolog/math Prolog script containing a formal mathematical exposition of set theory in mai (work in progress).
run.sh src/bash Bash script serving only as interface. Executed first (top) when a Docker container starts, and receiving its parameters from the command line.
create-temp-file-and-run-horc.sh src/bash Invoked by run.sh, this Bash script and assembles everything together. (1) It creates a temporary Prolog script that loads zfc-shell.pl, and an optional Prolog script <prolog_file>. (2) It invokes horc on the knowledge base zfc.hn (which loads the other knowledge bases), accompanied by the temporary Prolog script from (1).
build-docker.sh, run-docker.sh, test-docker.sh bin Bash utility scripts for developers: building a Docker image, running a Docker image in a container, and testing a Docker image.
Dockerfile . Docker script for building a Docker image.
.dockerignore . List of files to be excluded in Dockerfile's copy command.
.gitignore . List of files to be excluded from Git.
.gitattributes . File extensions and their associated languages.
mai.bib . BibTeX file containing project's bibliography.
LICENSE . License file (plain text).
README.md . This file (Markdown).

Additional Resources

License

Copyright 2020–2022 Amir Kantor

Licensed under the Apache License, Version 2.0 -- see LICENSE.txt.

Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License.