# IW Meeting 2009-02-12

### From Inference Web

## Contents |

## agenda

todo list from the previous meetings

Inference Web tools

- Probe-It! broken in one demo

combine proof

- Geoff's comments on Mizar
- three issues
- identify combinable proofs
- compute equivalence of formula
- evaluate and compare proof quality

## notes

### Probe-It not compatible with java 1.5

- jre 1.6 is missing on stephan's and peter's mac machine
- geoff: For IDV we compile for 1.5, so it runs on "old" Macs. You could do that too Paulo.
- Probe-It is depending on three components that is on java 1.6
- PML API
- jena http://jena.sourceforge.net/downloads.html
- ??

- Geoff has provided some help for mac users

Run Utilities/Java/Java Preferences The following image shows how to configure java on mac

### schedule

- Paulo need our server up on Jan 25 for a site visit
- peter is scheduling a spcdis telecon for next week. want to make sure everybody is available.

### combine proof

generate more proofs

- Mizar proofs: http://www.cs.miami.edu/~tptp/MizarTPTP/TPTPProofs/
- an example proof http://www.cs.miami.edu/~tptp/MizarTPTP/Articles/newton.html
- a proof to a theorem 'th9' http://www.cs.miami.edu/~tptp/MizarTPTP/TPTPProofs/newton/newton__t9_newton
- this is a big corpus of proof which are quite compatible

- Geoff: i like the huge corpus of pml proofs but what is i think most useful is the opportunity to combine them and show where we add value. i do not even need combined proofs with different sources - if i just have the same answer with different sources and/or different methods, then it is also of use

- another interesting point

http://us.metamath.org/mpegif/mmtheorems.html The Metamath Proof Explorer starts with basic axioms (ZFC) to build up mathematical proofs in number theory, set theory, etc. For example, the complete proof of 2 + 2 = 4 involves 2,452 sub-theorems. This proof system might be a potential testbed for proof combining, although we have sufficient proof data already. What makes their system interesting is two-fold: precise definitions of proof nodes and intriguing connections among proofs.

## pml api

pml for seismology and earth topography (1)

- by july pml for data on (1) will be ready.
- pml for environmental data studying reflectance in alaska
- by july, will have a repository of pml in 3 areas - seismology, earth science, and data fusion for geology
- paulo is creating a layer on top of the api. the pml wrappers are what utep is changing

## todo

- geoff talk to cynthia on translation
- todo - geoff will talk to josef and norm mcgil about a mapping between mizar and metamath