GNU Aris is a logical proof program that supports propositional and predicate logic, as well as Boolean algebra and arithmetical logic, in the form of abstract sequences. Aris uses a predefined set of inference and equivalence rules, but allows the user to reference older proofs, including proofs done in Isar. Aris uses standard logical symbols, and a natural deduction interface, making it easy for beginners to work with.
Aris can be found on the main GNU ftp server: http://ftp.gnu.org/gnu/aris/ (via HTTP) and ftp://ftp.gnu.org/gnu/aris/ (via FTP). It can also be found on the GNU mirrors; please use a mirror if possible.
Documentation for Aris is available online, as is documentation for most GNU software. You may also find more information about Aris by running info aris or man aris, or by looking at /usr/share/doc/aris/, /usr/local/doc/aris/, or similar directories on your system. A brief summary is available by running aris --help.
Aris has the following mailing lists:
Security reports that should not be made immediately public can be sent directly to the maintainer. If there is no response to an urgent issue, you can escalate to the general security mailing list for advice.
Development of Aris, and GNU in general, is a volunteer effort, and you can contribute. For information, please read How to help GNU. If you'd like to get involved, it's a good idea to join the discussion mailing list (see above).
Aris 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.
The Free Software Foundation is the principal organizational sponsor of the GNU Operating System. Support GNU and the FSF by buying manuals and gear, joining the FSF as an associate member, or making a donation, either directly to the FSF or via Flattr.