Look also at Ontic: http://lambda-the-ultimate.org/classic/message6641.html http://ttic.uchicago.edu/%7Edmcallester/ontic-spec.ps http://www.cs.cmu.edu/afs/cs/project/ai-repository/ai/areas/kr/systems/ontic/0.html http://citeseer.ist.psu.edu/witty95ontic.html
Josh On Saturday 21 April 2007 17:45, Lukasz Stafiniak wrote: > Hi, > > How should an AGI think about formal mathematical ideas? What > formalization of a logical argument would be the most digestible? Many > mathematicians don't like formalized approaches, because they think on > the level of patterns (which correspond to understanding the reality), > not on the "assembly" level of formalizations. But AGI could take > advantage of perceiving and manipulating the formalization itself. > Although I live not far from Bialystok, I don't think Mizar is the > right formalization to use. Mizar is a sophisticated artificial > language. What I would like to see used is a powerful, intelligible > system with frugal formulation, a logic whose assertions combine > theorems and proofs, and whose proofs are algorithms: the Calculus of > Inductive Constructions (CIC). The system that implements CIC is Coq > (http://coq.inria.fr/). The AGI would still need to think on the > patterns level (sometimes called heuristics), and it would still be > very useful to translate Mizar to CIC (perhaps the AGI could do the > translation...) but to have a being embodied at once in the physical > world and in the CIC world, wow! That would certainly prove something > ;-) > > Best regards, > Lukasz Stafiniak > > ----- > This list is sponsored by AGIRI: http://www.agiri.org/email > To unsubscribe or change your options, please go to: > http://v2.listbox.com/member/?&; ----- This list is sponsored by AGIRI: http://www.agiri.org/email To unsubscribe or change your options, please go to: http://v2.listbox.com/member/?member_id=231415&user_secret=fabd7936
