IW Meeting 2011-03-24

From Inference Web

Jump to: navigation, search

Contents

Meeting info

Proof combination

LAST TIME: next: 1) automating (Cynthia) (todo: Geoff to answer Cynthia's question for how to automate) 2) todo: geoff find more candidate problems.

Geoff points to: http://inference-web.org/proofs/tptpwork/tptpextract/test032111/SEU/SEU140+2/gcc_run_2.html

Geoff followed through Cynthia's results and is sending correction.

TODO: Geoff continue looking through Cynthia's output.

It all seems to be working. Cynthia is still doing combination by hand. They need confidence that technique is correct before automating it.

TODO: Cynthia still to automate combination.

Geoff has list of 10 candidate problems from some time ago (one from medicine; one from process control).

Tim: The original list of 10 vs. some more? Geoff: Can do more, but can't remember why we wanted more.

Number of iterations of search last week vs. this week?

Each iteration is showing improvement, so there is hope with current approach.

Take away: still press forward and should get results.

Paulo

Suggesting priority: focus on publishing some results, even if not conclusive so we can show activity that we are doing.

combination in formal world is idealized version of real world, so we should start targeting

Geoff: http://pxtp2011.loria.fr/ due 2 May submission deadline


We need to brainstorm on how to use it in different domains.

Geoff: Paulo owes two paragraphs on how to use combination in two domains.

Geoff: result does not need to be amazing, just convincing. We still need to find the convincing result.

Paulo: We need to work on applying the combinations.

The combination algorithm needs: Given a justification DAG, report a number for the quality. The hill climbing takes it from there.

Geoff: induction is computationally challenging. Paulo: but scientific proofs have induction. Geoff: induction: prove base case, prove an induction case.

e.g., In data analysis, one sees lots of ravens -- all were black; ASSUME all ravens are black.

Geoff's upcoming "fork" - 1) applying combo to sci domains (Paulo argues more people do/interested in this) 2) keep pushing for deep results in formal (Paulo argues less people in this discipline).

Geoff wants simple example using an induction problem in the scientific domain. Needs gut feeling for it.

TODO: 14 Apr Paulo gives written description of a process for data calibration, or stat analysis.

Future IW

Need to plan outcomes for next coming months.

objective: papers

TODO: Tim needs to write up his provenance application to LOGD.

Personal tools
Navigation