The Coq mailing list

[Marko Malikovi� <marko AT ffri.hr>]

Dear mr. Cedric,

>> When I start a difficult proof which takes time and memory Coq simply
>> die after minute or two. Its interface disappears from the screen
>> without any message about the reason for it. This is happening on the
>> computer with Microsoft Windows Vista Business Service Pack 2. The
>> computer has the AMD Athlon processor at 1.80 GHz and 4 GB of RAM.
>> Does anyone know what's going on?

> I guess you meant coqide; you also should be more precise on the
> problem you were trying to solve. Taking 1 or 2 minutes, is really a
> bad omen.

No, I meant coqtop. Problem is so demanding and proof take so much time
because it's problem within Presburger arithmetic which I try to solve
using omega. It use many hypothesis and axioms. Problem is provable. I
have proved it in theory!

> Does your problem arise at Qed time?

The proof can never be achieved and Coq does not stop at Qed time, but
before.

Thank you,

Marko Malikoviæ

-----------------------
Dr. Sc. Marko Malikoviæ
Filozofski fakultet
Sveuèili¹te u Rijeci
---------------------
Ph.D. Marko Malikoviæ
Faculty of Humanities and Social Sciences
University of Rijeka, Croatia
-----------------------------
marko AT ffri.hr
http://www.ffri.hr/~marko
-------------------------