Difference between revisions of "FormalSemantics"

From Provenance WG Wiki
Jump to: navigation, search
 
Line 1: Line 1:
 
= Introduction =  
 
= Introduction =  
  
This page is a placeholder for discussion of the formal semantics deliverable.
+
This page is records discussion of the PROV formal semantics deliverable.
  
Please feel free to add suggestions or critiques.  Please sign contributions. -James
 
  
 +
The [http://www.w3.org/TR/prov-constraints/ PROV-CONSTRAINTS] document contains formal content specifying a notion of validity (approximately, logical consistency) for PROV documents.  The formal semantics, PROV-SEM, is planned for release as a W3C Note that will complement the procedural specification in PROV-CONSTRAINTS with a declarative specification formulated in terms of first-order logic.  The formal semantics was published as a Working Group Note at the conclusion of the Provenance Interchange Working Group.  Some of the drafts below are intermediate stages and some of them are out of date. 
  
The [http://www.w3.org/TR/prov-constraints/ PROV-CONSTRAINTS] document contains formal content specifying a notion of validity (approximately, logical consistency) for PROV documents.  The formal semantics, PROV-SEM, is planned for release as a W3C Note that will complement the procedural specification in PROV-CONSTRAINTS with a declarative specification formulated in terms of first-order logic.  The formal semantics is '''work in progress'''.  The drafts below are intermediate stages and some of them are out of date. 
 
 
The current version (editor's draft) of the formal semantics can always be found at: [[FormalSemanticsED]]. 
 
  
 
* [[FormalSemanticsStrawman]] for an embryonic version of the formal semantics.
 
* [[FormalSemanticsStrawman]] for an embryonic version of the formal semantics.
Line 15: Line 12:
 
* [[FormalSemanticsLC]] for a draft formal semantics synchronized with PROV-DM Last Call Working Draft. (Outdated).
 
* [[FormalSemanticsLC]] for a draft formal semantics synchronized with PROV-DM Last Call Working Draft. (Outdated).
 
* [[FormalSemanticsCR]] for a draft formal semantics synchronized with PROV-DM Candidate Recommendation. (Outdated).
 
* [[FormalSemanticsCR]] for a draft formal semantics synchronized with PROV-DM Candidate Recommendation. (Outdated).
* [https://dvcs.w3.org/hg/prov/raw-file/default/semantics/prov-sem-review-20130226.html PROV-SEM] for a draft formal semantics synchronized with PROV-DM Candidate Recommendation. (In progress.)
 
 
* [[ProvRDF]] for a draft translation from PROV-DM to PROV-O.
 
* [[ProvRDF]] for a draft translation from PROV-DM to PROV-O.
 
* [[ProvXML]] for a draft translation from PROV-DM to PROV-XML.  (See also by [http://dvcs.w3.org/hg/prov/raw-file/default/xml/prov-xml.html PROV-XML].)
 
* [[ProvXML]] for a draft translation from PROV-DM to PROV-XML.  (See also by [http://dvcs.w3.org/hg/prov/raw-file/default/xml/prov-xml.html PROV-XML].)
 
* [http://www.w3.org/2011/prov/wiki/File:prov-sem.pdf Some slides for F2F2]
 
* [http://www.w3.org/2011/prov/wiki/File:prov-sem.pdf Some slides for F2F2]
 +
* [http://www.w3.org/TR/2013/WD-prov-sem-20130312/ PROV-SEM First Public Working Draft]
 +
* [http://www.w3.org/TR/prov-sem/ PROV-SEM Working Group Note]
  
 
= Possible Goals =
 
= Possible Goals =

Latest revision as of 16:03, 20 April 2013

Introduction

This page is records discussion of the PROV formal semantics deliverable.


The PROV-CONSTRAINTS document contains formal content specifying a notion of validity (approximately, logical consistency) for PROV documents. The formal semantics, PROV-SEM, is planned for release as a W3C Note that will complement the procedural specification in PROV-CONSTRAINTS with a declarative specification formulated in terms of first-order logic. The formal semantics was published as a Working Group Note at the conclusion of the Provenance Interchange Working Group. Some of the drafts below are intermediate stages and some of them are out of date.


Possible Goals

  • Explicate constraints (including possibly constraints not expressible in OWL)?
  • Resolve contentious issues:
    • transitivity of derivation?
    • granularity of processes?
  • Soundness and completeness of inferences over assertions?
  • "Semantic interoperability": Guidelines for mapping system behavior to provenance?
  • Others?

Possible Forms

  • OWL ontology + constraints?
  • Mathematical language (perhaps just restating OWL)?
  • Something else?


Possible objections

  • Redundant given semantics of OWL/RDF(S)?
  • Too much duplication?
  • Premature/over-formalization a barrier to adoption?


Constraints from the current Model document

These are copied somewhat haphazardly and without context.

  • "From the assertion of a process execution, one can infer that the start precedes the end of the represented activity. "
  • "Given an assertion isGeneratedBy(x,pe,r) or isGeneratedBy(x,pe,r,t), the activity denoted by pe and the entities used by pe dermine values of some of x's attributes."
  • "Given an assertion isGeneratedBy(x,pe,r) or isGeneratedBy(x,pe,r,t), one can infer that the generation of the entity denoted by x precedes the end of pe and follows the beginning of pe. "
  • "Use represents the consumption of a characterized entity by an activity."
  • "Given an assertion uses(pe,x,r) or uses(pe,x,r,t), at least one value of x's attributes is a pre-condition for the activity denoted by pe to terminate."
  • "Given an assertion uses(pe,x,r) or uses(pe,x,r,t), one can infer that the use of the entity denoted by x precedes the end of pe and follows the beginning of pe. Furthermore, we can infer that the generation of the entity x always precedes its use. * "From an assertion isDerivedFrom(B,A), the values of some attributes of B are at least partially determined by the values of some attributes of A."
  • "Given an assertion isDerivedFrom(B,A), one can infer that the use of characterized entity denoted by A precedes the generation of the characterized entity denoted by B. "
  • "if isDerivedFrom(e1,e0) holds, then there exists a process execution pe, and roles r0,r1, such that: isGeneratedBy(e1,pe,r1) and uses(pe,e0,r0)."
  • "The relationship isDerivedFrom is transitive. "
  • "The relationship isDerivedFrom+ is the transitive closure of isDerivedFrom."
  • Various things involving IVP-of


Questions

  • How do we define "created", "determined", "pre-condition", "consumption"
  • Is derivation the same as creation
  • Is there a difference between single execution derivation step and multiple execution derivation step
  • Is process execution a (characterized) entity - i.e. if it walks, talks, quacks like a duck then is it a duck?
  • Is IVP-of a primitive or derived notion (i.e. is it an atomic assertion or is it something we can define in terms of other atomic assertions).