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.

• FormalSemanticsStrawman for an embryonic version of the formal semantics.
• FormalSemanticsWD3 for a more complete formal semantics synchronized with PROV-DM WD3. (Outdated).
• FormalSemanticsWD5 for a draft formal semantics synchronized with PROV-DM WD5. (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).
• 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 PROV-XML.)
• Some slides for F2F2
• PROV-SEM First Public Working Draft
• PROV-SEM Working Group Note

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).