Thanks for the references, Josef. I will read them with interest.

It may be worth stating, though, that the project I wrote about is more 
type theory than expert system and that my questions probably pertain 
mostly to mathematical-reasoning efforts.

Cheers,
Rene

On 2/3/14, 7:17 PM, Josef Urban wrote:
> 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

Reply via email to