search

windsteiger / Theorema

Theorema: A System for Automated Reasoning (Theorem Proving) and Automated Theory Exploration based on Mathematica
GNU General Public License v3.0
71 stars 14 forks source link

Formula evaluation timings #37

Open amaletzk opened 11 years ago

amaletzk commented 11 years ago

I made the observation that evaluating formulae becomes extremely slow as notebooks grow big. This is most probably due to the fact that Theorema searches the entire notebook for applicable global declarations and therefore creates the very big raw notebook object, and so on. Evaluation of global declarations, and also of computations, is still fast though. Maybe change the way Theorema does all the "book-keeping" before actually processing formulae.

windsteiger commented 11 years ago

See related issue#28. Do the notebooks contain proofs, or are they just big as they are?

amaletzk commented 11 years ago

The notebook I have tried out does not contain a single proof, but is very big (many definitions, computations, text cells). It is, by the way, Bruno's Groebner-Rings file that I'm currently adapting to Theorema 2.

windsteiger commented 10 years ago

We add a "batch processing" mode, where checking duplicate labels, searching for applicable globals, and updating the KB browser is not done "live". We cache some of the necessary information in order not having to analyze the nb-expression every time.