IW Meeting 2013-10-03

From Inference Web

Jump to: navigation, search

Contents

Meeting Information

Agenda

Discharge

Example: http://browser.inference-web.org/iwbrowser/NodeSetBrowser?w=900&mg=999&st=Dag&fm=Raw&url=http%3A%2F%2Finference-web.org%2Fproofs%2Ftptp%2FSolutions%2FPUZ%2FPUZ001%2B1%2FEP---1.2%2Fanswer.owl%23answer

Please take a look at nodesets 47 and 48:

You can see the assumption and its negation.

And then take look towards the final conclusion of nodesets 1 and 2:

From nodeset 2 to 1, the refutation rule discharged nodeset 47 to prove nodeset 48.

Also see the summary view (be sure to click the "show" button of the "Justified by") :

http://browser.inference-web.org/iwbrowser/BrowseNodeSet?uri=http%3A%2F%2Finference-web.org%2Fproofs%2Ftptp%2FSolutions%2FPUZ%2FPUZ001%2B1%2FEP---1.2%2Fanswer.owl%23answer


ledToAnswer

PROPOSED: rename fromAnswer to pml:ledToAnswer subproperty of prov:hadDerivation, range is pml:Answer, domain is pml:Information .


OWL updates from resolutions

(Jim said he just added these, Tim just verified)

done: Jim to add pml:VariableMapping subclass of pml:Map to the ontology.

done: Jim to add pml:hasDescriptionTemplate range pml:Template domain Thing.

done: Jim to add capableOf domain Agent range Plan - what they can do in the future.

done: Jim add pml:wasGeneratedWithPlan property chain prov:wasGeneratedBy o prov:qualifiedAssociation o prov:hadPlan

done: Jim add pml:answers from pml:Answer range pml:Query UNION pml:Question subproperty of prov:wasDerivedFrom. pml:Answer min 1 pml:answers.

OWL publishing pragmatics

TODO: Jim to figure out why PML3 OMN files don't load in recent Protege versions. (precondition for other Jim tasks) Todo: also update a static link to an owl file of the newer version (once previous version is debugged )

(Tim runs a local "pml-3.0.sh" to aggregate all of the module's omn into pml-3.0.owl)

pml:Map vs. prov:Dictionary

We currently have pml:Map, but that needs to be reconciled with prov:Dictionary.

"Conceptually, a dictionary has a logical structure consisting of key-entity pairs. This structure is often referred to as a **map**, and is a generic indexing mechanism that can abstract commonly used data structures, including associative lists, relational tables, ordered lists, and more. " - prov-dict

Example of a prov Dictionary: (http://www.w3.org/TR/2013/NOTE-prov-dictionary-20130430/#dictionary-conceptual-definition)

@prefix prov: <http://www.w3.org/ns/prov#> .
@prefix xsd:  <http://www.w3.org/2001/XMLSchema#> .
@prefix :     <http://example.org/> .

:e1 a prov:Entity .
:e2 a prov:Entity .

:d1 a prov:Dictionary;
    prov:hadDictionaryMember [ 
       a prov:KeyEntityPair;
       prov:pairKey   "k1"^^xsd:string;
       prov:pairEntity :e1
     ], [ 
       a prov:KeyEntityPair;
       prov:pairKey   "k2"^^xsd:string;
       prov:pairEntity :e2
     ];
.

Tim doesn't like that prov:hadDictionaryMember isn't a subproperty of prov:hadMember, and that the dictionary Note doesn't use the Directed Qualification Pattern that is used throughout PROV-O. Instead, they reinvented terms that don't follow any pattern (b/c PROV-N couldn't handle it).

PML 3's current definition for a Map is "An associative array, an abstract data type composed of a collection of keys and a collection of values, where each key is associated with one value". So, our Map is a kind of prov:Dictionary that is also considered a prov:Plan. Since prov:Dictionaries have many more uses, I think we're justified in defining a pml:Map that specializes prov:Dictionary as a pml:Plan.

PROPOSE pml:Map subclassof prov:Dictionary, pml:Map (and thus pml:DeclarativePlan, prov:Plan)

PROPOSE pml:VariableMapping no longer subclass of pml:Map (instead, just subclass of pml:DeclarativePlan).

  • We agreed to modeling "prov:used [ a pml:VariableMapping, :A; prov:value 4 ]"
  • Having a pml:VariableMapping as a prov:Dictionary would lead to something like "prov:used [ a prov:Dictionary; prov:hadDictionaryMember [ a prov:KeyEntityPair; prov:pairKey "A"; prov:pairEntity [ prov:value 4 ] ] ] ."

Belief and Trust remodel

Approach is to reuse the Directed Qualification Pattern that PROV uses. Create an unqualified binary relation pml:believes, then permit qualification of it using pml:qualifiedBelief, pml:Belief, and prov:entity in the same way that PROV qualifies any of its unqualified relations.

:dinosaurs_still_roam_the_earth
  a pml:Information, prov:Entity;
  prov:value "Dinosaurs still roam the earth.";
.

:joe
   a prov:Agent;
   pml:believes :dinosaurs_still_roam_the_earth;
   pml:qualifiedBelief [
       a pml:Belief;
       prov:entity :dinosaurs_still_roam_the_earth;
       what:goesHere .95;
   ];
.


The property what:goesHere describing the Belief above could be prov:value, up:assertionConfidence, or up:contentConfidence. (See http://www2013.org/companion/p167.pdf for up:):

  • prov:value provides "direct representation" of the pml:Belief, but the value ".95" doesn't seem to cover enough of the Belief. It's too ambiguous, so we wont' use it.
  • Still waiting to here back from Tom on which of assertionConfidence and contentConfidence is appropriate.

The same pattern can be used for trust: the unqualified property pml:trusts, then permit qualification of it using pml:qualifiedTrust, pml:Trust, and prov:entity. The same property what:goesHere can be reused for Belief and Trust (and, any other weighting). The prov:entity is always used to indicate the trustee regardless of the type of trustee. If the trusted Entity happens to be a prov:Agent, then it will be typed as such.

:sally a prov:Agent .

:joe
   a prov:Agent;
   pml:trusts :sally;
   pml:qualifiedTrust [
       a pml:Trust;
       prov:entity :sally;
       what:goesHere .95;
   ];
.

QUESTION: Is Trust a Belief? And, if so, is that worth modeling? Belief is by Agents of Information, Trust is by Agents of Entities. To warp Trust as a Belief is to say that an Agent believes the Information that an Entity will (likely) maintain a condition in a future situation. And I think that's too intricate to bother modeling at this point.

PROPOSE: Add pml:believes domain prov:Agent, range pml:Information

PROPOSE: Rename BeliefElement to pml:Belief as a qualification class: Belief subclass (exactly 1 on prov:entity), (prov:entity allValuesFrom pml:Information)

  • This implies that we deprecate hasBelievedInformation and hasBelievingAgent

PROPOSE: Add pml:qualifiedBelief domain prov:Agent range pml:Belief

POLL: FloatBelief subclass Belief min 1 up:??Confidence

POLL: FloatTrust subclass Trust min 1 up:??Confidence

PROPOSE: deprecate FloatMetric

PROPOSE: Add pml:trusts domain prov:Agent, range pml:Entity

PROPOSE: Rename TrustElement to pml:Trust as a qualification class: Trust subclass (exactly 1 on prov:entity)

  • This implies that we deprecate hasTrustee and hasTrustor

Attendees

Meeting Preparation

Around the room

* Add a section for yourself 2 hours before meeting.
* Mark any discussion point that you would like to raise during meeting (with DURING MEETING). 
* Otherwise, assume that others will read the rest before meeting. 
* Also, please be considerate and read others' discussion points before the meeting starts.

Tim

Jim

James

Cynthia

Paulo

Patrice

Patrick

Deborah

  • i will need to get off by 4 today - meeting with potential funder
  • I am hoping we can move forward to wrapping up the mapping spreadsheet to get the tm/w3c submission document moving
  • IBM meeting yesterday was good - MIT, NYU, RPI, CMU partnering with IBM on cognitive computing effort - that is still being defined
  • writing for smart and connected health - with evan and patrice

Discussions

Discharge:

1) provenance vs. proof provenance: gathering evidence. Good change that things are ture. in proof, things are more strict.

provenance: facts, rules proof: inductive proofs, deductive, etc. If rules are true and antecedents are true, then proof is true.

axiom: the difference b/t proof and provenance. axiom does not leave open the possibility of something being true. Not up to discussion if a thing is true or not.

2) conjecture: the hypothesis. Something that we're not 100% sure if it's true. Can be either true or false.

deductive proof: every rule is sound. direct proof or proof by refutation. 99% of systems are designed to use refutation.

2.5) in refutation, need to conjecture something. Then negate the conjecture and add it as a ground fact for your proof. Then build a whole proof based on it and hope that you conclude "false". If you do, then the only way to get to "false" if if one of the ground facts are false. The negated conjecture must then be true.

3) When in a proof, you know that something is a conjecture. The discharged assumption.

When you hit the "false" conclusion, discharge the negated conjecture. It can no longer be assumed to be true.

"add it negated, get to a false, prove that the conjecture is true."


Example:

A) Assume (conjecture / belief): She did kill herself. B) So, introduce that "she not killed herself" and derive a "false" conclusion.

:negated_conjecture__did-not-kill-herself 
   a pml:Information, pml:Conjecture;
   prov:value false;
   dcterms:description "Agatha did not kill herself";
.

:false_from_conjecture 
   a pml:Information, pml:Answer;
   prov:value false;
   prov:wasDerivedFrom :negated_conjecture__did-not-kill-herself;
   pml:answers         :negated_conjecture__did-not-kill-herself;
. 
 
:my_new_inference_step 
    a pml:InferenceStep;
    prov:used  :negated_conjecture__did-not-kill-herself,
               :false_from_conjecture;
    prov:qualifiedAssociation [ 
       a prov:Association; 
       prov:agent   :my_reasoning_engine;
       prov:hadPlan pml:Refutation;
    ];    
    a pml:Refutation; # Jim's "type it when successful" pattern.
    prov:invalidated :negated_conjecture__did-not-kill-herself;
    prov:generated   :did_kill_herself;
.

:did_kill_herself
   a pml:Information;
   prov:value true;
   dcterms:description "Agatha killed herself";
   prov:wasDerivedFrom :negated_conjecture__did-not-kill-herself;
   pml:wasNegatedFrom  :negated_conjecture__did-not-kill-herself;
.

Paulo: pml:Refutation is an instance of pml:Rule.

declarative rules are patterns

the pattern for refutation is the following:

a) the input is "false"

b) it is necessary to have the invalidation clause

c) the generated clause is the negation of the invalidation clause (i.e. "discharge")

note:

n1) theorem provers often stop the dumping of their proofs when they conclude false

n2) it is not always the case that a proof is annotated with a conjecture, i.e., it often just contains the negated conjecture

The application of Refutation requires an instance of Information to be discharged.

1) [A1, didnot_kill_self, A2, A3] => false

2) A1, A2 and A3 are true thus didnot_kill_self needs to be false

3) If didnot_kill_self is false, then kill_self is true

4) [A1,A2,A3] => kill_self

1) [A1, ~kill_self, A2, A3] => false

Facts about IW Meeting 2013-10-03RDF feed
Date3 October 2013  +
Personal tools
Navigation