gnu_metalogic-inference's Introduction
MLI compilation, installation, and running MLI requires: C++14 compiler, and the GMP multiprecision library. If one wants to compile beyond what is in the distribution, Flex is needed to compile lexer.ll, and Bison to compile parser.yy. Note: Compiles on MacOS 10.12 using g++ (MacPorts gcc6 6.3.0_0) 6.3.0 and Apple LLVM version 8.0.0 (clang-800.0.42.1), Flex 2.5.37, and Bison 3.0.4. To compile: move to the directory src, and issue the shell command ./configure && make which results in the program 'mli'. To install: with suitable permissions, type 'make install' to install the programs 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 To run the program 'mli' examples: In a suitable working directory, 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 statement, and writes the result 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 commented out. So just change this, to include the correct line. ----- Copyright (C) 2017 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/>.
gnu_metalogic-inference's People
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.