| Name : metamath-data
| |
| Version : 0.196
| Vendor : openSUSE
|
| Release : bp153.2.1
| Date : 2021-03-25 11:09:40
|
| Group : Productivity/Scientific/Math
| Source RPM : metamath-0.196-bp153.2.1.src.rpm
|
| Size : 40.03 MB
| |
| Packager : https://bugs_opensuse_org
| |
| Summary : Data base files for metamath
|
Description :
This package contains Metamath data base files for several formal theories.
* set.mm – Logic and set theory database (see Ch. 3 of the Metamath book).
* nf.mm – Logic and set theory database for Quine\'s New Foundations set theory.
* hol.mm – Higher order logic (simple type theory) database.
* iset.mm – Intuitionistic logic database.
* ql.mm – Quantum logic database.
* demo0.mm – Demo of simple formal system (see Ch. 2 of the Metamath book).
* miu.mm – Hofstadter\'s MIU-system (see Appendix D of the Metamath book).
* big-unifier.mm – A unification stress test (see comments in the file).
* peano.mm – A presentation of Peano arithmetic by Robert Solovay.
|
RPM found in directory: /packages/linux-pbone/ftp5.gwdg.de/pub/opensuse/repositories/openSUSE:/Backports:/SLE-15-SP3/step/noarch |
