FormalSemantics

From Provenance WG Wiki
Revision as of 16:03, 20 April 2013 by Jcheney (Talk | contribs)

(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to: navigation, search

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