diff --git a/.gitignore b/.gitignore
index 93bd5279a..852b0cf5b 100644
--- a/.gitignore
+++ b/.gitignore
@@ -34,3 +34,6 @@ flycheck_*.el
 
 # ide settings
 /.vscode
+
+# macOS specific files
+.DS_Store
diff --git a/nemo/src/execution/tracing/resolve_origin.rs b/nemo/src/execution/tracing/resolve_origin.rs
index ad050e8e3..834affc9a 100644
--- a/nemo/src/execution/tracing/resolve_origin.rs
+++ b/nemo/src/execution/tracing/resolve_origin.rs
@@ -40,6 +40,7 @@ pub fn tracing_resolve_origin_id(
         | Origin::Extern
         | Origin::Substitution { .. } => id,
         Origin::Normalization(origin_id)
+        | Origin::Skolemization(origin_id)
         | Origin::Global(origin_id)
         | Origin::Incremental(origin_id)
         | Origin::MergeSparql(origin_id) => tracing_resolve_origin_id(handle, origin_id),
diff --git a/nemo/src/rule_model/components/atom.rs b/nemo/src/rule_model/components/atom.rs
index 5d69e756b..dce8b5d71 100644
--- a/nemo/src/rule_model/components/atom.rs
+++ b/nemo/src/rule_model/components/atom.rs
@@ -94,6 +94,11 @@ impl Atom {
         self.predicate.clone()
     }
 
+    /// Return a reference to the predicate of this atom.
+    pub fn predicate_ref(&self) -> &Tag {
+        &self.predicate
+    }
+
     /// Return an iterator over the terms of this atom.
     pub fn terms(&self) -> impl Iterator<Item = &Term> {
         self.terms.iter()
@@ -116,6 +121,11 @@ impl Atom {
     pub fn remove(&mut self, index: usize) -> Term {
         self.terms.remove(index)
     }
+
+    /// Return an iterator over the universal variables in this atom.
+    pub fn universal_variables(&self) -> impl Iterator<Item = &Variable> {
+        self.variables().filter(|variable| variable.is_universal())
+    }
 }
 
 impl Index<usize> for Atom {
diff --git a/nemo/src/rule_model/components/literal.rs b/nemo/src/rule_model/components/literal.rs
index 04e0699c2..4098ca213 100644
--- a/nemo/src/rule_model/components/literal.rs
+++ b/nemo/src/rule_model/components/literal.rs
@@ -52,6 +52,15 @@ impl Literal {
             Literal::Operation(_) => None,
         }
     }
+
+    /// If this literal is not an operation, return a reference to its predicate.
+    /// Returns `None` otherwise.
+    pub fn predicate_ref(&self) -> Option<&Tag> {
+        match self {
+            Literal::Positive(atom) | Literal::Negative(atom) => Some(atom.predicate_ref()),
+            Literal::Operation(_) => None,
+        }
+    }
 }
 
 impl Display for Literal {
diff --git a/nemo/src/rule_model/components/rule.rs b/nemo/src/rule_model/components/rule.rs
index a23027967..05d01fa47 100644
--- a/nemo/src/rule_model/components/rule.rs
+++ b/nemo/src/rule_model/components/rule.rs
@@ -18,6 +18,7 @@ use super::{
     atom::Atom,
     component_iterator, component_iterator_mut,
     literal::Literal,
+    tag::Tag,
     term::{
         Term,
         primitive::{Primitive, variable::Variable},
@@ -164,6 +165,20 @@ impl Rule {
         &mut self.head
     }
 
+    /// Return an iterator over all existential variables in this rule.
+    pub fn existential_variables(&self) -> impl Iterator<Item = &Variable> {
+        self.variables()
+            .filter(|variable| variable.is_existential())
+    }
+
+    /// Return an iterator over the variables bound in positive body atoms.
+    pub fn positive_variables(&self) -> impl Iterator<Item = &Variable> {
+        self.body_positive().flat_map(|atom| {
+            atom.universal_variables()
+                .filter(|var| var.name().is_some())
+        })
+    }
+
     /// Return an iterator over all positive and negative [Atom]s
     /// contained in the body of this rule.
     pub fn body_atoms(&self) -> impl Iterator<Item = &Atom> {
@@ -179,6 +194,14 @@ impl Rule {
         self.head.iter().chain(self.body_atoms())
     }
 
+    /// Return references to the predicates of all atoms in this rule.
+    pub fn predicates_ref(&self) -> impl Iterator<Item = &Tag> {
+        self.body
+            .iter()
+            .filter_map(Literal::predicate_ref)
+            .chain(self.head.iter().map(Atom::predicate_ref))
+    }
+
     /// Return an iterator over all [ImportLiteral]s
     /// that are evaluated as part of this rule.
     pub fn imports(&self) -> impl Iterator<Item = &ImportLiteral> {
@@ -196,32 +219,21 @@ impl Rule {
         self.imports.push(import);
     }
 
-    /// Return the set of variables that are bound in positive body atoms.
-    pub fn positive_variables(&self) -> HashSet<&Variable> {
-        let mut result = HashSet::new();
-
-        for literal in &self.body {
-            if let Literal::Positive(atom) = literal {
-                for term in atom.terms() {
-                    if let Term::Primitive(Primitive::Variable(variable)) = term
-                        && variable.is_universal()
-                        && variable.name().is_some()
-                    {
-                        result.insert(variable);
-                    }
-                }
-            }
-        }
+    /// Return an iterator over the frontier variables of this rule.
+    pub fn frontier_variables(&self) -> impl Iterator<Item = &Variable> {
+        let positive_variables = self.positive_variables().collect::<HashSet<_>>();
+        self.universal_head_variables()
+            .filter(move |variable| positive_variables.contains(variable))
+    }
 
-        result
+    /// Return an iterator over all universal variables in the head of this rule.
+    fn universal_head_variables(&self) -> impl Iterator<Item = &Variable> {
+        self.head.iter().flat_map(|atom| atom.universal_variables())
     }
 
-    /// Return the set of variables that are bound by import statements
-    pub fn import_variables(&self) -> HashSet<&Variable> {
-        self.imports
-            .iter()
-            .flat_map(|import| import.variables())
-            .collect::<HashSet<_>>()
+    /// Return an iterator over the variables bound by import statements.
+    pub fn import_variables(&self) -> impl Iterator<Item = &Variable> {
+        self.imports.iter().flat_map(|import| import.variables())
     }
 
     /// Return a set of "safe" variables.
@@ -233,8 +245,7 @@ impl Rule {
     pub fn safe_variables(&self) -> HashSet<&Variable> {
         let mut result = self
             .positive_variables()
-            .union(&self.import_variables())
-            .cloned()
+            .chain(self.import_variables())
             .collect::<HashSet<_>>();
 
         loop {
diff --git a/nemo/src/rule_model/components/tag.rs b/nemo/src/rule_model/components/tag.rs
index 1903b5ebb..e2d28c3a8 100644
--- a/nemo/src/rule_model/components/tag.rs
+++ b/nemo/src/rule_model/components/tag.rs
@@ -62,9 +62,15 @@ impl PartialEq for Tag {
 
 impl Eq for Tag {}
 
+impl Ord for Tag {
+    fn cmp(&self, other: &Self) -> std::cmp::Ordering {
+        self.tag.cmp(&other.tag)
+    }
+}
+
 impl PartialOrd for Tag {
     fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering> {
-        self.tag.partial_cmp(&other.tag)
+        Some(self.cmp(other))
     }
 }
 
diff --git a/nemo/src/rule_model/components/term/function.rs b/nemo/src/rule_model/components/term/function.rs
index 4639cb645..562336572 100644
--- a/nemo/src/rule_model/components/term/function.rs
+++ b/nemo/src/rule_model/components/term/function.rs
@@ -73,7 +73,7 @@ impl FunctionTerm {
     }
 
     /// Create a new [FunctionTerm] with a [Tag].
-    pub(crate) fn new_tagged<Terms: IntoIterator<Item = Term>>(tag: Tag, subterms: Terms) -> Self {
+    pub fn new_tagged<Terms: IntoIterator<Item = Term>>(tag: Tag, subterms: Terms) -> Self {
         Self {
             origin: Origin::default(),
             id: ProgramComponentId::default(),
diff --git a/nemo/src/rule_model/components/term/primitive/variable.rs b/nemo/src/rule_model/components/term/primitive/variable.rs
index 46cce2d30..53ca43363 100644
--- a/nemo/src/rule_model/components/term/primitive/variable.rs
+++ b/nemo/src/rule_model/components/term/primitive/variable.rs
@@ -26,7 +26,7 @@ pub mod universal;
 ///
 /// A general placeholder that can be bound to any value.
 /// We distinguish [UniversalVariable] and [ExistentialVariable].
-#[derive(Debug, Clone, PartialEq, Eq, Hash, PartialOrd)]
+#[derive(Debug, Clone, PartialEq, Eq, Hash, Ord, PartialOrd)]
 pub enum Variable {
     /// Universal variable
     Universal(UniversalVariable),
diff --git a/nemo/src/rule_model/components/term/primitive/variable/existential.rs b/nemo/src/rule_model/components/term/primitive/variable/existential.rs
index 44c2ddb0f..cdf2187b8 100644
--- a/nemo/src/rule_model/components/term/primitive/variable/existential.rs
+++ b/nemo/src/rule_model/components/term/primitive/variable/existential.rs
@@ -76,9 +76,15 @@ impl PartialEq for ExistentialVariable {
 
 impl Eq for ExistentialVariable {}
 
+impl Ord for ExistentialVariable {
+    fn cmp(&self, other: &Self) -> std::cmp::Ordering {
+        self.name.cmp(&other.name)
+    }
+}
+
 impl PartialOrd for ExistentialVariable {
     fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering> {
-        self.name.partial_cmp(&other.name)
+        Some(self.cmp(other))
     }
 }
 
diff --git a/nemo/src/rule_model/components/term/primitive/variable/global.rs b/nemo/src/rule_model/components/term/primitive/variable/global.rs
index 8e6ca8f13..34a9844a6 100644
--- a/nemo/src/rule_model/components/term/primitive/variable/global.rs
+++ b/nemo/src/rule_model/components/term/primitive/variable/global.rs
@@ -70,9 +70,15 @@ impl PartialEq for GlobalVariable {
 
 impl Eq for GlobalVariable {}
 
+impl Ord for GlobalVariable {
+    fn cmp(&self, other: &Self) -> std::cmp::Ordering {
+        self.name.cmp(&other.name)
+    }
+}
+
 impl PartialOrd for GlobalVariable {
     fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering> {
-        self.name.partial_cmp(&other.name)
+        Some(self.cmp(other))
     }
 }
 
diff --git a/nemo/src/rule_model/components/term/primitive/variable/universal.rs b/nemo/src/rule_model/components/term/primitive/variable/universal.rs
index 8b9893595..4707f8f73 100644
--- a/nemo/src/rule_model/components/term/primitive/variable/universal.rs
+++ b/nemo/src/rule_model/components/term/primitive/variable/universal.rs
@@ -100,9 +100,15 @@ impl PartialEq for UniversalVariable {
 
 impl Eq for UniversalVariable {}
 
+impl Ord for UniversalVariable {
+    fn cmp(&self, other: &Self) -> std::cmp::Ordering {
+        self.name.cmp(&other.name)
+    }
+}
+
 impl PartialOrd for UniversalVariable {
     fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering> {
-        self.name.partial_cmp(&other.name)
+        Some(self.cmp(other))
     }
 }
 
diff --git a/nemo/src/rule_model/error.rs b/nemo/src/rule_model/error.rs
index 25a56c278..e3a03d7a5 100644
--- a/nemo/src/rule_model/error.rs
+++ b/nemo/src/rule_model/error.rs
@@ -407,6 +407,7 @@ impl ValidationReport {
                 None
             }
             Origin::Normalization(id)
+            | Origin::Skolemization(id)
             | Origin::Global(id)
             | Origin::Incremental(id)
             | Origin::MergeSparql(id) => Self::id_to_range(program, *id, error),
diff --git a/nemo/src/rule_model/origin.rs b/nemo/src/rule_model/origin.rs
index 4e07466ac..eeb55018a 100644
--- a/nemo/src/rule_model/origin.rs
+++ b/nemo/src/rule_model/origin.rs
@@ -40,6 +40,9 @@ pub enum Origin {
     /// Rule that was created by normalizing a rule
     Normalization(ProgramComponentId),
 
+    /// Rule that was created by skolemizing a rule
+    Skolemization(ProgramComponentId),
+
     /// Statement that was created by substituting global variables in a rule
     Global(ProgramComponentId),
 
diff --git a/nemo/src/rule_model/pipeline/transformations/skolem.rs b/nemo/src/rule_model/pipeline/transformations/skolem.rs
index 5205b1a24..5dda7a4f5 100644
--- a/nemo/src/rule_model/pipeline/transformations/skolem.rs
+++ b/nemo/src/rule_model/pipeline/transformations/skolem.rs
@@ -4,7 +4,7 @@ use std::collections::{HashMap, HashSet};
 
 use crate::rule_model::{
     components::{
-        IterableVariables,
+        ComponentIdentity, ComponentSource, IterableVariables,
         literal::Literal,
         statement::Statement,
         term::{
@@ -14,6 +14,7 @@ use crate::rule_model::{
         },
     },
     error::ValidationReport,
+    origin::Origin,
     programs::{ProgramRead, ProgramWrite, handle::ProgramHandle},
 };
 
@@ -62,6 +63,7 @@ impl ProgramTransformation for TransformationSkolemize {
                     .collect::<Vec<_>>();
 
                 let mut new_rule = rule.clone();
+                new_rule.set_origin(Origin::Skolemization(rule.id()));
                 let mut sk_terms_by_ex_var = HashMap::new();
                 for head_atom in new_rule.head_mut() {
                     for term in head_atom.terms_mut() {