Mimir is a deep inference tool to test exhaustively the proving capability of a given set of rewrite rules on linear inferences involving a specific (given) number of variables. It is written in C with efficiency in mind: a balance was specifically chosen between memory consumption and speed. Parallel processing is implemented via the OpenMPI library, but it is also perfectly suited for single-process computing. The source also provides a framework for a more general suite of deep inference tools.
It was written as part of a project in the summer of 2012 at the Department of Computer Science of the University of Bath, the details of which (and more detail on Mimir's development) are discussed in the final writeup. I delivered a talk on 2012-12-13 to the Mathematical Foundations Group at the department as well, slides for which can be found below:
For now, source code is available via git from https://github.com/blahblahson/mimir.git. It can also be browsed online via GitHub.
No real documentation exists at the moment, so your best bet is to refer to the source code (main.c in particular).
To compile, for now just run:
mpicc src/*.c -o mim -Wall -O3 -lm
at the top level directory after you've pulled it from the repository. Then running mim on the command line and referring to main.c should be sufficient for figuring out the basics for now.
Send all bug reports to . If you fork the project or use some of the code, shoot me an email too (although you are not obligated to).
Standard MIT/X11 terms.
Permission is hereby granted, free of charge, to any person obtaining
a copy of this software and associated documentation files (the
"Software"), to deal in the Software without restriction, including
without limitation the rights to use, copy, modify, merge, publish,
distribute, sublicense, and/or sell copies of the Software, and to
permit persons to whom the Software is furnished to do so, subject to
the following conditions:
The above copyright notice and this permission notice shall be
included in all copies or substantial portions of the Software.
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
See also COPYING.