# FormalSemantics

## Contents

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

- 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. (In progress.)
- 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

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