FormalSemantics

From Provenance WG Wiki
Revision as of 12:06, 21 November 2012 by Jcheney (Talk | contribs)

Jump to: navigation, search

Introduction

This page is a placeholder for discussion of the formal semantics deliverable.

Please feel free to add suggestions or critiques. Please sign contributions. -James


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

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