This seems close to what has been tried in Project Halo. There was a talk about automated reasoning challenges over the textbook "Campbell Biology" last year at the CADE KInAR workshop: http://www.michael-wessel.info/papers/kinar-2013-b.pdf . There is of course also the recent $1B IBM is pumping into Watson: http://www.reuters.com/article/2014/01/09/us-ibm-watson-idUSBREA0808U20140109
Josef On Mon, Feb 3, 2014 at 5:09 AM, Rene Vestergaard <[email protected]> wrote: > I will shortly be attempting to reach a, for us, non-standard audience with a > project that includes the verification of the complete reasoning in a > molecular-biology monograph. > > The primary sales argument is by proxy: there's a Curry-Howard component to > the project that allows us to solve an open problem in the application domain. > > The primary scientific argument concerns formal reasoning, including the > value of formalising/verifying a large body of knowledge, be it a textbook, a > monograph, a "big" result, or similar. > > I have my own personal arguments for why large applications are a good idea: > - tests of and guidance for maturity/naturalness/expressivity of tools and > methodologies, > - development of libraries/momentum/etc., > - teaching/industrial/etc. purposes, > - retrodiction and, of course, > - assuring large case splits and proof by reflection. > > I was hoping people would help me with > 1) what big applications have been done? what arguments were used? > 2) do the arguments hold up in retrospect? > > While 1) can be answered by references, I am particularly hoping that some of > the people behind these projects would attempt to answer 2) as best as > possible. > > Cheers, > Rene ------------------------------------------------------------------------------ Managing the Performance of Cloud-Based Applications Take advantage of what the Cloud has to offer - Avoid Common Pitfalls. Read the Whitepaper. http://pubads.g.doubleclick.net/gampad/clk?id=121051231&iu=/4140/ostg.clktrk _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
