IW Meeting 2009-02-12

From Inference Web

Jump to: navigation, search



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


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
  • Geoff has provided some help for mac users
Run Utilities/Java/Java Preferences
The following image shows how to configure java on mac

Image:java on mac.png


  • 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

  • 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
 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


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