\( \newcommand\D{\mathrm{d}} \newcommand\E{\mathrm{e}} \newcommand\I{\mathrm{i}} \newcommand\bigOh{\mathcal{O}} \newcommand{\cat}[1]{\mathbf{#1}} \newcommand\curl{\vec{\nabla}\times} \newcommand{\CC}{\mathbb{C}} \newcommand{\NN}{\mathbb{N}} \newcommand{\QQ}{\mathbb{Q}} \newcommand{\RR}{\mathbb{R}} \newcommand{\ZZ}{\mathbb{Z}} \)
UP | HOME

Mizar

Table of Contents

1. Useful Definitions

  • Element of X is defined in subset_1.miz , lines 67 et seq.
  • Subset of X is defined in subset_1.miz (line 99), but it just means Element of bool X; and bool X is defined in zfmisc_1.miz (line 71) as bool X -> set means Z in it iff Z c= X (and c= is the subset operator, defined in tarski.miz, as we would expect its meaning \(X\subseteq Y\iff (\forall x, x\in X\implies x\in Y)\))

2. Random

3. Lessons Learned

3.1. Vocabulary Files

When defining new terms, well, we should get started by doing something like: 

user@computer:~/$ mkdir -p work/first-article/
user@computer:~/$ cd work/first-article/
user@computer:~/work/first-article/$ mkdir DICT
user@computer:~/work/first-article/$ mkdir TEXT
user@computer:~/work/first-article/$ mkdir PREL

Now for a "Hello World" type Mizar file: just create a new predicate foobar. We do this by creating first-article/DICT/TMP.voc and sticking one line in it: 

Rfoobar

Then in first-article/TEXT/TMP.miz we would have: 

environ
vocabularies TMP; :: this is important! Without it, you get an error


begin

definition
  let a,b be set;
  pred a,b foobar means
  :Def1:
  a = b;
end;

Without the vocabularies TMP; line, you'll get a "301: Predicate symbol expected" error, basically Mizar telling you that you forgot to include foobar as a predicate in your vocabulary file.

4. Installing on Raspberry Pi

This was surprisingly simple. I usually keep source code related stuff in ~/src/, so here's the bash commands that got me cooking: 

alex@pi:~$ cd src
alex@pi:~/src/$ mkdir mizar
alex@pi:~/src/$ cd mizar
alex@pi:~/src/mizar/$ wget http://mizar.uwb.edu.pl/~softadm/pub/system/arm-linux/mizar-8.1.09_5.59.1363-arm-linux.tar
alex@pi:~/src/mizar/$ tar -xvf mizar-8.1.09_5.59.1363-arm-linux.tar
README
install.sh
mizbin.tar.gz
mizdoc.tar.gz
mizshare.tar.gz

alex@pi:~/src/mizar$ ls

install.sh                            mizbin.tar.gz  mizshare.tar.gz
mizar-8.1.09_5.59.1363-arm-linux.tar  mizdoc.tar.gz  README

alex@pi:~/src/mizar$ sudo ./install.sh --default
...

Then I added one line of code to my ~/.bash_profile: 

# at the end of ~/.bash_profile
MIZFILES=/usr/local/share/mizar

And, voilà/, once we've =source ~.bashprofile= we'll be able to start proving in no time. Unfortunately, I still have problems trying to get it working on my Raspberry Pi.

5. Exporting MIZFILES on Linux

On Ubuntu, I noticed it was insufficient to add MIZFILES=/usr/local/share/mizar followed by export MIZFILES to my .bashrc; instead I needed to add a line to /etc/environment, namely: 

# in /etc/environment, at the end
MIZFILES=/usr/local/share/mizar

After rebooting the computer, emacs expands (substitute-in-file-name "$MIZFILES") correctly to /usr/local/share/mizar. This allows me to compile a Mizar file in Emacs with C-c Ret.

6. References

Last Updated 2022-12-31 Sat 08:23.