My old idea which I periodically recall is to create computer game which has as a base model where winning (making progress in) the game meaning solving some real world problems (like proving some mathematical theorems or building theories). That way people will not be wasting time during gaming but doing some useful work.
Archive for January, 2010
Playing games = Solving problems
Wednesday, January 20th, 2010Digital Gastronomy
Tuesday, January 19th, 2010Cornucopia is a concept design for a personal food factory that brings the versatility of the digital world to the realm of cooking. In essence, it is a three dimensional printer for food, which works by storing, precisely mixing, depositing and cooking layers of ingredients.
Cornucopia’s cooking process starts with an array of food canisters, which refrigerate and store a user’s favorite ingredients. These are piped into a mixer and extruder head that can accurately deposit elaborate combinations of food. While the deposition takes place, the food is heated or cooled by Cornucopia’s chamber or the heating and cooling tubes located on the printing head. This fabrication process not only allows for the creation of flavors and textures that would be completely unimaginable through other cooking techniques, but it also allows the user to have ultimate control over the origin, quality, nutritional value and taste of every meal.
Proof Systems
Monday, January 18th, 2010proof assistant author
- HOL John Harrison, Konrad Slind, Rob Arthan
- Mizar Andrzej Trybulec
- PVS Bart Jacobs, John Rushby
- Coq Laurent Thery, Pierre Letouzey, Georges Gonthier
- Otter/Ivy Michael Beeson, William McCune
- Isabelle/Isar Markus Wenzel, Larry Paulson
- Alfa/Agda Thierry Coquand
- ACL2 Ruben Gamboa
- PhoX Christophe Raffalli, Paul Roziµere
- IMPS William Farmer
- Metamath Norman Megill
- Theorema Wolfgang Windsteiger, Bruno Buchberger, Markus Rozenkranz
- Lego Conor McBride
- Nuprl Paul Jackson
- mega Christoph BenzmÄuller, Armin Fiedler, Andreas Meier, Martin Pollet, JÄorg Siekmann
- B method Dominique Cansell
- Minlog Helmut Schwichtenberg
Mizar Math Library
Sunday, January 17th, 2010Found this and consider as a right direction for formalizing mathematics knowledges. Going to spend time and promote it among the Institute of Mathematics scientists.