/nyaya

proof language based on https://en.wikipedia.org/wiki/Sequent_calculus and https://us.metamath.org/.

Primary LanguageRustGNU General Public License v3.0GPL-3.0

nyaya

This aims to be a very simple theorem verifier based on sequent calculus and Metamath to educate myself and others about the basics of theorem provers.

Examples are on the examples directory.

For instructions on installation and how to prove your theorems in nyaya, see tutorial.

For the mathematical foundations of nyaya, see foundations.

License

all files in ./examples are available under public domain, while the interpreter is licensed under GPLv3.0