Hi, Il 09/11/19 12:27, 'Filip Cernatescu' via Metamath ha scritto: > Automatic prover for a+b,a-b,a×b,a/b, a<b,a>b... it will be necessary?
Maybe not necessary, but I believe it would be good to have automated provers for everything that can be automated. Unfortunately not any problem arising in real number (or integer number) theories can be decided automatically, but some can. Z3 can prove statements (and emit related proofs) in a range of theories, also using real numbers, and eventually I would like to be able to convert those to Metamath. Giovanni. -- Giovanni Mascellani <[email protected]> Postdoc researcher - Université Libre de Bruxelles -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/cc9dbcc0-c89d-ef94-b1d9-daa78c35cc64%40gmail.com.
signature.asc
Description: OpenPGP digital signature
