# metalogic-inference

**Repository Path**: mirrors_gnu/metalogic-inference

## Basic Information

- **Project Name**: metalogic-inference
- **Description**: No description available
- **Primary Language**: Unknown
- **License**: GPL-3.0
- **Default Branch**: master
- **Homepage**: None
- **GVP Project**: No

## Statistics

- **Stars**: 0
- **Forks**: 0
- **Created**: 2020-10-26
- **Last Updated**: 2026-07-19

## Categories & Tags

**Categories**: Uncategorized

**Tags**: None

## README

This package contains GNU MLI, the MetaLogic Inference program.

  MLI requirements, compilation, installation, and running


* Installation and Building

For basic building and installation, see below. See the file INSTALL for more detailed compilation and installation instructions.


* Requirements

MLI requires: C++20 compiler. If one wants to compile beyond what is included in the distribution, Flex is needed to compile lexer.ll, and Bison to compile parser.yy.

Note: MLI compiles on MacOS using GCC g++ and clang++, Flex, and Bison.


* Simple build and installation

To compile: Move to the directory named 'mli-<version>', and issue the shell command
  ./configure && make
which results in the program 'mli' in the directory 'src'.

To install: With suitable permissions, type 'make install' to install the program, and any data files and documentation.

After installation, as a first check that the program is properly installed and in the PATH, try say
  mli --help
or
  mli --version

The install location can be changed for example to the home directory by running
  ./configure prefix=$HOME && make
or any other directory supplying an absolute path instead of $HOME.

Out of source builds are also possible, like making a directory at the side (same parent directory) of the 'mli-<version>' directory, say called 'build', and another called 'install', and running in the 'build' directory:
  ../mli-<version>/configure prefix=$PWD/../install && make
Then 'make install' will install in the 'install' directory.


* Running examples

To run the program 'mli' examples:

In a suitable working directory, assuming the docs are in the standard location, copy in the installed examples by:
  cp -R /usr/local/share/doc/mli/examples .
Then move to the directory examples:
  cd examples

Run the file "main.mli" by
  mli main.mli
which interprets it, attempts to verify the parsed statements, and writes the result of the analysis in a file "main.mlo", where the verifications that failed are marked "unproved". Any earlier file "main.mlo" is overwritten. Also, a file "main.log" is written with more detailed debugging information about the verification process.

The proofs in the file that "main.mli" includes can then be altered, and mli rerun, to see the difference in verification:

The last statement in the file tests/TK1.mli has a deliberate error in the proof, and the correct proof is commented out. So just change this to include the correct line, rerun 'mli main.mli', and verify in main.mlo that the proof now has been passed.

-----

Copyright (C) 2017, 2021-2026 Hans Åberg.

This file is part of MLI, MetaLogic Inference.

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 3 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, see <http://www.gnu.org/licenses/>.