Re: [gnu-soc] GNU GSOC 2023 application

[Jose E. Marchesi]

> Jose E. Marchesi <jemarch@gnu.org> ezt írta (időpont: 2023. febr. 8., Sze,
> 11:43):
>
>>
>> Hi Kovács.
>>
>> I have added the ideas for aris and xaos to the page.
>>
>
> Hi Jose, thank you!
>
>
>> However,
>>
>> > - 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?

I think it is better yes.
I have added that to the description.

Thanks!