I have added the ideas for aris and xaos to the page.
Hi Jose, thank you!
> - Short description of the program: 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.
I think that description is a bit lacking for someone who doesn't know
what a "logical proof program" is.
We can add something like this:
A logical proof program can prove mathematical statements by using strict reasoning steps,
based on axioms and rewrite rules. GNU Aris supports manual creation of such proofs
and it can verify if a proof is correct according to the axioms and rewrite rules.
Therefore, it can give good support for undergraduate math courses like logic or abstract algebra.
Do you think it suffices?