diff --git a/src/Makefile.am b/src/Makefile.am
index 3e8a9b1150e..25b39020d5a 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -203,6 +203,8 @@ souffle_sources = \
         ast2ram/Location.h                                 \
         ast2ram/ProvenanceClauseTranslator.cpp             \
         ast2ram/ProvenanceClauseTranslator.h               \
+        ast2ram/ProvenanceTranslator.cpp                   \
+        ast2ram/ProvenanceTranslator.h                     \
         ast2ram/ValueIndex.cpp                             \
         ast2ram/ValueIndex.h                               \
         ast2ram/ValueTranslator.cpp                        \
diff --git a/src/ast2ram/AstToRamTranslator.cpp b/src/ast2ram/AstToRamTranslator.cpp
index 3da4f5fa595..55a1e8f684c 100644
--- a/src/ast2ram/AstToRamTranslator.cpp
+++ b/src/ast2ram/AstToRamTranslator.cpp
@@ -130,7 +130,7 @@ AstToRamTranslator::AstToRamTranslator() = default;
 AstToRamTranslator::~AstToRamTranslator() = default;
 
 /** append statement to a list of statements */
-inline void appendStmt(VecOwn<ram::Statement>& stmtList, Own<ram::Statement> stmt) {
+void AstToRamTranslator::appendStmt(VecOwn<ram::Statement>& stmtList, Own<ram::Statement> stmt) {
     if (stmt) {
         stmtList.push_back(std::move(stmt));
     }
@@ -383,9 +383,6 @@ VecOwn<ram::Statement> AstToRamTranslator::translateSCC(size_t scc, size_t idx)
     const auto& internIns = sccGraph->getInternalInputRelations(scc);
     const auto& internOuts = sccGraph->getInternalOutputRelations(scc);
 
-    // make a variable for all relations that are expired at the current SCC
-    const auto& internExps = relationSchedule->schedule().at(idx).expired();
-
     // load all internal input relations from the facts dir with a .facts extension
     for (const auto& relation : internIns) {
         makeRamLoad(current, relation);
@@ -402,8 +399,8 @@ VecOwn<ram::Statement> AstToRamTranslator::translateSCC(size_t scc, size_t idx)
         makeRamStore(current, relation);
     }
 
-    // if provenance is disabled, drop all relations expired as per the topological order
     if (!Global::config().has("provenance")) {
+        const auto& internExps = relationSchedule->schedule().at(idx).expired();
         for (const auto& relation : internExps) {
             makeRamClear(current, relation);
         }
@@ -413,9 +410,7 @@ VecOwn<ram::Statement> AstToRamTranslator::translateSCC(size_t scc, size_t idx)
 }
 
 void AstToRamTranslator::addNegation(ast::Clause& clause, const ast::Atom* atom) {
-    if (Global::config().has("provenance")) {
-        clause.addToBody(mk<ast::ProvenanceNegation>(souffle::clone(atom)));
-    } else if (clause.getHead()->getArity() > 0) {
+    if (clause.getHead()->getArity() > 0) {
         clause.addToBody(mk<ast::Negation>(souffle::clone(atom)));
     }
 }
@@ -625,262 +620,6 @@ Own<ram::Statement> AstToRamTranslator::translateRecursiveRelation(
     return mk<ram::Sequence>(std::move(res));
 }
 
-/** make a subroutine to search for subproofs */
-Own<ram::Statement> AstToRamTranslator::makeSubproofSubroutine(const ast::Clause& clause) {
-    auto intermediateClause = mk<ast::Clause>(souffle::clone(clause.getHead()));
-
-    // create a clone where all the constraints are moved to the end
-    for (auto bodyLit : clause.getBodyLiterals()) {
-        // first add all the things that are not constraints
-        if (!isA<ast::Constraint>(bodyLit)) {
-            intermediateClause->addToBody(souffle::clone(bodyLit));
-        }
-    }
-
-    // now add all constraints
-    for (auto bodyLit : ast::getBodyLiterals<ast::Constraint>(clause)) {
-        intermediateClause->addToBody(souffle::clone(bodyLit));
-    }
-
-    // name unnamed variables
-    nameUnnamedVariables(intermediateClause.get());
-
-    // add constraint for each argument in head of atom
-    ast::Atom* head = intermediateClause->getHead();
-    size_t auxiliaryArity = auxArityAnalysis->getArity(head);
-    auto args = head->getArguments();
-    for (size_t i = 0; i < head->getArity() - auxiliaryArity; i++) {
-        auto arg = args[i];
-
-        if (auto var = dynamic_cast<ast::Variable*>(arg)) {
-            // FIXME: float equiv (`FEQ`)
-            auto constraint = mk<ast::BinaryConstraint>(
-                    BinaryConstraintOp::EQ, souffle::clone(var), mk<ast::SubroutineArgument>(i));
-            constraint->setFinalType(BinaryConstraintOp::EQ);
-            intermediateClause->addToBody(std::move(constraint));
-        } else if (auto func = dynamic_cast<ast::Functor*>(arg)) {
-            TypeAttribute returnType;
-            if (auto* inf = dynamic_cast<ast::IntrinsicFunctor*>(func)) {
-                assert(inf->getFinalReturnType().has_value() && "functor has missing return type");
-                returnType = inf->getFinalReturnType().value();
-            } else if (auto* udf = dynamic_cast<ast::UserDefinedFunctor*>(func)) {
-                assert(udf->getFinalReturnType().has_value() && "functor has missing return type");
-                returnType = udf->getFinalReturnType().value();
-            } else {
-                assert(false && "unexpected functor type");
-            }
-            auto opEq = returnType == TypeAttribute::Float ? BinaryConstraintOp::FEQ : BinaryConstraintOp::EQ;
-            auto constraint =
-                    mk<ast::BinaryConstraint>(opEq, souffle::clone(func), mk<ast::SubroutineArgument>(i));
-            constraint->setFinalType(opEq);
-            intermediateClause->addToBody(std::move(constraint));
-        } else if (auto rec = dynamic_cast<ast::RecordInit*>(arg)) {
-            auto constraint = mk<ast::BinaryConstraint>(
-                    BinaryConstraintOp::EQ, souffle::clone(rec), mk<ast::SubroutineArgument>(i));
-            constraint->setFinalType(BinaryConstraintOp::EQ);
-            intermediateClause->addToBody(std::move(constraint));
-        }
-    }
-
-    // index of level argument in argument list
-    size_t levelIndex = head->getArguments().size() - auxiliaryArity;
-
-    // add level constraints, i.e., that each body literal has height less than that of the head atom
-    const auto& bodyLiterals = intermediateClause->getBodyLiterals();
-    for (auto lit : bodyLiterals) {
-        if (auto atom = dynamic_cast<ast::Atom*>(lit)) {
-            auto arity = atom->getArity();
-            auto atomArgs = atom->getArguments();
-            // arity - 1 is the level number in body atoms
-            auto constraint = mk<ast::BinaryConstraint>(BinaryConstraintOp::LT,
-                    souffle::clone(atomArgs[arity - 1]), mk<ast::SubroutineArgument>(levelIndex));
-            constraint->setFinalType(BinaryConstraintOp::LT);
-            intermediateClause->addToBody(std::move(constraint));
-        }
-    }
-    return ProvenanceClauseTranslator(*this).translateClause(*intermediateClause, clause);
-}
-
-/** make a subroutine to search for subproofs for the non-existence of a tuple */
-Own<ram::Statement> AstToRamTranslator::makeNegationSubproofSubroutine(const ast::Clause& clause) {
-    // TODO (taipan-snake): Currently we only deal with atoms (no constraints or negations or aggregates
-    // or anything else...)
-    //
-    // The resulting subroutine looks something like this:
-    // IF (arg(0), arg(1), _, _) IN rel_1:
-    //   return 1
-    // IF (arg(0), arg(1), _ ,_) NOT IN rel_1:
-    //   return 0
-    // ...
-
-    // clone clause for mutation, rearranging constraints to be at the end
-    auto clauseReplacedAggregates = mk<ast::Clause>(souffle::clone(clause.getHead()));
-
-    // create a clone where all the constraints are moved to the end
-    for (auto bodyLit : clause.getBodyLiterals()) {
-        // first add all the things that are not constraints
-        if (!isA<ast::Constraint>(bodyLit)) {
-            clauseReplacedAggregates->addToBody(souffle::clone(bodyLit));
-        }
-    }
-
-    // now add all constraints
-    for (auto bodyLit : ast::getBodyLiterals<ast::Constraint>(clause)) {
-        clauseReplacedAggregates->addToBody(souffle::clone(bodyLit));
-    }
-
-    struct AggregatesToVariables : public ast::NodeMapper {
-        mutable int aggNumber{0};
-
-        AggregatesToVariables() = default;
-
-        Own<ast::Node> operator()(Own<ast::Node> node) const override {
-            if (dynamic_cast<ast::Aggregator*>(node.get()) != nullptr) {
-                return mk<ast::Variable>("agg_" + std::to_string(aggNumber++));
-            }
-
-            node->apply(*this);
-            return node;
-        }
-    };
-
-    AggregatesToVariables aggToVar;
-    clauseReplacedAggregates->apply(aggToVar);
-
-    // build a vector of unique variables
-    std::vector<const ast::Variable*> uniqueVariables;
-
-    visitDepthFirst(*clauseReplacedAggregates, [&](const ast::Variable& var) {
-        if (var.getName().find("@level_num") == std::string::npos) {
-            // use find_if since uniqueVariables stores pointers, and we need to dereference the pointer to
-            // check equality
-            if (std::find_if(uniqueVariables.begin(), uniqueVariables.end(),
-                        [&](const ast::Variable* v) { return *v == var; }) == uniqueVariables.end()) {
-                uniqueVariables.push_back(&var);
-            }
-        }
-    });
-
-    // a mapper to replace variables with subroutine arguments
-    struct VariablesToArguments : public ast::NodeMapper {
-        const std::vector<const ast::Variable*>& uniqueVariables;
-
-        VariablesToArguments(const std::vector<const ast::Variable*>& uniqueVariables)
-                : uniqueVariables(uniqueVariables) {}
-
-        Own<ast::Node> operator()(Own<ast::Node> node) const override {
-            // replace unknown variables
-            if (auto varPtr = dynamic_cast<const ast::Variable*>(node.get())) {
-                if (varPtr->getName().find("@level_num") == std::string::npos) {
-                    size_t argNum = std::find_if(uniqueVariables.begin(), uniqueVariables.end(),
-                                            [&](const ast::Variable* v) { return *v == *varPtr; }) -
-                                    uniqueVariables.begin();
-
-                    return mk<ast::SubroutineArgument>(argNum);
-                } else {
-                    return mk<ast::UnnamedVariable>();
-                }
-            }
-
-            // apply recursive
-            node->apply(*this);
-
-            // otherwise nothing
-            return node;
-        }
-    };
-
-    auto makeRamAtomExistenceCheck = [&](ast::Atom* atom) {
-        auto relName = getConcreteRelationName(atom);
-        size_t auxiliaryArity = auxArityAnalysis->getArity(atom);
-
-        // translate variables to subroutine arguments
-        VariablesToArguments varsToArgs(uniqueVariables);
-        atom->apply(varsToArgs);
-
-        // construct a query
-        VecOwn<ram::Expression> query;
-        auto atomArgs = atom->getArguments();
-
-        // add each value (subroutine argument) to the search query
-        for (size_t i = 0; i < atom->getArity() - auxiliaryArity; i++) {
-            auto arg = atomArgs[i];
-            query.push_back(translateValue(arg, ValueIndex()));
-        }
-
-        // fill up query with nullptrs for the provenance columns
-        for (size_t i = 0; i < auxiliaryArity; i++) {
-            query.push_back(mk<ram::UndefValue>());
-        }
-
-        // ensure the length of query tuple is correct
-        assert(query.size() == atom->getArity() && "wrong query tuple size");
-
-        // create existence checks to check if the tuple exists or not
-        return mk<ram::ExistenceCheck>(relName, std::move(query));
-    };
-
-    auto makeRamReturnTrue = [&]() {
-        VecOwn<ram::Expression> returnTrue;
-        returnTrue.push_back(mk<ram::SignedConstant>(1));
-        return mk<ram::SubroutineReturn>(std::move(returnTrue));
-    };
-
-    auto makeRamReturnFalse = [&]() {
-        VecOwn<ram::Expression> returnFalse;
-        returnFalse.push_back(mk<ram::SignedConstant>(0));
-        return mk<ram::SubroutineReturn>(std::move(returnFalse));
-    };
-
-    // the structure of this subroutine is a sequence where each nested statement is a search in each
-    // relation
-    VecOwn<ram::Statement> searchSequence;
-
-    // make a copy so that when we mutate clause, pointers to objects in newClause are not affected
-    auto newClause = souffle::clone(clauseReplacedAggregates);
-
-    // go through each body atom and create a return
-    size_t litNumber = 0;
-    for (const auto& lit : newClause->getBodyLiterals()) {
-        if (auto atom = dynamic_cast<ast::Atom*>(lit)) {
-            auto existenceCheck = makeRamAtomExistenceCheck(atom);
-            auto negativeExistenceCheck = mk<ram::Negation>(souffle::clone(existenceCheck));
-
-            // create a ram::Query to return true/false
-            appendStmt(searchSequence,
-                    mk<ram::Query>(mk<ram::Filter>(std::move(existenceCheck), makeRamReturnTrue())));
-            appendStmt(searchSequence,
-                    mk<ram::Query>(mk<ram::Filter>(std::move(negativeExistenceCheck), makeRamReturnFalse())));
-        } else if (auto neg = dynamic_cast<ast::Negation*>(lit)) {
-            auto atom = neg->getAtom();
-            auto existenceCheck = makeRamAtomExistenceCheck(atom);
-            auto negativeExistenceCheck = mk<ram::Negation>(souffle::clone(existenceCheck));
-
-            // create a ram::Query to return true/false
-            appendStmt(searchSequence,
-                    mk<ram::Query>(mk<ram::Filter>(std::move(existenceCheck), makeRamReturnFalse())));
-            appendStmt(searchSequence,
-                    mk<ram::Query>(mk<ram::Filter>(std::move(negativeExistenceCheck), makeRamReturnTrue())));
-        } else if (auto con = dynamic_cast<ast::Constraint*>(lit)) {
-            VariablesToArguments varsToArgs(uniqueVariables);
-            con->apply(varsToArgs);
-
-            // translate to a ram::Condition
-            auto condition = translateConstraint(con, ValueIndex());
-            auto negativeCondition = mk<ram::Negation>(souffle::clone(condition));
-
-            appendStmt(searchSequence,
-                    mk<ram::Query>(mk<ram::Filter>(std::move(condition), makeRamReturnTrue())));
-            appendStmt(searchSequence,
-                    mk<ram::Query>(mk<ram::Filter>(std::move(negativeCondition), makeRamReturnFalse())));
-        }
-
-        litNumber++;
-    }
-
-    return mk<ram::Sequence>(std::move(searchSequence));
-}
-
 bool AstToRamTranslator::removeADTs(const ast::TranslationUnit& translationUnit) {
     struct ADTsFuneral : public ast::NodeMapper {
         mutable bool changed{false};
@@ -1016,26 +755,6 @@ void AstToRamTranslator::createRamRelation(size_t scc) {
     }
 }
 
-void AstToRamTranslator::addProvenanceClauseSubroutines(const ast::Program* program) {
-    visitDepthFirst(*program, [&](const ast::Clause& clause) {
-        std::stringstream relName;
-        relName << clause.getHead()->getQualifiedName();
-
-        // do not add subroutines for info relations or facts
-        if (relName.str().find("@info") != std::string::npos || clause.getBodyLiterals().empty()) {
-            return;
-        }
-
-        std::string subroutineLabel =
-                relName.str() + "_" + std::to_string(getClauseNum(program, &clause)) + "_subproof";
-        ramSubs[subroutineLabel] = makeSubproofSubroutine(clause);
-
-        std::string negationSubroutineLabel =
-                relName.str() + "_" + std::to_string(getClauseNum(program, &clause)) + "_negation_subproof";
-        ramSubs[negationSubroutineLabel] = makeNegationSubproofSubroutine(clause);
-    });
-}
-
 /** translates the given datalog program into an equivalent RAM program  */
 void AstToRamTranslator::translateProgram(const ast::TranslationUnit& translationUnit) {
     // keep track of relevant analyses
@@ -1111,11 +830,6 @@ void AstToRamTranslator::translateProgram(const ast::TranslationUnit& translatio
 
     // done for main prog
     ramMain = mk<ram::Sequence>(std::move(res));
-
-    // add subroutines for each clause
-    if (Global::config().has("provenance")) {
-        addProvenanceClauseSubroutines(program);
-    }
 }
 
 Own<ram::TranslationUnit> AstToRamTranslator::translateUnit(ast::TranslationUnit& tu) {
diff --git a/src/ast2ram/AstToRamTranslator.h b/src/ast2ram/AstToRamTranslator.h
index 9ce7841cdd9..7a71e642409 100644
--- a/src/ast2ram/AstToRamTranslator.h
+++ b/src/ast2ram/AstToRamTranslator.h
@@ -120,10 +120,35 @@ class AstToRamTranslator {
         return (*it).second.get();
     }
 
-private:
+protected:
     /** AST program */
     const ast::Program* program = nullptr;
 
+    /** RAM program */
+    Own<ram::Statement> ramMain;
+
+    /** Subroutines */
+    std::map<std::string, Own<ram::Statement>> ramSubs;
+
+    /** RAM relations */
+    std::map<std::string, Own<ram::Relation>> ramRels;
+
+    const ast::analysis::AuxiliaryArityAnalysis* auxArityAnalysis = nullptr;
+
+    /**
+     * assigns names to unnamed variables such that enclosing
+     * constructs may be cloned without losing the variable-identity
+     */
+    virtual void addNegation(ast::Clause& clause, const ast::Atom* atom);
+
+    void nameUnnamedVariables(ast::Clause* clause);
+
+    void appendStmt(VecOwn<ram::Statement>& stmtList, Own<ram::Statement> stmt);
+
+    /** translate AST to RAM Program */
+    virtual void translateProgram(const ast::TranslationUnit& translationUnit);
+
+private:
     /** Type environment */
     const ast::analysis::TypeEnvironment* typeEnv = nullptr;
 
@@ -133,34 +158,15 @@ class AstToRamTranslator {
     const ast::analysis::RelationScheduleAnalysis* relationSchedule = nullptr;
     const ast::analysis::SCCGraphAnalysis* sccGraph = nullptr;
     const ast::analysis::RecursiveClausesAnalysis* recursiveClauses = nullptr;
-    const ast::analysis::AuxiliaryArityAnalysis* auxArityAnalysis = nullptr;
     const ast::analysis::RelationDetailCacheAnalysis* relDetail = nullptr;
     const ast::analysis::PolymorphicObjectsAnalysis* polyAnalysis = nullptr;
 
     /** SIPS metric for reordering */
     Own<ast::SipsMetric> sips;
 
-    /** RAM program */
-    Own<ram::Statement> ramMain;
-
-    /** Subroutines */
-    std::map<std::string, Own<ram::Statement>> ramSubs;
-
-    /** RAM relations */
-    std::map<std::string, Own<ram::Relation>> ramRels;
-
-    /** translate AST to RAM Program */
-    void translateProgram(const ast::TranslationUnit& translationUnit);
-
     /** replace ADTs with special records */
     static bool removeADTs(const ast::TranslationUnit& translationUnit);
 
-    /**
-     * assigns names to unnamed variables such that enclosing
-     * constructs may be cloned without losing the variable-identity
-     */
-    void nameUnnamedVariables(ast::Clause* clause);
-
     /** converts the given relation identifier into a relation name */
     static std::string getRelationName(const ast::QualifiedName& id);
 
@@ -194,14 +200,6 @@ class AstToRamTranslator {
     /** translate RAM code for recursive relations in a strongly-connected component */
     Own<ram::Statement> translateRecursiveRelation(const std::set<const ast::Relation*>& scc);
 
-    /** translate RAM code for subroutine to get subproofs */
-    Own<ram::Statement> makeSubproofSubroutine(const ast::Clause& clause);
-
-    /** translate RAM code for subroutine to get subproofs for non-existence of a tuple */
-    Own<ram::Statement> makeNegationSubproofSubroutine(const ast::Clause& clause);
-
-    static void addNegation(ast::Clause& clause, const ast::Atom* atom);
-
     /** add a statement to store a relation */
     void makeRamClear(VecOwn<ram::Statement>& curStmts, const ast::Relation* relation);
 
@@ -210,9 +208,6 @@ class AstToRamTranslator {
 
     /** add a statement to load a relation */
     void makeRamLoad(VecOwn<ram::Statement>& curStmts, const ast::Relation* relation);
-
-    /** add provenance clause subroutines */
-    void addProvenanceClauseSubroutines(const ast::Program* program);
 };
 
 }  // namespace souffle::ast2ram
diff --git a/src/ast2ram/ProvenanceTranslator.cpp b/src/ast2ram/ProvenanceTranslator.cpp
new file mode 100644
index 00000000000..2c4d4f8a6a5
--- /dev/null
+++ b/src/ast2ram/ProvenanceTranslator.cpp
@@ -0,0 +1,327 @@
+/*
+ * Souffle - A Datalog Compiler
+ * Copyright (c) 2018 The Souffle Developers. All rights reserved
+ * Licensed under the Universal Permissive License v 1.0 as shown at:
+ * - https://opensource.org/licenses/UPL
+ * - <souffle root>/licenses/SOUFFLE-UPL.txt
+ */
+
+/************************************************************************
+ *
+ * @file ProvenanceTranslator.h
+ *
+ ***********************************************************************/
+
+#include "ast2ram/ProvenanceTranslator.h"
+#include "ast/BinaryConstraint.h"
+#include "ast/Clause.h"
+#include "ast/Constraint.h"
+#include "ast/ProvenanceNegation.h"
+#include "ast/SubroutineArgument.h"
+#include "ast/analysis/AuxArity.h"
+#include "ast/utility/Utils.h"
+#include "ast/utility/Visitor.h"
+#include "ast2ram/ProvenanceClauseTranslator.h"
+#include "ast2ram/ValueIndex.h"
+#include "ram/ExistenceCheck.h"
+#include "ram/Filter.h"
+#include "ram/Negation.h"
+#include "ram/Query.h"
+#include "ram/Sequence.h"
+#include "ram/SignedConstant.h"
+#include "ram/SubroutineReturn.h"
+#include "ram/UndefValue.h"
+#include "souffle/BinaryConstraintOps.h"
+#include <sstream>
+
+namespace souffle::ast2ram {
+
+void ProvenanceTranslator::translateProgram(const ast::TranslationUnit& translationUnit) {
+    // do the regular translation
+    AstToRamTranslator::translateProgram(translationUnit);
+
+    // add subroutines for each clause
+    addProvenanceClauseSubroutines(program);
+}
+
+void ProvenanceTranslator::addNegation(ast::Clause& clause, const ast::Atom* atom) {
+    clause.addToBody(mk<ast::ProvenanceNegation>(souffle::clone(atom)));
+}
+
+void ProvenanceTranslator::addProvenanceClauseSubroutines(const ast::Program* program) {
+    visitDepthFirst(*program, [&](const ast::Clause& clause) {
+        std::stringstream relName;
+        relName << clause.getHead()->getQualifiedName();
+
+        // do not add subroutines for info relations or facts
+        if (relName.str().find("@info") != std::string::npos || clause.getBodyLiterals().empty()) {
+            return;
+        }
+
+        std::string subroutineLabel =
+                relName.str() + "_" + std::to_string(getClauseNum(program, &clause)) + "_subproof";
+        ramSubs[subroutineLabel] = makeSubproofSubroutine(clause);
+
+        std::string negationSubroutineLabel =
+                relName.str() + "_" + std::to_string(getClauseNum(program, &clause)) + "_negation_subproof";
+        ramSubs[negationSubroutineLabel] = makeNegationSubproofSubroutine(clause);
+    });
+}
+
+/** make a subroutine to search for subproofs */
+Own<ram::Statement> ProvenanceTranslator::makeSubproofSubroutine(const ast::Clause& clause) {
+    auto intermediateClause = mk<ast::Clause>(souffle::clone(clause.getHead()));
+
+    // create a clone where all the constraints are moved to the end
+    for (auto bodyLit : clause.getBodyLiterals()) {
+        // first add all the things that are not constraints
+        if (!isA<ast::Constraint>(bodyLit)) {
+            intermediateClause->addToBody(souffle::clone(bodyLit));
+        }
+    }
+
+    // now add all constraints
+    for (auto bodyLit : ast::getBodyLiterals<ast::Constraint>(clause)) {
+        intermediateClause->addToBody(souffle::clone(bodyLit));
+    }
+
+    // name unnamed variables
+    nameUnnamedVariables(intermediateClause.get());
+
+    // add constraint for each argument in head of atom
+    ast::Atom* head = intermediateClause->getHead();
+    size_t auxiliaryArity = auxArityAnalysis->getArity(head);
+    auto args = head->getArguments();
+    for (size_t i = 0; i < head->getArity() - auxiliaryArity; i++) {
+        auto arg = args[i];
+
+        if (auto var = dynamic_cast<ast::Variable*>(arg)) {
+            // FIXME: float equiv (`FEQ`)
+            auto constraint = mk<ast::BinaryConstraint>(
+                    BinaryConstraintOp::EQ, souffle::clone(var), mk<ast::SubroutineArgument>(i));
+            constraint->setFinalType(BinaryConstraintOp::EQ);
+            intermediateClause->addToBody(std::move(constraint));
+        } else if (auto func = dynamic_cast<ast::Functor*>(arg)) {
+            TypeAttribute returnType;
+            if (auto* inf = dynamic_cast<ast::IntrinsicFunctor*>(func)) {
+                assert(inf->getFinalReturnType().has_value() && "functor has missing return type");
+                returnType = inf->getFinalReturnType().value();
+            } else if (auto* udf = dynamic_cast<ast::UserDefinedFunctor*>(func)) {
+                assert(udf->getFinalReturnType().has_value() && "functor has missing return type");
+                returnType = udf->getFinalReturnType().value();
+            } else {
+                assert(false && "unexpected functor type");
+            }
+            auto opEq = returnType == TypeAttribute::Float ? BinaryConstraintOp::FEQ : BinaryConstraintOp::EQ;
+            auto constraint =
+                    mk<ast::BinaryConstraint>(opEq, souffle::clone(func), mk<ast::SubroutineArgument>(i));
+            constraint->setFinalType(opEq);
+            intermediateClause->addToBody(std::move(constraint));
+        } else if (auto rec = dynamic_cast<ast::RecordInit*>(arg)) {
+            auto constraint = mk<ast::BinaryConstraint>(
+                    BinaryConstraintOp::EQ, souffle::clone(rec), mk<ast::SubroutineArgument>(i));
+            constraint->setFinalType(BinaryConstraintOp::EQ);
+            intermediateClause->addToBody(std::move(constraint));
+        }
+    }
+
+    // index of level argument in argument list
+    size_t levelIndex = head->getArguments().size() - auxiliaryArity;
+
+    // add level constraints, i.e., that each body literal has height less than that of the head atom
+    const auto& bodyLiterals = intermediateClause->getBodyLiterals();
+    for (auto lit : bodyLiterals) {
+        if (auto atom = dynamic_cast<ast::Atom*>(lit)) {
+            auto arity = atom->getArity();
+            auto atomArgs = atom->getArguments();
+            // arity - 1 is the level number in body atoms
+            auto constraint = mk<ast::BinaryConstraint>(BinaryConstraintOp::LT,
+                    souffle::clone(atomArgs[arity - 1]), mk<ast::SubroutineArgument>(levelIndex));
+            constraint->setFinalType(BinaryConstraintOp::LT);
+            intermediateClause->addToBody(std::move(constraint));
+        }
+    }
+    return ProvenanceClauseTranslator(*this).translateClause(*intermediateClause, clause);
+}
+
+/** make a subroutine to search for subproofs for the non-existence of a tuple */
+Own<ram::Statement> ProvenanceTranslator::makeNegationSubproofSubroutine(const ast::Clause& clause) {
+    // TODO (taipan-snake): Currently we only deal with atoms (no constraints or negations or aggregates
+    // or anything else...)
+    //
+    // The resulting subroutine looks something like this:
+    // IF (arg(0), arg(1), _, _) IN rel_1:
+    //   return 1
+    // IF (arg(0), arg(1), _ ,_) NOT IN rel_1:
+    //   return 0
+    // ...
+
+    // clone clause for mutation, rearranging constraints to be at the end
+    auto clauseReplacedAggregates = mk<ast::Clause>(souffle::clone(clause.getHead()));
+
+    // create a clone where all the constraints are moved to the end
+    for (auto bodyLit : clause.getBodyLiterals()) {
+        // first add all the things that are not constraints
+        if (!isA<ast::Constraint>(bodyLit)) {
+            clauseReplacedAggregates->addToBody(souffle::clone(bodyLit));
+        }
+    }
+
+    // now add all constraints
+    for (auto bodyLit : ast::getBodyLiterals<ast::Constraint>(clause)) {
+        clauseReplacedAggregates->addToBody(souffle::clone(bodyLit));
+    }
+
+    struct AggregatesToVariables : public ast::NodeMapper {
+        mutable int aggNumber{0};
+
+        AggregatesToVariables() = default;
+
+        Own<ast::Node> operator()(Own<ast::Node> node) const override {
+            if (dynamic_cast<ast::Aggregator*>(node.get()) != nullptr) {
+                return mk<ast::Variable>("agg_" + std::to_string(aggNumber++));
+            }
+
+            node->apply(*this);
+            return node;
+        }
+    };
+
+    AggregatesToVariables aggToVar;
+    clauseReplacedAggregates->apply(aggToVar);
+
+    // build a vector of unique variables
+    std::vector<const ast::Variable*> uniqueVariables;
+
+    visitDepthFirst(*clauseReplacedAggregates, [&](const ast::Variable& var) {
+        if (var.getName().find("@level_num") == std::string::npos) {
+            // use find_if since uniqueVariables stores pointers, and we need to dereference the pointer to
+            // check equality
+            if (std::find_if(uniqueVariables.begin(), uniqueVariables.end(),
+                        [&](const ast::Variable* v) { return *v == var; }) == uniqueVariables.end()) {
+                uniqueVariables.push_back(&var);
+            }
+        }
+    });
+
+    // a mapper to replace variables with subroutine arguments
+    struct VariablesToArguments : public ast::NodeMapper {
+        const std::vector<const ast::Variable*>& uniqueVariables;
+
+        VariablesToArguments(const std::vector<const ast::Variable*>& uniqueVariables)
+                : uniqueVariables(uniqueVariables) {}
+
+        Own<ast::Node> operator()(Own<ast::Node> node) const override {
+            // replace unknown variables
+            if (auto varPtr = dynamic_cast<const ast::Variable*>(node.get())) {
+                if (varPtr->getName().find("@level_num") == std::string::npos) {
+                    size_t argNum = std::find_if(uniqueVariables.begin(), uniqueVariables.end(),
+                                            [&](const ast::Variable* v) { return *v == *varPtr; }) -
+                                    uniqueVariables.begin();
+
+                    return mk<ast::SubroutineArgument>(argNum);
+                } else {
+                    return mk<ast::UnnamedVariable>();
+                }
+            }
+
+            // apply recursive
+            node->apply(*this);
+
+            // otherwise nothing
+            return node;
+        }
+    };
+
+    auto makeRamAtomExistenceCheck = [&](ast::Atom* atom) {
+        auto relName = getConcreteRelationName(atom);
+        size_t auxiliaryArity = auxArityAnalysis->getArity(atom);
+
+        // translate variables to subroutine arguments
+        VariablesToArguments varsToArgs(uniqueVariables);
+        atom->apply(varsToArgs);
+
+        // construct a query
+        VecOwn<ram::Expression> query;
+        auto atomArgs = atom->getArguments();
+
+        // add each value (subroutine argument) to the search query
+        for (size_t i = 0; i < atom->getArity() - auxiliaryArity; i++) {
+            auto arg = atomArgs[i];
+            query.push_back(translateValue(arg, ValueIndex()));
+        }
+
+        // fill up query with nullptrs for the provenance columns
+        for (size_t i = 0; i < auxiliaryArity; i++) {
+            query.push_back(mk<ram::UndefValue>());
+        }
+
+        // ensure the length of query tuple is correct
+        assert(query.size() == atom->getArity() && "wrong query tuple size");
+
+        // create existence checks to check if the tuple exists or not
+        return mk<ram::ExistenceCheck>(relName, std::move(query));
+    };
+
+    auto makeRamReturnTrue = [&]() {
+        VecOwn<ram::Expression> returnTrue;
+        returnTrue.push_back(mk<ram::SignedConstant>(1));
+        return mk<ram::SubroutineReturn>(std::move(returnTrue));
+    };
+
+    auto makeRamReturnFalse = [&]() {
+        VecOwn<ram::Expression> returnFalse;
+        returnFalse.push_back(mk<ram::SignedConstant>(0));
+        return mk<ram::SubroutineReturn>(std::move(returnFalse));
+    };
+
+    // the structure of this subroutine is a sequence where each nested statement is a search in each
+    // relation
+    VecOwn<ram::Statement> searchSequence;
+
+    // make a copy so that when we mutate clause, pointers to objects in newClause are not affected
+    auto newClause = souffle::clone(clauseReplacedAggregates);
+
+    // go through each body atom and create a return
+    size_t litNumber = 0;
+    for (const auto& lit : newClause->getBodyLiterals()) {
+        if (auto atom = dynamic_cast<ast::Atom*>(lit)) {
+            auto existenceCheck = makeRamAtomExistenceCheck(atom);
+            auto negativeExistenceCheck = mk<ram::Negation>(souffle::clone(existenceCheck));
+
+            // create a ram::Query to return true/false
+            appendStmt(searchSequence,
+                    mk<ram::Query>(mk<ram::Filter>(std::move(existenceCheck), makeRamReturnTrue())));
+            appendStmt(searchSequence,
+                    mk<ram::Query>(mk<ram::Filter>(std::move(negativeExistenceCheck), makeRamReturnFalse())));
+        } else if (auto neg = dynamic_cast<ast::Negation*>(lit)) {
+            auto atom = neg->getAtom();
+            auto existenceCheck = makeRamAtomExistenceCheck(atom);
+            auto negativeExistenceCheck = mk<ram::Negation>(souffle::clone(existenceCheck));
+
+            // create a ram::Query to return true/false
+            appendStmt(searchSequence,
+                    mk<ram::Query>(mk<ram::Filter>(std::move(existenceCheck), makeRamReturnFalse())));
+            appendStmt(searchSequence,
+                    mk<ram::Query>(mk<ram::Filter>(std::move(negativeExistenceCheck), makeRamReturnTrue())));
+        } else if (auto con = dynamic_cast<ast::Constraint*>(lit)) {
+            VariablesToArguments varsToArgs(uniqueVariables);
+            con->apply(varsToArgs);
+
+            // translate to a ram::Condition
+            auto condition = translateConstraint(con, ValueIndex());
+            auto negativeCondition = mk<ram::Negation>(souffle::clone(condition));
+
+            appendStmt(searchSequence,
+                    mk<ram::Query>(mk<ram::Filter>(std::move(condition), makeRamReturnTrue())));
+            appendStmt(searchSequence,
+                    mk<ram::Query>(mk<ram::Filter>(std::move(negativeCondition), makeRamReturnFalse())));
+        }
+
+        litNumber++;
+    }
+
+    return mk<ram::Sequence>(std::move(searchSequence));
+}
+
+}  // namespace souffle::ast2ram
diff --git a/src/ast2ram/ProvenanceTranslator.h b/src/ast2ram/ProvenanceTranslator.h
new file mode 100644
index 00000000000..a2f34e8390d
--- /dev/null
+++ b/src/ast2ram/ProvenanceTranslator.h
@@ -0,0 +1,38 @@
+/*
+ * Souffle - A Datalog Compiler
+ * Copyright (c) 2018 The Souffle Developers. All rights reserved
+ * Licensed under the Universal Permissive License v 1.0 as shown at:
+ * - https://opensource.org/licenses/UPL
+ * - <souffle root>/licenses/SOUFFLE-UPL.txt
+ */
+
+/************************************************************************
+ *
+ * @file ProvenanceTranslator.h
+ *
+ ***********************************************************************/
+
+#pragma once
+
+#include "ast2ram/AstToRamTranslator.h"
+
+namespace souffle::ast2ram {
+
+class ProvenanceTranslator : public AstToRamTranslator {
+public:
+    ProvenanceTranslator() = default;
+    ~ProvenanceTranslator() = default;
+
+protected:
+    void translateProgram(const ast::TranslationUnit& translationUnit) override;
+    void addNegation(ast::Clause& clause, const ast::Atom* atom) override;
+private:
+    /** translate RAM code for subroutine to get subproofs */
+    Own<ram::Statement> makeSubproofSubroutine(const ast::Clause& clause);
+
+    /** translate RAM code for subroutine to get subproofs for non-existence of a tuple */
+    Own<ram::Statement> makeNegationSubproofSubroutine(const ast::Clause& clause);
+
+    void addProvenanceClauseSubroutines(const ast::Program* program);
+};
+}  // namespace souffle::ast2ram
diff --git a/src/main.cpp b/src/main.cpp
index 266cc98e71e..d1f8c15ff34 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -57,6 +57,7 @@
 #include "ast/transform/SimplifyAggregateTargetExpression.h"
 #include "ast/transform/UniqueAggregationVariables.h"
 #include "ast2ram/AstToRamTranslator.h"
+#include "ast2ram/ProvenanceTranslator.h"
 #include "config.h"
 #include "interpreter/Engine.h"
 #include "interpreter/ProgInterface.h"
@@ -582,7 +583,9 @@ int main(int argc, char** argv) {
     // ------- execution -------------
     /* translate AST to RAM */
     debugReport.startSection();
-    auto ramTranslationUnit = ast2ram::AstToRamTranslator().translateUnit(*astTranslationUnit);
+    auto ramTranslationUnit = Global::config().has("provenance")
+                                      ? ast2ram::ProvenanceTranslator().translateUnit(*astTranslationUnit)
+                                      : ast2ram::AstToRamTranslator().translateUnit(*astTranslationUnit);
     debugReport.endSection("ast-to-ram", "Translate AST to RAM");
 
     // Apply RAM transforms