Regular Derivations in Basic Superposition-Based Calculi

We prove the completeness of the regular strategy of derivations for superposition-based calculi. The regular strategy was pioneered by Kanger in [Kan63], who proposed that all equality inferences take place before all other steps in the proof. We show that the strategy is complete with the elimination of tautologies. The implication of our result is the completeness of non-standard selection functions by which in non-relational clauses only equality literals (and all of them) are selected.

The Open Provenance Model Core Specification (v1.1)

The Open Provenance Model is a model of provenance that is designed to meet the following requirements: (1) To allow provenance information to be exchanged between systems, by means of a compatibility layer based on a shared provenance model. (2) To allow developers to build and share tools that operate on such a provenance model. (3) To define provenance in a precise, technology-agnostic manner. (4) To support a digital representation of provenance for any 'thing', whether produced by computer systems or not. (5) To allow multiple levels of description to coexist. (6) To define a core set of rules that identify the valid inferences that can be made on provenance representation. This document contains the specification of the Open Provenance Model (v1.1) resulting from a community-effort to achieve inter-operability in the Provenance Challenge series.