{'fraction_non_alphanumeric': 0.0776981465136805, 'fraction_numerical': 0.008903795233892321, 'mean_word_length': 3.7028391167192427, 'pattern_counts': {'":': 0, '<': 10, '<?xml version=': 0, '>': 2, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 82, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Securing Databases from Probabilistic Inference

Databases can leak confidential information when users combine query results with probabilistic data dependencies and prior knowledge. Current research offers mechanisms that either handle a limited class of dependencies or lack tractable enforcement algorithms. We propose a foundation for Database Inference Control based on ProbLog, a probabilistic logic programming language. We leverage this foundation to develop Angerona, a provably secure enforcement mechanism that prevents information leakage in the presence of probabilistic dependencies. We then provide a tractable inference algorithm for a practically relevant fragment of ProbLog. We empirically evaluate Angerona's performance showing that it scales to relevant security-critical problems.

An important and relevant class of data dependencies are probabilistic dependencies, such as those found in genomics [43], [47], [49], social networks [40], and location tracking [52]. Attackers can exploit these dependencies to infer sensitive information with high confidence. To effectively prevent probabilistic inferences, DBIC mechanisms should (1) support a large class of probabilistic dependencies, and (2) have tractable runtime performance. The former is needed to express different attacker models. The latter is necessary for mechanisms to scale to real-world databases.
First, we develop ATKLOG, a language for formalizing users' beliefs and how they evolve while interacting with the system. ATKLOG builds on PROBLOG [20], [21], [31], a stateof-the-art probabilistic extension of DATALOG, and extends its semantics by building on three key ideas from [18], [46], [51]: (1) users' beliefs can be represented as probability distributions, (2) belief revision can be performed by conditioning the probability distribution based on the users' observations, and (3) rejecting queries as insecure may leak information. By combining DATALOG with probabilistic models and belief revision based on users' knowledge, ATKLOG provides a natural and expressive language to model users' beliefs and thereby serves as a foundation for DBIC in the presence of probabilistic inferences.
Second, we identify acyclic PROBLOG programs, a class of programs where probabilistic inference's data complexity is PTIME. We precisely characterize this class and develop a dedicated inference engine. Since PROBLOG's inference is intractable in general, we see acyclic programs as an essential building block to effectively using ATKLOG for DBIC.
Finally, we present ANGERONA 1 , a novel DBIC mechanism that secures databases against probabilistic inferences. We prove that ANGERONA is secure with respect to any ATKLOGattacker. In contrast to existing mechanisms, ANGERONA provides precise tractability and completeness guarantees for a practically relevant class of attackers. We empirically show that ANGERONA scales to relevant problems of interest. Structure. In §II, we illustrate the security risks associated with probabilistic data dependencies. In §III, we present our system model, which we formalize in §IV. We introduce ATKLOG in §V and in §VI we present our inference engine for acyclic programs. In §VII, we present ANGERONA. We discuss related work in §VIII and draw conclusions in §IX. A prototype of our enforcement mechanism is available at [36].
II. MOTIVATING EXAMPLE Hospitals and medical research centres store large quantities of health-related information for purposes ranging from diag-nosis to research. As this information is extremely sensitive, the databases used must be carefully secured [13], [28]. This task is, however, challenging due to the dependencies between health-related data items. For instance, information about someone's hereditary diseases or genome can be inferred from information about her relatives. Even seemingly non-sensitive information, such as someone's job or habits, may leak sensitive health-related information such as her predisposition to diseases. Most of these dependencies can be formalized using probabilistic models developed by medical researchers.
Consider a database storing information about the smoking habits of patients and whether they have been diagnosed with lung cancer. The database contains the tables patient, smokes, cancer , father , and mother . The first table contains all patients, the second contains all regular smokers, the third contains all diagnosed patients, and the last two associate patients with their parents. Now consider the following probabilistic model: (a) every patient has a 5% chance of developing cancer, (b) for each parent with cancer, the likelihood that a child develops cancer increases by 15%, and (c) if a patient smokes regularly, his probability of developing cancer increases by 25%. We intentionally work with a simple model since, despite its simplicity, it illustrates the challenges of securing data with probabilistic dependencies. We refer the reader to medical research for more realistic probabilistic models [4], [69].
The database is shared between different medical researchers, each conducting a research study on a subset of the patients. All researchers have access to the patient, smokes, father , and mother tables. Each researcher, however, has access only to the subset of the cancer table associated with the patients that opted-in to his research study. We want to protect our database against a malicious researcher whose goal is to infer the health status of patients not participating in the study. This is challenging since restricting direct access to the cancer table is insufficient. Sensitive information may be leaked even by queries involving only authorized data. For instance, the attacker may know that the patient Carl , which has not disclosed his health status, smokes regularly. From this, he can infer that Carl 's probability of developing lung cancer is, at least, 30%. If, additionally, Carl 's parents optedin to the research study and both have cancer, the attacker can directly infer that the probability of Carl developing lung cancer is 60% by accessing his parents' information.
Security mechanisms that ignore such probabilistic dependencies allow attackers to infer sensitive information. An alternative is to use standard DBIC mechanisms and encode all dependencies as precise, non-probabilistic, dependencies. This, however, would result in an unusable system. Medical researchers, even honest ones, would be able to access the health-related status only of those patients whose relatives also opted-in to the user study, independently of the amount of leaked information, which may be negligible. Hence, to secure the database and retain usability, it is essential to reason about the probabilistic dependencies. We assume that all communication between users and the components and between the components themselves is over secure channels.
Database System. The database system manages the system's data. Its state is a mapping from tables to sets of tuples.
Users. Each user has a unique account used to retrieve information from the database system by issuing SELECT commands. Note that these commands do not change the database state. This reflects settings where users have only read-access to a database. Each command is checked by the inference control system and is executed if and only if the command is authorized by the security policy.
Security policy. The system's security policy consists of a set of negative permissions specifying information to be kept secret. These permissions express bounds on users ' beliefs, formalized as probability distributions, about the actual database content. Negative permissions are formalized using commands of the form SECRET q FOR u THRESHOLD l, where q is a query, u is a user identifier, and l is a rational number, 0 ≤ l ≤ 1. This represents the requirement that "A user u's belief in the result of q must be less than l." Namely, the probability assigned by u's belief to q's result must be less than l. Requirements like "A user u is not authorized to know the result of q" can be formalized as SECRET q FOR u THRESHOLD 1. The system also supports commands of the form SECRET q FOR USERS NOT IN {u 1 , . . . , u n } THRESHOLD l, which represents the requirement that "For all users u ∈ {u 1 , . . . , u n }, u's belief in the result of q must be less than l." Attacker. An attacker is a system user with an assigned user account, and each user is a potential attacker. An attacker's goal is to violate the security policy, that is, to read or infer information about one of the SECRETs with a probability of at least the given threshold.
An attacker can interact with the system and observe its behaviour in response to his commands. Furthermore, he can reason about this information and infer information by exploiting domain-specific relationships between data items.
We assume that attackers know the database schema as well as any integrity constraints on it. Attacker Model. An attacker model represents each user's initial beliefs about the actual database state and how he updates his beliefs by interacting with the system and observing its behaviour in response to his commands. These beliefs may reflect the attacker's knowledge of domain-specific relationships between the data items or prior knowledge. Inference Control System. The inference control system protects the confidentiality of database data. It consists of a PEP and a PDP, configured with a security policy P and an attacker model ATK . For each user, the inference control system keeps track of the user's beliefs according to ATK .
The system intercepts all commands issued by the users. When a user u issues a command c, the inference control system decides whether u is authorized to execute c. If c complies with the policy, i.e., the users' beliefs still satisfy P even after executing c, then the system forwards the command to the database, which executes c and returns its result to u. Otherwise, it raises a security exception and rejects c.

A. Database Model
We introduce here background and notation for databases and queries. Our formalization follows [2].
Let R be a countably infinite set representing identifiers of relation schemas. A database schema D is a pair Σ, dom , where Σ is a first-order signature and dom is a fixed domain. For simplicity, we consider just a single domain. Extensions to the many-sorted case are straightforward [2]. The signature Σ consists of a set of relation schemas R ∈ R, each schema with arity |R|, and one constant symbol for each constant in dom. We interpret constants by themselves in the semantics.
A state s of D is a finite Σ-structure with domain dom that interprets each relation schema R by an |R|-ary relation over dom. We denote by Ω D the set of all states. Given a schema R ∈ D, s(R) denotes the tuples that belong to (the interpretation of) R in the state s. We assume that the domain dom is finite, as is standard for many application areas combining databases and probabilistic reasoning [20], [33], [47], [65]. In this case, the set of all states Ω D is finite.
A query q over a schema D is of the form {x | φ}, where x is a sequence of variables, φ is a relational calculus formula over D, and φ's free variables are those in x. A boolean query is a query { | φ}, also written as φ, where φ is a sentence. The result of executing a query q on a state s, denoted by [q] s , is a boolean value in { , ⊥}, if q is a boolean query, or a set of tuples otherwise. Furthermore, given a sentence φ, φ denotes the set {s ∈ Ω D | [φ] s = }. We denote by RC (respectively RC bool ) the set of all relational calculus queries (respectively sentences). We consider only domain-independent queries and we employ the standard relational calculus semantics [2].
An integrity constraint over D is a relational calculus sentence γ over D. Given a state s, we say that s satisfies the constraint γ iff [γ] s = . Given a set of constraints Γ, Ω Γ D denotes the set of all states satisfying the constraints in Γ, i.e., Ω Γ D = {s ∈ Ω D | γ∈Γ [γ] s = }. Example IV.1. The database associated with the example in §II consists of five relational schemas patient, smokes, cancer , father , and mother , where the first three schemas have arity 1 and the last two have arity 2. We assume that there are only three patients Alice, Bob, and Carl, so the domain dom is {Alice, Bob, Carl}. The integrity constraints are as follows: • Alice, Bob, and Carl are patients.

¬smokes(Alice) ∧ smokes(Bob) ∧ smokes(Carl)
Given these constraints, there are just 8 possible database states in Ω Γ D , which differ only in their cancer relation. The content of the cancer relation is a subset of {Alice, Bob, Carl}, whereas the content of the other tables is shown in Figure 2. We denote each possible world as s C , where the set C ⊆ {Alice, Bob, Carl} denotes the users having cancer.

B. Security Policies
Existing access control models for databases are inadequate to formalize security requirements capturing probabilistic dependencies. For example, SQL cannot express statements like "A user u's belief that φ holds must be less than l." We present a simple framework, inspired by knowledge-based policies [51], for expressing such requirements.
A D-secret is a tuple U, φ, l , where U is either a finite set of users in U or a co-finite set of users, i.e., U = U \ U for some finite U ⊂ U, φ is a relational calculus sentence over D, and l is rational number 0 ≤ l ≤ 1 specifying the uncertainty threshold. Abusing notation, when U consists of a single user u, we write u instead of {u}. Informally, U, φ, l represents that for each user u ∈ U , u's belief that φ holds in the actual database state must be less than l. Therefore, a command of the form SECRET q FOR u THRESHOLD l can be represented as u, q, l , whereas a command SECRET q FOR USERS NOT IN {u 1 , . . . , u n } THRESHOLD l can be represented as U \{u 1 , . . . , u n }, q, l . Finally, a D-security policy is a finite set of D-secrets. Given a D-security policy P , we denote by secrets(P, u) the set of D-secrets associated with the user u, i.e., secrets(P, u) = { u, φ, l | U, φ, l ∈ P ∧u ∈ U }. Note that the function secrets is computable since the set U is always either finite or co-finite.
Our framework also allows the specification of lower bounds. Requirements of the form "A user u's belief that φ holds must be greater than l" can be formalized as u, ¬φ, 1 − l (since the probability of ¬φ is 1 − P (φ), where P (φ) is φ's probability). Security policies can be extended to support secrets over non-boolean queries. A secret u, {x | φ(x)}, l can be seen as a shorthand for the set i.e., u's belief in any tuple t being in the query's result must be less than l.
Example IV.2. Let Mallory denote the malicious researcher from §II and D be the schema from Example IV.1. Consider the requirement from §II: Mallory's belief in a patient having cancer must be less than 50%. This can be formalized as Mallory, cancer (Alice), 1 /2 , Mallory, cancer (Bob), 1 /2 , and Mallory, cancer (Carl), 1 /2 , or equivalently as Mallory, {p | cancer (p)}, 1 /2 . In contrast, the requirement "For all users u that are not Carl , u's belief in Carl having cancer must be less than 50%" can be formalized as U \ {Carl }, cancer (Carl), 1 /2 , where Carl denotes the user identifier associated with Carl.

C. Formalized System Model
We now formalize our system model. We first define a system configuration, which describes the database schema and the integrity constraints. Afterwards, we define the system's state. Finally, we define a system run, which represents a possible interaction of users with the system.
A system configuration is a tuple D, Γ , where D is a database schema and Γ is a set of D-integrity constraints. Let C = D, Γ be a system configuration. A C-system state is a tuple db, U, P , where db ∈ Ω Γ D is a database state, U ⊂ U is a finite set of users, and P is a D-security policy. A C-query is a pair u, φ where u ∈ U is a user and φ is a relational calculus sentence over D. 2 We denote by Ω C the set of all system states and by Q C the set of all queries.
A C-event is a triple q, a, res , where q is a C-query in Q C , a ∈ { , ⊥} is a security decision, where stands for "authorized query" and ⊥ stands for "unauthorized query", and res ∈ { , ⊥, †} is the query's result, where and ⊥ represent the usual boolean values and † represents that the query was not executed as access was denied. Given a Cevent e = q, a, res , we denote by q(e) (respectively a(e) and res(e)) the query q (respectively the decision a and the result res). A C-history is a finite sequence of C-events. We denote by H C the set of all possible C-histories. Moreover, given a sequence h, |h| denotes its length, h(i) its i-th element, and h i the sequence containing the first i elements of h. We also denote by h 0 the empty sequence , and · denotes the concatenation operator.
We now formalize Policy Decision Points. A C-PDP is a function f : Ω C × Q C × H C → { , ⊥} taking as input a system state, a query, and a history and returning the security decision, accept ( ) or deny (⊥).
Let C be a system configuration, s = db, U, P be a Cstate, and f be a C-PDP. A C-history h is compatible with s and f iff for each In other words, h is compatible with s and f iff it was generated by the PDP f starting in state s.
A (C, f )-run is a pair s, h , where s is a system state in Ω C and h is a history in H C compatible with s and f . Since all queries are SELECT queries, the system state does not change along the run. Hence, our runs consist of a state and a history instead of e.g., an alternating sequence of states and actions (as is standard for runs). We denote by runs(C, f ) the set of all (C, f )-runs. Furthermore, given a run r = db, U, P , h , we denote by r i the run db, U, P , h i , and we use dot notation to access to r's components. For instance, r.db denotes the database state db and r.h denotes the history.

D. Attacker Model
To reason about DBIC, it is essential to precisely define (1) how users interact with the system, (2) how they reason about the system's behaviour, (3) their initial beliefs about the database state, and (4) how these beliefs change by observing the system's behaviour. We formalize this in an attacker model.
Each user has an initial belief about the database state. Following [18], [19], [29], [51], we represent a user's beliefs as a probability distribution over all database states. Furthermore, users observe the system's behaviour and derive information about the database content. We formalize a user's observations as an equivalence relation over runs, where two runs are equivalent iff the user's observations are the same in both runs, as is standard in information-flow [7], [8]. A user's knowledge is the set of all database states that he considers possible given his observations. Finally, we use Bayesian conditioning to update a user's beliefs given his knowledge.
Let C = D, Γ be a system configuration and f be a C-PDP. A C-probability distribution is a discrete probability distribution given by a function P : (E ) as is standard. We denote by P C the set of all possible Cprobability distributions. Abusing notation, we extend probability distributions to formulae: We now introduce indistinstinguishability, an equivalence relation used in information-flow control [41]. Let C be a system configuration and f be a C-PDP. Given a history h and a user u ∈ U, h| u denotes the history obtained from h by removing all C-events from users other than u, namely | u = , and if h = u , q , a, res · h , then h| u = h | u in case u = u , and h| u = u, q , a, res · h | u if u = u . Given two runs r = db, U, P , h and r = db , U , P , h in runs(C, f ) and a user u ∈ U, we say that r and r are indistinguishable for u, written r ∼ u r , iff h| u = h | u . This means that r and r are indistinguishable for a user u iff the system's behaviour in response to u's commands is the same in both runs. Note that ∼ u depends on both C and f , which we generally leave implicit. Given a run r, [r] ∼u is the equivalence class of r with respect to ∼ u , i.e, [r] ∼u = {r ∈ runs(C, f ) | r ∼ u r}, whereas r ∼u is set of all databases associated to the runs in [r] ∼u , i.e., r ∼u = {db | ∃U, P, h. db, U, P , h ∈ [r] ∼u }.
Definition IV.1. Let C = D, Γ be a configuration and f be a C-PDP. A (C, f )-attacker model is a function ATK : U → P C associating to each user u ∈ U a C-probability distribution representing u's initial beliefs. Additionally, for all users u ∈ U and all states s ∈ Ω Γ D , we require that ATK (u)(s) > 0. The semantics of ATK is ATK (u, r) = λs ∈ Ω Γ D . ATK (u)(s | r ∼u ), where u ∈ U and r ∈ runs(C, f ).
The semantics of an attacker model ATK associates to each user u and each run r the probability distribution obtained by updating u's initial beliefs given his knowledge with respect to the run r. We informally refer to ATK (u, r)( φ ) as u's beliefs in a sentence φ (given a run r).
Example IV.4. The attacker model for the example from §II is as follows. Let X Alice , X Bob , and X Carl be three boolean random variables, representing the probability that the corresponding patient has cancer. They define the following joint probability distribution, which represents a user's initial beliefs about the actual database state: P (X Alice , X Bob , X Carl ) = P (X Alice ) · P (X Bob ) · P (X Carl | X Alice , X Bob ). The probability distributions of these variables are given in Figure 3 and they are derived from the probabilistic model in §II. We associate each outcome (x, y, z) of X Alice , X Bob , X Carl with the corresponding database state s C , where C is the set of patients such that the outcome of the corresponding variable is . For each user u ∈ U, the distribution P u is defined as P u (s C ) = P (X Alice = x, X Bob = y, X Carl = z), where x (respectively y and z) is if Alice (respectively Bob and Carl) is in C and ⊥ otherwise. Figure 4 shows the probabilities associated with each state in Ω Γ D , i.e., a user's initial beliefs. Finally, the attacker model is ATK = λu ∈ U.P u .

E. Confidentiality
We first define the notion of a secrecy-preserving run for a secret u, φ, l and an attacker model ATK . Informally, a run r is secrecy-preserving for u, φ, l iff whenever an attacker's belief in the secret φ is below the threshold l, then there is no way for the attacker to increase his belief in φ above the threshold. Our notion of secrecy-preserving runs is inspired by existing security notions for query auditing [29].
Definition IV.2. Let C = D, Γ be a configuration, f be a C-PDP, and ATK be a (C, f )-attacker model. A run r is secrecypreserving for a secret u, φ, l and ATK iff for all 0 ≤ i < |r|, We now formalize our confidentiality notion. A PDP provides data confidentiality for an attacker model ATK iff all runs are secrecy-preserving for ATK . Note that our security notion can be seen as a probabilistic generalization of opacity [60] for the database setting. Our notion is also inspired by the semantics of knowledge-based policies [51].
Definition IV.3. Let C = D, Γ be a system configuration, f be a C-PDP, and ATK be a (C, f )-attacker model. We say that the PDP f provides data confidentiality with respect to C and ATK iff for all runs r = db, U, P , h in runs(C, f ), for all users u ∈ U , for all secrets s ∈ secrets(P, u), r is secrecy-preserving for s and ATK .
A PDP providing confidentiality ensures that if an attacker's initial belief in a secret φ is below the corresponding threshold, then there is no way for the attacker to increase his belief in φ above the threshold by interacting with the system. This guarantee does not however apply to trivial non-secrets, i.e., those secrets an attacker knows with a probability at least the threshold even before interacting with the system. No PDP can prevent their disclosure since the disclosure does not depend on the attacker's interaction with the database.
Example IV.5. Let r be the run given in Example IV.3, ATK be the attacker model in Example IV.4, and u be the user Mallory. In the following, φ 1 , φ 2 , and φ 3 denote cancer (Carl), cancer (Bob), and cancer (Alice) respectively, i.e., the three secrets from Example IV.2. Furthermore, we assume that the policy contains an additional secret Mallory, φ 4 , 1 /2 , where φ 4 := ¬cancer (Alice). Figure 5 illustrates Mallory's beliefs about φ 1 , . . . , φ 4 and whether the run is secrecy-preserving for the secrets φ 1 , . . . , φ 4 . The probabilities in the tables can be obtained by combining the states in r i ∼u , for 0 ≤ i ≤ 4, and φ j , for 1 ≤ j ≤ 4, with the probabilities from Figure 4. As shown in Figure 5, the run is not secrecy-preserving for the secrets φ 1 and φ 2 as it completely discloses that Alice and Bob have cancer, in the third and fourth steps respectively. Secrecypreservation is also violated for the secret φ 1 , even though r does not directly disclose any information about Carl 's health status. Indeed, in the last step of the run, Mallory's belief in φ 1 is 0.6, which is higher than the threshold 1 /2, even though his belief in φ 1 before learning that Bob had cancer was below the threshold. Note that φ 4 is a trivial non-secret: even before interacting with the system, Mallory's belief in φ 4 is 0.95.

F. Discussion
Our approach assumes that the attacker's capabilities are well-defined. While this, in general, is a strong assumption, there are many domains where such information is known. There are, however, domains where this information is lacking. In these cases, security engineers must (1) determine the appropriate beliefs capturing the desired attacker models, and (2) formalize them. The latter can be done, for instance, using ATKLOG (see §V). Note however that precisely eliciting the attackers' capabilities is still an open problem in DBIC.
Conventional logic programs are constructed from terms, atoms, literals, and rules. In the following, we consider only function-free logic programs, also called DATALOG programs. In this setting, terms are either variable identifiers or constants.
Let Σ be a first-order signature, dom be a finite domain, and Var be a countably infinite set of variable identifiers. A (Σ, dom)-atom R(v 1 , . . . , v n ) consists of a predicate symbol R ∈ Σ and arguments v 1 , . . . , v n such that n is the arity of R, and each v i , for 1 ≤ i ≤ n, is either a variable identifier in Var or a constant in dom. We denote by A Σ,dom the set {R(v 1 , . . . , v |R| ) | R ∈ Σ ∧ v 1 , . . . , v |R| ∈ dom ∪ Var } of all (Σ, dom)-atoms. A (Σ, dom)-literal l is either a (Σ, dom)-atom a or its negation ¬a, where a ∈ A Σ,dom . We denote by L Σ,dom the set A Σ,dom ∪ {¬a | a ∈ A Σ,dom } of all (Σ, dom)-literals. Given a literal l, vars(l) denotes the set of its variables, args(l) the list of its arguments, and pred (l) the predicate symbol used in l. As is standard, we say that a literal l is positive if it is an atom in A Σ,dom and negative if it is the negation of an atom. Furthermore, we say that a literal l is ground iff vars(l) = ∅.
A (Σ, dom)-rule is of the form h ← l 1 , . . . , l n , e 1 , . . . , e m , where h ∈ A Σ,dom is a (Σ, dom)-atom, l 1 , . . . , l n ∈ L Σ,dom are (Σ, dom)-literals, and e 1 , . . . , e m are equality and inequality constraints over the variables in h, l 1 , . . . , l m . 3 Given a rule r, we denote by head (r) the atom h, by body(r) the literals l 1 , . . . , l n , by cstr (r) the constraints e 1 , . . . , e m , and by body(r, i) the i-th literal in r's body, i.e., body(r, i) = l i . Furthermore, we denote by body + (r) (respectively body − (r)) all positive (respectively negative) literals in body(r). As is standard, we assume that the free variables in a rule's head are a subset of the free variables of the positive literals in the rule's body, i.e., vars(head (r)) ⊆ l∈body + (r) vars(l) ∪ (x=c)∈cstr (r)∧c∈dom {x}. Finally, a (Σ, dom)-logic program is a set of (Σ, dom)-ground atoms and (Σ, dom)-rules. We consider only programs p that do not contain negative cycles in the rules as is standard for stratified DATALOG [2].
To reason about probabilities, PROBLOG extends logic programming with probabilistic atoms. A (Σ, dom)-probabilistic atom is a (Σ, dom)-atom a annotated with a value 0 ≤ v ≤ 1, denoted v::a. PROBLOG supports both probabilistic ground atoms and rules having probabilistic atoms in their heads. PROBLOG also supports annotated disjunctions v 1 ::a 1 ; . . . ; v n ::a n , where a 1 , . . . , a n are ground atoms and 1≤i≤n v i ≤ 1, which denote that a 1 , . . . , a n are mutually exclusive probabilistic events happening with probabilities v 1 , . . . , v n . Annotated disjunctions can either be used as ground atoms or as heads in rules. Both annotated disjunctions and probabilistic rules are just syntactic sugar and can be expressed using ground probabilistic atoms and standard rules [20], [21], [31]; see Appendix A.
A (Σ, dom)-PROBLOG program p defines a probability distribution over all possible (Σ, dom)-structures, denoted p . Note that we consider only function-free PROBLOG programs. Hence, in our setting, PROBLOG is a probabilistic extension of DATALOG. Appendix A contains a formal account of PROBLOG's semantics.
Medical Data. We formalize the probability distribution from Example IV.4 as a PROBLOG program. We reuse the database schema and the domain from Example IV.1 as the first-order signature and the domain for the PROBLOG program. First, we encode the template shown in Figure 2 using ground atoms: patient(Alice), patient(Bob), patient(Carl), smokes(Bob), smokes(Carl), father (Bob, Carl), and mother (Alice, Carl). Second, we encode the probability distribution associated with the possible values of the cancer table using the following PROBLOG rules, which In the table, X and denote that secrecy-preservation is violated and satisfied respectively, whereas * denotes trivial secrets.
have probabilistic atoms in their heads: 1 /20::cancer (x) ← patient(x) 5 /19::cancer (x) ← smokes(x) 3 /14::cancer (y) ← father (x, y), cancer (x), mother (z, y), ¬cancer (z) 3 /14::cancer (y) ← father (x, y), ¬cancer (x), mother (z, y), cancer (z) 3 /7::cancer (y) ← father (x, y), cancer (x), mother (z, y), cancer (z) The coefficients in the above example are derived from §II. For instance, the probability that a smoking patient x whose parents are not not in the cancer relation has cancer is 30%. The coefficient in the first rule is 1 /20 since each patient has a 5% probability of having cancer. The coefficient in the second rule is 5 the probability that cancer (x) is derived from the second rule given that it has not been derived from the first rule. This ensures that the overall probability of deriving cancer (x) is 6 /20, i.e., 30%. The coefficients for the last two rules are derived analogously. Informally, a probabilistic ground atom 1 /2::cancer (Bob) expresses that cancer (Bob) holds with a probability 1 /2. Similarly, the rule 1 /20::cancer(x) ← patient(x) states that, for any x such that patient(x) holds, then cancer (x) can be derived with probability 1 /20. This program yields the probability distribution shown in Figure 4.

B. ATKLOG's Foundations
We first introduce belief programs, which formalize an attacker's initial beliefs. Afterwards, we formalize ATKLOG.
Belief Programs. A belief program formalizes an attacker's beliefs as a probability distribution over the database states.
A database schema D = Σ , dom extends a schema D = Σ, dom iff Σ contains all relation schemas in Σ. The extension D may extend Σ with additional predicate symbols necessary to encode probabilistic dependencies. Given an extension D , a D -state s agrees with a D-state s iff s (R) = s(R) for all R in D. Given a D-state s, we denote by EXT (s, D, D ) the set of all D -states that agree with s.
A (Σ , dom)-PROBLOG program p, where D = Σ , dom extends D, is a belief program over D. The Dsemantics of p is p D = λs ∈ Ω D . s ∈EXT (s,D,D ) p (s ). Given a system configuration C = D, Γ , a belief program p over D complies with C iff p D is a C-probability distribution. With a slight abuse of notation, we lift the semantics of belief programs to sentences: ATKLOG. An ATKLOG model specifies the initial beliefs of all users in U using belief programs.
Let D be a database schema and C = D, Γ be a system configuration. A C-ATKLOG model ATK is a function associating to each user u ∈ U , where U ⊂ U is a finite set of users, a belief program p u and to all users u ∈ U \U a belief program p 0 , such that for all users u ∈ U, ATK (u) D complies with C and for all database states s ∈ Ω Γ D , ATK (u) D (s) > 0, i.e., all database states satisfying the integrity constraints are possible. Informally, a C-ATKLOG model associates a distinct belief program to each user in U , and it associates to each user in U \ U the same belief program p 0 .
Given a C-PDP f , a C-ATKLOG model ATK defines the (C, f )-attacker model λu ∈ U. ATK (u) D that associates to each user u ∈ U the probability distribution defined by the belief program ATK (u). The semantics of this (C, f )-attacker model is: λu ∈ U.λr ∈ runs(C, f ).λs ∈ Ω Γ D . ATK (u) D (s | r ∼u ). Informally, given a C-ATKLOG model ATK , a C-PDP f , and a user u, u's belief in a database state s, given a run r, is obtained by conditioning the probability distribution defined by the belief program ATK (u) given the set of database states corresponding to all runs r ∼ u r.

VI. TRACTABLE INFERENCE FOR PROBLOG PROGRAMS
Probabilistic inference in PROBLOG is intractable in general. Its data complexity, i.e., the complexity of inference when only the programs' probabilistic ground atoms are part of the input and the rules are considered fixed and not part of the input, is #P -hard; see Appendix B. This limits the practical applicability of PROBLOG (and ATKLOG) for DBIC. To address this, we define acyclic PROBLOG programs, a class of programs where the data complexity of inference is PTIME.
Given a PROBLOG program p, our inference algorithm consists of three steps: (1) we compute all of p's derivations, (2) we compile these derivations into a Bayesian Network (BN) bn, and (3) we perform the inference over bn. To ensure tractability, we leverage two key insights. First, we exploit guarded negation [9] to develop a sound overapproximation, called the relaxed grounding, of all derivations of a program that is independent of the presence (or absence) of the probabilistic atoms. This ensures that whenever a ground atom can be derived from a program (for a possible assignment to the probabilistic atoms), the atom is also part of this program's relaxed grounding. This avoids grounding p for each possible assignment to the probabilistic atoms. Second, we introduce syntactic constraints (acyclicity) that ensure that bn is a forest of poly-trees. This ensures tractability since inference for poly-tree BNs can be performed in polynomial time in the network's size [47].
We also precisely characterize the expressiveness of acyclic PROBLOG programs. In this respect, we prove that acyclic programs are as expressive as forests of poly-tree BNs, one of the few classes of BNs with tractable inference.
As mentioned in §V, probabilistic rules and annotated disjunctions are just syntactic sugar. Hence, in the following we consider PROBLOG programs consisting just of probabilistic ground atoms and non-probabilistic rules. Note also that we treat ground atoms as rules with an empty body.

A. Preliminaries
Negation-guarded Programs. A rule r is negationguarded [9] iff all the variables occurring in negative literals also occur in positive literals, namely for all negative literals l in body − (r), vars(l) ⊆ l ∈body + (r) vars(l ). To illustrate, the rule C(x) ← A(x), ¬B(x) is negation-guarded, whereas C(x) ← A(x), ¬B(x, y) is not since the variable y does not occur in any positive literal. We say that a program p is negation-guarded if all rules r ∈ p are. Relaxed Grounding. The relaxed grounding of a program p is obtained by considering all probabilistic atoms as certain and by grounding all positive literals. For all negationguarded programs, the relaxed grounding of p is a sound overapproximation of all possible derivations in p. Given a program p and a rule r ∈ p, rg(p) denotes p's relaxed grounding and rg(p, r) denotes the set of r's ground instances. We formalize relaxed groundings in Appendix B. Dependency and Ground Graphs. The dependency graph of a program p, denoted graph(p), is the directed labelled graph having as nodes all the predicate symbols in p and having an edge a r,i −→ b iff there is a rule r such that a occurs in i-th literal in r's body and b occurs in r's head. Figure 6 depicts the dependency graph from Example VI.1. The ground graph of a program p is the graph obtained from its relaxed grounding. Hence, there is an edge a r,gr ,i −−−→ b from the ground atom a to the ground atom b iff there is a rule r and a ground rule gr ∈ rg(p, r) such that body(gr , i) ∈ {a, ¬a} and head (gr ) = b. Figure 7 depicts the ground graph from Example VI.1. Note that there are no incoming or  outgoing edges from A(3) because the node is not involved in any derivation. Propagation Maps. We use propagation maps to track how information flows inside rules. Given a rule r and a literal l ∈ body(r), the (r, l)-vertical map is the mapping µ from {1, . . . , |l|} to {1, . . . , |head (r)|} such that µ(i) = j iff args(l)(i) = args(head (r))(j) and args(l)(i) ∈ Var . Given a rule r and literals l and l in r's body, the (r, l, l )-horizontal map is the mapping µ from {1, . . . , |l|} to {1, . . . , |l |} such that µ(i) = j iff args(l)(i) = args(l )(j) and args(l)(i) ∈ Var . We say that a path links to a literal l if information flows along the rules to l. This can be formalized by posing constraints on the mapping obtained by combining horizontal and vertical maps along the path. Formally, given a literal l and a mapping ν : N → N, a directed path pr 1 )-vertical map, and µ is the horizontal map connecting body(r j+1 , i j+1 ) with l.
Similarly, a directed path pr 1 . .•µ −1 n−1 satisfies µ(k) = ν(k) for all k for which ν(k) is defined, where µ h is the (r h , body(r h , i h ))-vertical map, for j < h ≤ n − 1, and µ is the (r j , l)vertical map. A path P links to a predicate symbol a iff there is an atom a(x) such that P links to a(x).
Example VI.2. The horizontal map connecting A(x) and D(x) in r a , i.e., the (r a , A(x), D(x))-horizontal map, is {1 → 1}. The horizontal map connecting A(x) and E(x) in r b is {1 → 1} as well. Hence, the path A ra,1 −−→ B downward links to D and the path A

B. Acyclic PROBLOG programs
A sufficient condition for tractable inference is that p's ground graph is a forest of poly-trees. This requires that p's ground graph neither contains directed nor undirected cycles, or, equivalently, the undirected version of p's ground graph is acyclic. To illustrate, the ground graph in Figure 7 is a poly-tree. The key insight here is that a cycle among ground atoms is caused by a (directed or undirected) cycle among p's predicate symbols. In a nutshell, acyclicity requires that all possible cycles in graph(p) are guarded. This ensures that cycles in graph(p) do not lead to cycles in the ground graph. Additionally, acyclicity requires that programs are negationguarded. This ensures that the relaxed grounding and the ground graph are well-defined. In the following, let p be a (Σ, dom)-PROBLOG program. Annotations. Annotations represent properties of the relations induced by the program p, and they are syntactically derived by analysing p's ground atoms and rules.
Let a, a ∈ Σ be two predicate symbols such that |a| = |a |. A disjointness annotation DIS (a, a ) represents that the relations induced by a and a (given p's relaxed grounding) are disjoint. We say that DIS (a, a ) can be derived from p iff no rules in p contain a or a in their heads, and there is no v ∈ dom |a| where both a(v) and a (v) appear as (possibly probabilistic) ground atoms in p. Hence, the relations induced by a and a are disjoint.
Let n ∈ N and A ⊆ Σ be a set of predicate symbols such that |a| = 2n for all a ∈ A. An ordering annotation ORD(A) represents that the transitive closure of the union of the relations induced by predicates in A given p's relaxed grounding is a strict partial order over dom n . The annotation ORD(A) can be derived from the program p iff there is no rule r ∈ p that contains any of the predicates in A in its head and the transitive closure of a∈A {((v 1 , . . . , v n ), (v n+1 , . . . , v 2n )) | ∃k. k::a(v 1 , . . . , v 2n ) ∈ p} is a strict partial order over dom n . Hence, the closure of the relation a∈A {((v 1 , . . . , v n ), (v n+1 , . . . , v 2n )) | a(v 1 , . . . , v 2n ) ∈ rg(p)} induced by the relaxed grounding is a strict partial order.
Let a ∈ Σ be a predicate symbol and K ⊆ {1, . . . , |a|}. A uniqueness annotation UNQ(a, K) represents that the attributes in K are a primary key for the relation induced by a given the relaxed grounding. We say that UNQ(a, K) can be derived from a program p iff no rule contains a in its head and for all v, v ∈ dom |a| , if (1) v(i) = v (i) for all i ∈ K, and (2) there are k and k such k::a(v) ∈ p and k ::a(v ) ∈ p, A Σ-template T is a set of annotations. In Appendix B, we relax our syntactic rules for deriving annotations. Unsafe structures. An unsafe structure models a part of the dependency graph that may introduce cycles in the ground graph. We define directed and undirected unsafe structures which may respectively introduce directed and undirected cycles in the ground graph.
A directed unsafe structure in graph(p) is a directed cycle C in graph(p). We say that a directed unsafe structure C covers a directed cycle C iff C is equivalent to C .
An undirected unsafe structure in graph(p) is quadruple and D 3 are directed paths whereas U is an undirected path, (2) D 1 and D 2 start from the same node, (3) D 2 and D 3 end in the same node, and Connected Rules. A connected rule r ensures that a grounding of r is fully determined either by the assignment to the head's variables or to the variables of any literal in r's body. Formally, a strongly connected rule r guarantees that for any two groundings gr , gr of r, if head (gr ) = head (gr ), then gr = gr . In contrast, a weakly connected rule r guarantees that for any two groundings gr , gr of r, if body(gr , i) = body(gr , i) for some i, then gr = gr . This is done by exploiting uniqueness annotations and the rule's structure.
Before formalizing connected rules, we introduce join trees. A join tree represents how multiple predicate symbols in a rule share variables. In the following, let r be a rule and T be a template. A join tree for a rule r is a rooted labelled tree (N, E, root, λ), where N ⊆ body(r), E is a set of edges (i.e., unordered pairs over N 2 ), root ∈ N is the tree's root, and λ is the labelling function. Moreover, we require that for all n, n ∈ N , if n = n and (n, n ) ∈ E, then λ(n, n ) = vars(n)∩vars(n ) and λ(n, n ) = ∅. A join tree (N, E, root, λ) covers a literal l iff l ∈ N . Given a join tree J = (N, E, root, λ) and a node n ∈ N , the support of n, denoted support(n), is the set vars(head (r)) ∪ {x | (x = c) ∈ cstr (r) ∧ c ∈ dom} ∪ {vars(n ) | n ∈ anc(J, n)}, where anc(J, n) is the set of n's ancestors in J, i.e., the set of all nodes (different from n) on the path from root to n. A join tree J = (N, E, root, λ) is T -strongly connected iff for all positive literals l ∈ N , there is a set K ⊆ {i | x = args(l) ∧ x(i) ∈ support(l)} such that UNQ(pred (l), K) ∈ T and for all negative literals l ∈ N , vars(l) ⊆ support(l). In contrast, a join tree (N, We now formalize strongly and weakly connected rules. A rule r is T -strongly connected iff there exist T -strongly connected join trees J 1 , . . . , J n that cover all literals in r's body. This guarantees that for any two groundings gr , gr of r, if head (gr ) = head (gr ), then gr = gr .
Given a rule r, a set of literals L, and a template T , a literal (2) there is a positive literal a(x) ∈ L and an annotation UNQ(a, K) ∈ T such that {x(i) | i ∈ K} ⊆ vars(l). A rule r is weakly connected for T iff there exists a T -weakly connected join tree J = (N, E, root, λ) such that N ⊆ body + (r), and all literals in body(r) \ N are (r, T , N )-strictly guarded. This guarantees that for any two groundings gr , gr of r, if body(gr , i) = body(gr , i) for some i, then gr = gr .
is T -strongly connected. Indeed, the join tree having O(x, y) as root and B(x) and ¬F (x) as leaves is such that (1)  is T -weakly connected and the literals B(x) and ¬F (x) are strictly guarded. Note that the rules r a and r b are trivially both strongly and weakly connected.
Guarded undirected structures. Guarded undirected structures ensure that undirected cycles in the dependency graph do not correspond to undirected cycles in the ground graph by exploiting disjointness annotations. Formally, an undirected unsafe structure A pair of non-empty paths (P 1 , P 2 ) sharing the same initial node a is T -head guarded iff (1) if P 1 = P 2 , all rules in P 1 are weakly connected for T , or (2) if P 1 = P 2 , there is an annotation DIS (pr , pr ) ∈ T , a set K ⊆ {1, . . . , |a|}, and a bijection ν : K → {1, . . . , |pr |} such that P 1 ν-downward links to pr and P 2 ν-downward links to pr . Given two ground paths P 1 and P 2 corresponding to P 1 and P 2 , the first condition ensures that P 1 = P 2 whereas the second ensures that P 1 or P 2 are not in the ground graph.
Example VI.6. The only non-trivially guarded undirected cycle in the graph from Figure 6 is the one represented by the undirected unsafe structure A ra,1 E). Indeed, for the same ground atom A(v), for some v ∈ {1, 2, 3}, only one of r a and r b can be applied since D and E are disjoint.
Guarded directed structures. Guarded directed structures exploit ordering annotations to ensure that directed cycles in the dependency graph do not correspond to directed cycles among ground atoms. A directed unsafe structure pr 1 Acyclic Programs. Let p be a negation-guarded program and T be the template containing all annotations that can be derived from p. We say that p is acyclic iff (a) for all undirected cycles U in graph(p) that are not directed cycles, there is a T -guarded undirected unsafe structure that covers U , and (b) for all directed cycles C in graph(p), there is a Tguarded directed unsafe structure that covers C. This ensures the absence of cycles in the ground graph.
Proposition VI.1. Let p be a PROBLOG program. If p is acyclic, then the ground graph of p is a forest of poly-trees.
Example VI.8. The program p from Example VI.1 is acyclic. This is reflected in the ground graph in Figure 7. The program q = p ∪ {E(1)}, however, is not acyclic: we cannot derive DIS (D, E) from q and the undirected unsafe structure A ra,1 is not guarded. As expected, q's ground graph contains an undirected cycle between A(1) and B(1), as shown in Figure 8.  Expressiveness. Acyclicity trades off the programs expressible in PROBLOG for a tractable inference procedure. Acyclic programs, nevertheless, can encode many relevant probabilistic models.
Proposition VI.2. Any forest of poly-tree BNs can be represented as an acyclic PROBLOG program.
To clarify this proposition's scope, observe that poly-tree BNs are one of the few classes of BNs with tractable inference procedures. From Proposition VI.2, it follows that a large class of probabilistic models with tractable inference can be represented as acyclic programs. This supports our thesis that our syntactic constraints are not overly restrictive. In Appendix B, we relax acyclicity to support a limited form of annotated disjunctions and rules sharing a part of their bodies, which are needed to encode the example from §V and for Proposition VI.2. We also provide all the proofs.

C. Inference Engine
Our inference algorithm for acyclic PROBLOG programs consists of three steps: (1) we compute the relaxed grounding of p (cf. §VI-A), (2) we compile the relaxed grounding into a Bayesian Network (BN), and (3) we perform the inference using standard algorithms for poly-tree Bayesian Networks [47]. Encoding as BNs. We compile the relaxed grounding rg(p) into the BN bn(p). The boolean random variables in bn(p) are as follows: (a) for each atom a in rg(p) and ground literal a or ¬a occurring in any gr ∈ r∈p rg(p, r), there is a random variable X[a], (b) for each rule r ∈ p and each ground atom a such that there is gr ∈ rg(p, r) satisfying a = head (gr ), there is a random variable X[r, a], and (c) for each rule r ∈ p, each ground atom a, and each ground rule gr ∈ rg(p, r) such that a = head (gr ), there is a random variable X[r, gr , a].
The edges in bn(p) are as follows: (a) for each ground atom a, rule r, and ground rule gr , there is an edge from X[r, gr , a] to X[r, a] and an edge from X[r, a] to X[a], and (b) for each ground atoms a and b, rule r, and ground rule gr , there is an Finally, the Conditional Probability Tables (CPTs) of the variables in bn(p) are as follows. The CPT of variables of the form X[a] and X[r, a] is just the OR of the values of their parents, i.e., the value is with probability 1 iff at least one of the parents has value . For variables of the form X[r, gr , a] such that body(r) = ∅, then the variable's CPT encode the semantics of the rule r, i.e., the value of X[r, gr , a] is with probability 1 iff all positive literals have value and all negative literals have value ⊥. In contrast, for variables of the form X[r, gr , a] such that body(r) = ∅, then the variable has value with probability v and ⊥ with probability 1 − v, where r is of the form v::a (if r = a then v = 1).
To ensure that the size of the CPT of variables of the form X[r, a] is independent of the size of the relaxed grounding, instead of directly connecting variables of the form X[r, gr , a] with X[r, a], we construct a binary tree of auxiliary variables where the leaves are all variables of the form X[r, gr , a] and the root is the variable X[r, a]. Figure 9 depicts a portion of the BN for the program in Example VI.1. Complexity. We now introduce the main result of this section.
Theorem VI.1. The data complexity of inference for acyclic PROBLOG programs is PTIME.
This follows from (1) the relaxed grounding and the encoding can be computed in PTIME in terms of data complexity, (2) the encoding ensures that, for acyclic programs, the resulting Bayesian Network is a forest of poly-trees, and (3) inference algorithms for poly-tree BNs [47] run in polynomial time in the BN's size. In Appendix B, we extend our encoding to handle additional features such as annotated disjunctions, and we prove its correctness and complexity.

VII. ANGERONA
ANGERONA is a DBIC mechanism that provably secures databases against probabilistic inferences. ANGERONA is Algorithm 1: ANGERONA Enforcement Algorithm. Input: A system state s = db, U, P , a history h, an action u, q , a system configuration C, and a C-ATKLOG model ATK .
parametrized by an ATKLOG model representing the attacker's capabilities and it leverages PROBLOG's inference capabilities.

A. Checking Query Security
Algorithm 1 presents ANGERONA. It takes as input a system state s = db, U, P , a history h, the current query q issued by the user u, a system configuration C, and an ATKLOG model ATK formalizing the users' beliefs. ANGERONA checks whether disclosing the result of the current query q may violate any secrets in secrets(P, u). If this is the case, the algorithm concludes that q's execution would be insecure and returns ⊥. Otherwise, it returns and authorizes q's execution. Note that once we fix a configuration C and an ATKLOG model ATK , ANGERONA is a C-PDP as defined in §IV-C.
To check whether a query q may violate a secret u, ψ, l ∈ secrets(P, u), ANGERONA first checks whether the secret has been already violated. If this is not the case, ANGERONA checks whether disclosing q violates any secret. This requires checking that u's belief about the secret ψ stays below the threshold independently of the result of the query q; hence, we must ensure that u's belief is below the threshold both in case the query q holds in the actual database and in case q does not hold (this ensures that the access control decision itself does not leak information). ANGERONA, therefore, first checks whether there exists at least one possible database state where q is satisfied given h, using the procedure pox . If this is the case, the algorithm extends the current history h with the new event recording that the query q is authorized and its result is and it checks whether u's belief about ψ is still below the corresponding threshold once q's result is disclosed, using the secure procedure. Afterwards, ANGERONA checks whether there exists at least a possible database state where q is not satisfied given h, it extends the current history h with another event representing that the query q does not hold, and it checks again whether disclosing that q does not hold in the current database state violates the secret. Note that checking whether there is a database state where q is (or is not) satisfied is essential to ensure that the conditioning that happens in the secure procedure is well-defined, i.e., the set of states we condition on has non-zero probability.
ANGERONA uses the secure subroutine to determine whether a secret's confidentiality is violated. This subroutine takes as input a system configuration, an ATKLOG model ATK , a history h, and a secret u, ψ, l . It first computes the set knowledge(h, u) containing all the authorized queries Afterwards, it generates a PROBLOG program p by extending ATK (u) with additional rules. In more detail, it translates each relational calculus sentence φ ∈ knowledge(h, u) to an equivalent set of PROBLOG rules PL(φ). The translation PL(φ) is standard [2]. For example, given a query . . , h 5 are fresh predicate symbols. We denote by head (φ) the unique predicate symbol associated with the sentence φ by the translation PL(φ). In our example, head (φ) is the fresh predicate symbol h 5 . The algorithm then conditions the initial probability distribution ATK (u) based on the sentences in knowledge(h, u). This is done using evidence statements, which are special PROBLOG statements of the form evidence(a, v), where a is a ground atom and v is either true or false; see Appendix A. For each sentence φ ∈ knowledge(h, u), the program p contains a statement evidence(head (φ), true). Finally, the algorithm translates ψ to a set of logic programming rules and checks whether ψ's probability is below the threshold l.
The pox subroutine takes as input a system configuration, an ATKLOG model ATK , a history h, and a query u, ψ . It determines whether there is a database db that satisfies ψ and complies with the history h| u . Internally, the routine again constructs a PROBLOG program starting from ATK , knowledge(h, u), and ψ. Afterwards, it uses the program to check whether the probability of ψ given h| u is greater than 0.
Given a run s, h and a user u, the secure and pox subroutines condition u's initial beliefs based on the sentences in knowledge(h, u), instead of using the set r ∼u as in the ATKLOG semantics. The key insight is that, as we prove in Appendix C, the set of possible database states defined by the sentences in knowledge(h, u) is equivalent to r ∼u , which contains all database states derivable from the runs r ∼ u r. This allows us to use PROBLOG to implement ATKLOG's semantics without explicitly computing r ∼u .
Example VII.1. Let ATK be the attacker model in Example IV.4, u be the user Mallory, the database state be s {A,B,C} , where Alice, Bob, and Carl have cancer, and the policy P be the one from Example IV.2. Furthermore, let q 1 , . . . , q 4 be the queries issued by Mallory in Example IV.3. ANGERONA permits the execution of the first two queries since they do not violate the policy. In contrast, it denies the execution of the last two queries as they leak sensitive information.
Confidentiality. As we prove in Appendix C, ANGERONA provides the desired security guarantees for any ATKLOGattacker. Namely, it authorizes only those queries whose disclosure does not increase an attacker's beliefs in the secrets above the corresponding thresholds. ANGERONA also provides precise completeness guarantees: it authorizes all secrecypreserving queries. Informally, a query u, q is secrecypreserving given a run r and a secret u, ψ, l iff disclosing the result of u, q in any run r ∼ u r does not violate the secret.
Theorem VII.1. Let a system configuration C and a C-ATKLOG model ATK be given, and let ANGERONA be the C-PDP f . ANGERONA provides data confidentiality with respect to C and λu ∈ U. ATK (u) D , and it authorizes all secrecypreserving queries.
Complexity. ANGERONA's complexity is dominated by the complexity of inference. We focus our analysis only on data complexity, i.e., the complexity when only the ground atoms in the PROBLOG programs are part of the input while everything else is fixed. A literal query is a query consisting either of a ground atom a(c) or its negation ¬a(c). We call an ATKLOG model acyclic if all belief programs in it are acyclic. Furthermore, a literal secret is a secret U, φ, l such that φ is a literal query. We prove in Appendix C that for acyclic ATKLOG models, literal queries, and literal secrets, the PROBLOG programs produced by the secure and pox subroutines are acyclic. We can therefore use our dedicated inference engine from §VI to reason about them. Hence, ANGERONA can be used to protect databases in PTIME in terms of data complexity. Literal queries are expressive enough to formulate queries about the database content such as "does Alice have cancer?".
Theorem VII.2. For all acyclic ATKLOG attackers, for all literal queries q, for all runs r whose histories contain only literal queries and contain only secrets expressed using literal queries, ANGERONA's data complexity is PTIME.
Discussion. Our tractability guarantees apply only to acyclic ATKLOG models, literal queries, and literal secrets. Nevertheless, ANGERONA can still handle relevant problems of interest. As stated in §VI, acyclic models are as expressive as poly-tree Bayesian Networks, one of the few classes of Bayesian Networks with tractable inference. Hence, for many probabilistic models that cannot be represented as acyclic ATKLOG models, exact probabilistic inference is intractable. Literal queries are expressive enough to state simple facts about the database content. More complex (non-literal) queries can be simulated using (possibly large) sequences of literal queries. Similarly, policies with non-literal secrets can be implemented as sets of literal secrets, and the Boole-Fréchet inequalities [38] can be used to derive the desired thresholds. In both cases, however, our completeness guarantees hold only for the resulting literal queries, not for the original ones.
Finally, whenever our tractability constraints are violated, ANGERONA can still be used by directly using PROBLOG's inference capabilities. In this case, one would retain the security and completeness guarantees (Theorem VII.1) but lose the tractability guarantees (Theorem VII.2).

B. Implementation and Empirical Evaluation
To evaluate the feasibility of our approach in practice, we implemented a prototype of ANGERONA, available at [36]. The prototype implements our dedicated inference algorithm for acyclic PROBLOG programs ( §VI), which computes the relaxed grounding of the input program p, constructs the Bayesian Networks BN , and performs the inference over BN using belief propagation [47]. For inference over BN , we rely on the GRRM library [66]. Observe that evidence statements in PROBLOG are encoded by fixing the values of the corresponding random variables in the BN. Note also that computing the relaxed grounding of p takes polynomial time in terms of data complexity, where the exponent is determined by p's rules. A key optimization is to pre-compute the relaxed grounding and construct BN off-line. This avoids grounding p and constructing the (same) Bayesian Network for each query. In our experiments we measure this time separately.
We use our prototype to study ANGERONA's efficiency and scalability. We run our experiments on a PC with an Intel i7 processor and 32GB of RAM. For our experiments, we consider the database schema from §IV. For the belief programs, we use the PROBLOG program given in §V, which can be encoded as an acyclic program when the parent-child relation is a poly-tree. We evaluate ANGERONA's efficiency and scalability in terms of the number of ground atoms in the belief programs. We generate synthetic belief programs containing 1,000 to 100,000 patients and for each of these instances, we generate 100 random queries of the form R(t), where R is a predicate symbol and t is a tuple. For each instance and sequence of queries, we check the security of each query with our prototype, against a policy containing 100 randomly generated secrets specified as literal queries. Figure 10 reports the execution times for our case study. Once the BN is generated, ANGERONA takes under 300 milliseconds, even for our larger examples, to check a query's security. During the initialization phase of our dedicated inference engine, we ground the original PROBLOG program and translate it into a BN. Most of the time is spent in the grounding process, whose data complexity is polynomial, where the polynomial's degree is determined by the number of free variables in the belief program. Our prototype uses a naive bottom-up grounding technique, and for our larger examples the initialization times is less than 2.5 minutes. We remark, however, that the initialization is performed just once per belief program. Furthermore, it can be done offline and its performance can be greatly improved by naive parallelization.

VIII. RELATED WORK
Database Inference Control. Existing DBIC approaches protect databases (either at design time [54], [55] or at runtime [14], [15], [39]) only against restricted classes of probabilistic dependencies, e.g., those arising from functional and multi-valued dependencies. ATKLOG, instead, supports arbitrary probabilistic dependencies, and even our acyclic fragment can express probabilistic dependencies that are not supported by [14], [15], [39], [54], [55]. Weise [71] proposes a DBIC framework, based on possibilistic logic, that formalizes secrets as sentences and expresses policies by associating bounds to secrets. Possibility theory differs from probability theory, which results in subtle differences. For instance, there is no widely accepted definition of conditioning for possibility distributions, cf. [11]. Thus, the probabilistic model from §II cannot be encoded in Weise's framework [71].
Statistical databases store information associated to different individuals and support queries that return statistical information about an entire population [16]. DBIC solutions for statistical databases [3], [16], [22]- [24] prevent leakages of information about single individuals while allowing the execution of statistical queries. These approaches rely on various techniques, such as perturbating the original data, synthetically generating data, or restricting the data on which the queries are executed. Instead, we protect specific secrets in the presence of probabilistic data dependencies and we return the original query result, without modifications, if it is secure.
Differential Privacy. Differential Privacy [25], [26] is widely used for privacy-preserving data analysis. Systems such as ProPer [27] or PINQ [53] provide users with automated ways to perform differentially private computations. A differentially private computation guarantees that the presence (or absence) of an individual's data in the input data set affects the probability of the computation's result only in limited way, i.e., by at most a factor e where is a parameter controlling the privacyutility trade-off. While differential privacy does not make any assumption about the attacker's beliefs, we assume that the attacker's belief is known and we guarantee that for all secrets in the policy, no user can increase his beliefs, as specified in the attacker model, over the corresponding thresholds by interacting with the system. Information Flow Control. Quantified Information Flow [6], [17], [48], [50] aims at quantifying the amount of information leaked by a program. Instead of measuring the amount of leaked information, we focus on restricting the information that an attacker may obtain about a set of given secrets.
Non-interference has been extended to consider probabilities [5], [58], [70] for concurrent programs. Our security notion, instead, allows those leaks that do not increase an attacker's beliefs in a secret above the threshold, and it can be seen as a probabilistic extension of opacity [60], which allows any leak except leaking whether the secret holds.
Mardziel et al. [51] present a general DBIC architecture, where users' beliefs are expressed as probabilistic programs, security requirements as threshold on these beliefs, and the beliefs are updated in response to the system's behaviour. Our work directly builds on top of this architecture. However, instead of using an imperative probabilistic language, we formalize beliefs using probabilistic logic programming, which provides a natural and expressive language for formalizing dependencies arising in the database setting, e.g., functional and multi-valued dependencies, as well as common probabilistic models, like Bayesian Networks.
Mardziel et al. [51] also propose a DBIC mechanism based on abstract interpretation. They do not provide any precise complexity bound for their mechanism. Their algorithm's complexity class, however, appears to be intractable, since they use a probabilistic extension of the polyhedra abstract domain, whose asymptotic complexity is exponential in the number of program variables [62]. In contrast, ANGERONA exploits our inference engine for acyclic programs to secure databases against a practically relevant class of probabilistic inferences, and it provides precise tractability and completeness guarantees.
We now compare (unrestricted) ATKLOG with the imperative probabilistic language used in [51]. ATKLOG allows one to concisely encode probabilistic properties specifying relations between tuples in the database. For instance, a property like "the probability of A(x) is 1 /2 n , where n is the number of tuples (x, y) in B" can be encoded as 1 /2::A(x) ← B(x, y). Encoding this property as an imperative program is more complex; it requires a for statement to iterate over all variables representing tuples in B and an if statement to filter the tuples. In contrast to [51], ATKLOG provides limited support for numerical constraints (as we support only finite domains).
Mardziel et al. [51] formalize queries as imperative probabilistic programs. They can, therefore, also model probabilistic queries or the use of randomization to limit disclosure. While all these features are supported by ATKLOG, our goal is to protect databases from attackers that use standard query lan-guages like SQL. Hence, we formalize queries using relational calculus and ignore probabilistic queries. Similarly to [51], our approach can be extended to handle some uncertainty on the attackers' capabilities. In particular, we can associate to each user a finite number of possible beliefs, instead of a single one. However, like [51], we cannot handle infinitely many alternative beliefs. Probabilistic Programming. Probabilistic programming is an active area of research [35]. Here, we position PROBLOG with respect to expressiveness and inference. Similarly to [33], [51], PROBLOG can express only discrete probability distributions, and it is less expressive than languages supporting continuous distributions [32], [34], [61]. Current exact inference algorithms for probabilistic programs are based on program analysis techniques, such as symbolic execution [32], [61] or abstract interpretation [51]. In this respect, we present syntactic criteria that ensure tractable inference for PROBLOG. Sampson et al. [59] symbolically execute probabilistic programs and translate them to BNs to verify probabilistic assertions. In contrast, we translate PROBLOG programs to BNs to perform exact inference and our translation is tailored to work together with our acyclicity constraints to allow tractable inference.

IX. CONCLUSION
Effectively securing databases that store data with probabilistic dependencies requires an expressive language to capture the dependencies and a tractable enforcement mechanism. To address these requirements, we developed ATKLOG, a formal language providing an expressive and concise way to represent attackers' beliefs while interacting with the system. We leveraged this to design ANGERONA, a provably secure DBIC mechanism that prevents the leakage of sensitive information in the presence of probabilistic dependencies. ANGERONA is based on a dedicated inference engine for a fragment of PROBLOG where exact inference is tractable.
We see these results as providing a foundation for building practical protection mechanisms, which include probabilistic dependencies, as part of real-world database systems. As future work, we plan to extend our framework to dynamic settings where the database and the policy change. We also intend to explore different fragments of PROBLOG and relational calculus for which exact inference is practical APPENDICES Here, we provide additional details about numerous aspects of the paper, such as acyclic PROBLOG programs and ANGERONA. We also provide complete proofs of all our results. Structure. Appendix A reviews PROBLOG's syntax and semantics. In Appendix B, we formalize acyclicity for PROBLOG programs, we present our encoding from acyclic programs to poly-tree Bayesian Networks, we prove the correctness of this encoding, and we give complexity results for inference for acyclic PROBLOG programs. Finally, Appendix C contains additional details about ANGERONA as well as all the security and complexity proofs.

APPENDIX A PROBLOG
Here, we provide a formal account of PROBLOG, which follows [20], [21], [31]. In addition to PROBLOG's semantics, we present here again some (revised) aspects of PROBLOG's syntax, which we introduced in §V. As mentioned in §V, we restrict ourselves to the function-free fragment of PROBLOG. Syntax. As introduced in §V, a (Σ, dom)-probabilistic atom is an atom a ∈ A Σ,dom annotated with a value 0 ≤ v ≤ 1, denoted v::a. If v = 1, then we write a(c) instead of 1::a(c). A (Σ, dom)-PROBLOG program is a finite set of ground probabilistic (Σ, dom)-atoms and (Σ, dom)-rules. Note that ground atoms a ∈ A Σ,dom are represented as 1::a. Observe also that rules do not involve probabilistic atoms (as formalized in §V). This is without loss of generality: as we show below probabilistic rules and annotated disjunctions can be represented using only probabilistic atoms and nonprobabilistic rules. We denote by prob(p) the set of all probabilistic ground atoms v::a in p, i.e., prob(p) := {v::a ∈ p | 0 ≤ v ≤ 1 ∧ a ∈ A Σ,dom }, and by rules(p) the nonprobabilistic rules in p, i.e., rules(p) := p\prob(p). As already stated in §V, we consider only programs p that do not contain negative cycles in the rules. Finally, we say that a PROBLOG program p is a logic program iff v = 1 for all v::a ∈ prob(p), i.e., p does not contain probabilistic atoms. Semantics. Given a (Σ, dom)-PROBLOG program p, a pgrounded instance is a PROBLOG program A ∪ R, where the set of ground atoms A is a subset of {a | v::a ∈ prob(p)} and R = rules(p). Informally, a grounded instance of p is one of the logic programs that can be obtained by selecting some of the probabilistic atoms in p and keeping all rules in p. A p-probabilistic assignment is a total function associating to each probabilistic atom v::a in prob(p) a value in { , ⊥}. We denote by A(p) the set of all p-probabilistic assignments. The probability of a p-probabilistic assignment f is prob(f ) = Π v::a∈prob(p) Π f (v::a)= v · Π f (v::a)=⊥ (1 − v) . Given a p-probabilistic assignment f , instance(p, f ) denotes the p-grounded instance {a | ∃v. f (v::a) = } ∪ rules(p). Finally, given a p-grounded instance p , WFM (p ) denotes the well-founded model associated with the logic program p , as defined by standard logic programming semantics [2].
The semantics of a (Σ, dom)-PROBLOG program p is defined as a probability distribution over all possible pgrounded instances. Note that PROBLOG's semantics relies on the closed world assumption, namely every fact that is not in a given model is considered false. The semantics of p, denoted by p , is as follows: We remark that a (Σ, dom)-PROBLOG program p implicitly defines a probability distribution over (Σ, dom)-structures. Indeed, the probability of a given (Σ, dom)-structure s is the sum of the probabilities of all p-grounded instances whose well-founded model is s. With a slight abuse of notation, we extend the semantics of p to (Σ, dom)-structures and ground atoms as follows: p (s) = f ∈M(p,s) prob(f ), where s is a (Σ, dom)-structure and M(p, s) is the set of all assignments f such that WFM (instance(p, f )) = s. Finally, p's semantics can be lifted to sentences as follows: Evidence. PROBLOG supports expressing evidence inside programs [20]. To express evidence, i.e., to condition a distribution on some event, we use statements of the form evidence (a, v), where a is a ground atom and v ∈ {true, false}. Let p be a (Σ, dom)-PROBLOG program p with evidence evidence (a 1 , v 1 ), . . . , evidence(a n , v n ), and p be the program without the evidence statements. Furthermore, let POX (p ) be the set of all (Σ, dom)-structures s complying with the evidence, i.e., the set of all states s such that a i holds in s iff v i = true. Then, p (s), for a (Σ, dom)-structure Syntactic Sugar. Following [20], [21], [31], we extend PROBLOG programs with two additional constructs: annotated disjunctions and probabilistic rules. As shown in [20], these constructs are just syntactic sugar. A probabilistic rule is a PROBLOG rule where the head is a probabilistic atom. The probabilistic rule v::h ← l 1 , . . . , l n can be encoded using the additional probabilistic atoms v::sw( ) and the rule h ← l 1 , . . . , l n , sw(x), where sw is a fresh predicate symbol, x is the tuple containing the variables in vars(h) ∪ 1≤i≤n vars(l i ), and v::sw( ) is a shorthand representing the fact that there is a probabilistic atom v::sw(t) for each tuple t ∈ dom |x| .
An annotated disjunction v 1 ::a 1 ; . . . ; v n ::a n , where a 1 , . . . , a n are ground atoms and 1≤i≤n v i ≤ 1, denotes that a 1 , . . . , a n are mutually exclusive probabilistic events happening with probabilities v 1 , . . . , v n . It can be encoded as: . . . p n ::sw n ( ) . Probabilistic rules can be easily extended to support annotated disjunctions in their heads. The probability associated to each (Σ, dom)-structure by the program p is shown in the following table. The empty structure has probability 3 /32. The only grounded instance whose well-formed model is the empty database is the instance i 1 that does not contain grounded atoms. Its probability is 3 /32 because the probability that T (a) is not in i 1 is 3 /4, the probability that T (b) is not in i 1 is 1 /2, and the probability that neither W (a) nor W (b) are in i 1 is 1 /4 and all these events are independent.
The probability of some structures is determined by more than one grounded instance. For example, the probability of the structure s where s(T ) = {a, b} and s(W ) = {a} is 5 /64. There are two grounded instances i 2 and i 3 whose wellfounded model is s. The instance i 2 has probability 1 /16 and it consists of the atoms T (b), W (a), sw (a) and the rule T (x) ← W (x), sw (x), whereas the instance i 3 has probability 1 /64 and it consists of the atoms T (a), T (b), W (a) and the rule T (x) ← W (x), sw (x). Note that before computing the ground instances, we translated probabilistic rules and annotated disjunctions into standard PROBLOG rules.

APPENDIX B ACYCLIC PROBLOG PROGRAMS
The belief programs in ATKLOG are based on PROBLOG, which is a very expressive probabilistic language and it can be used to encode a wide range of probabilistic models. As a result, performing exact inference in PROBLOG is intractable in general, i.e., it is #P -hard in terms of data complexity.
We identify acyclic PROBLOG programs, a restricted class of PROBLOG programs where exact inference can be done efficiently, in linear time in terms of data complexity.
We first introduce acyclic programs. Afterwards, we introduce relaxed acyclic programs, a generalization of acyclic programs, and we provide an encoding of relaxed acyclic programs as a Bayesian Network. Observe that here we state again (sometimes with some generalizations) some of the concepts we introduced in the main paper. Note also that in the main paper we do not distinguish between acyclic programs and relaxed acyclic programs.

A. Acyclic Programs
Here, we define acyclic PROBLOG programs. Intuitively, an acyclic program is a PROBLOG program whose probability distribution can be represented using a poly-tree Bayesian Network. While inference for general Bayesian Networks is intractable, i.e., NP -hard, inference for poly-tree Bayesian Networks can be done in linear time in the size of the corresponding Bayesian Network.
1) Acyclic PROBLOG Programs: In the following, let Σ be a first-order signature, dom be a finite domain, and p be a (Σ, dom)-program. Without loss of generality, in the following we assume that (1) inside rules (not ground atoms), constants are used just inside equality and inequality atoms, i.e., instead of B(x, 7) ← D(x, y) we consider only the equivalent rule B(x, k) ← D(x, y), k = 7, and (2) there are no distinct v 1 and v 2 such that v 1 ::a(c) ∈ p and v 2 ::a(c) ∈ p (this is without loss of generality since multiple occurrences of the same ground atom with different probabilities can be represented as a single ground atom an adjusted probability). Observe that in the following we re-define, extend, or make more precise the definitions from §VI.   −−−−−−→ pr n in graph(p), we denote by start(P ) the predicate symbol pr 1 and by end (P ) the predicate symbol pr n . We say that a directed cycle C is simple iff (1) each edge occurs at most once in C, and (2) there is a predicate symbol pr such that pr occurs twice in C and for all pr = pr , pr occurs at most once in C. Undirected Paths and Cycles. A directed path P 1 in graph(p) is connected with P 2 iff end (P 1 ) = end (P 2 ), start(P 1 ) = start(P 2 ), or end (P 1 ) = start(P 2 ). An undirected path in graph(p) is a sequence of directed paths P 1 , . . . , P n such that, for all 1 ≤ i < n, P i is connected with P i+1 . An undirected cycle in graph(p) is a sequence of directed paths P 1 , . . . , P n such that (1) P 1 , . . . , P n is an undirected path and (2) P n is connected with P 1 . Note that a directed path (respectively cycle) is also an undirected path (respectively cycle). We say that two (directed or undirected) cycles are equivalent iff they are the same cycle.
Directed Unsafe Structures. A directed unsafe structure in graph(p) is a directed cycle C in graph(p). A directed unsafe structure C covers a directed cycle C iff C is equivalent to C . Deriving Ordering Annotations. A Σ-ordering annotation is ORD(A), where A ⊆ Σ and there is a k ∈ N such that for all a ∈ A, |a| = 2k. Let be a well-founded partial order over 2 Σ . We say that the ordering annotation ORD(A) can be derived from the program p given , written p, |= ORD(A), iff one of the following conditions hold: 1) For all pr ∈ A, there is no rule r in p such that pred (head (r)) = pr and body(r) = ∅, there is no pr ∈ Σ such that pr ≺ pr and p, |= ORD(pr ), and the transitive closure of the relation R = pr ∈A {(c, v) | ∃r ∈ p. ((head (r) = pr(c, v) ∨ ∃v . head (r) = v ::pr(c, v)) ∧ body(r) = ∅) ∧ |c| = |v| = |pr | /2} is strict partial order. 2) There is a set A ⊆ Σ such that (1) A A, (2) p, |= ORD(A ), (3) there is a pr ∈ Σ and a pr ∈ A such that (a) |pr | = |pr |, (b) A = (A \ {pr }) ∪ {pr }, and (c) for all rules r in p such that pred (head (r)) = pr, there are sequences of variables x and y and an i, such that head (r) = pr (x, y), body(r, i) = pr (x, y), and |x| = |y|. A Σ-ordering template O is a set of ordering annotations. We say that p complies with O with respect to iff for all ordering annotations a ∈ O, p, |= a holds. We say that p complies with O iff there exists a well-founded partial order over Σ such that p complies with O with respect to . Intuitively, a program p complies with an ordering template O iff all sets of predicates in O represent strict partial orders in all possible models of p. DIS (a, a ), where a, a ∈ Σ and |a| = |a |. Let be a well-founded partial order over Σ 2 . We say that the disjointness annotation DIS (pr , pr ) can be derived from the program p given , written p, |= DIS (pr , pr ), iff one of the following conditions hold:
Deriving Uniqueness Annotations. A Σ-uniqueness annotation is UNQ(a, K), where a ∈ Σ and K is a non-empty subset of {1, . . . , |a|}. Let be a well-founded order over Σ. We say that the uniqueness annotation UNQ(pr , K) can be derived from p given , written p, |= UNQ(pr , K), iff one of the following conditions hold: 1) There are no rules r ∈ p such that body(r) = ∅ and pred (head (r)) = pr , and there is no pr such that pr ≺ pr , and for all t, v in {c | pr (c) ∈ p ∨ ∃v. v::pr (c) ∈ p}, if t(i) = v(i) for all i ∈ K, then t = v. 2) Both the following conditions hold: a) For each rule r ∈ p such that head (r) = pr (x) and body(r) = ∅, there is a mapping µ associating to each predicate pr ≺ pr a set K such that (a) p, |= UNQ(pr , µ(pr )), and (b) the following hold: V ⊆ l∈bound(head(r),K,body + (r),µ ) vars(l), b) For all rules r 1 , r 2 ∈ p, if r 1 = r 2 , pred (head (r 1 )) = pred (head (r 2 )) = pr , and K = {1, . . . , |pr |}, then there is a value i ∈ K such that args(head (r 1 )) ∈ dom, args(head (r 2 )) ∈ dom, and args(head (r 1 )) = args(head (r 1 )). A Σ-uniqueness template U is a set of uniqueness annotations. We say that p complies with U with respect to iff for all uniqueness annotations a ∈ U, p, |= a holds. We say that p complies with U iff there exists a well-founded partial order over Σ such that p complies with U with respect to . Intuitively, a program complies with a uniqueness template U iff for all predicates pr each set K such that UNQ(pr , K) ∈ U represents a primary key for pr . Propagation Maps. We use propagation maps to track how information flows inside rules. Given a rule r and a literal l ∈ body(r), the (r, l)-vertical map is the mapping µ from {1, . . . , |l|} to {1, . . . , |head (r)|} such that µ(i) = j iff args(l)(i) = args(head (r))(j) and args(l)(i) ∈ Var . Given a rule r and literals l, l in r's body, the (r, l, l )-horizontal map is the mapping µ from {1, . . . , |l|} to {1, . . . , |l |} such that µ(i) = j iff args(l)(i) = args(l )(j) and args(l)(i) ∈ Var .
We say that a path links to a literal l if information flows along the rules to l. This can be formalized by posing constraints on the mapping obtained by combining horizontal and vertical maps along the path. Formally, given a literal l and a mapping ν : N → N, a directed path pr 1 for all k for which ν(k) is defined, where for 1 ≤ h ≤ j, µ h is the vertical map connecting body(r h , i h ) and r h , and µ is the horizontal map connecting body(r j+1 , i j+1 ) with l. Similarly, body(r h , i h ))vertical map, for j < h ≤ n − 1, and µ is the (r j , l)-vertical map. A path P links to a predicate symbol a iff there is an atom a(x) such that P links to a(x). Negation-guarded Programs. A rule r is negationguarded [9] iff for all negative literals l in r, vars(l) ⊆ Join Trees. A join tree represents how multiple predicate symbols in a rule share variables. A join tree for a rule r is a rooted labelled tree (N, E, root, λ), where N ⊆ body(r), E is a set of edges (i.e., unordered pairs over N 2 ), root ∈ N is the tree's root, and λ is the labelling function. Moreover, we require that for all n, n ∈ N , if n = n and (n, n ) ∈ E, then λ(n, n ) = vars(n) ∩ vars(n ) and λ(n, n ) = ∅. A join tree (N, E, root, λ) covers a literal l iff l ∈ N . Given a join tree J = (N, E, root, λ) and a node n ∈ N , the support of n, denoted support(n), is the set vars(head (r)) ∪ {x | (x = c) ∈ cstr (r) ∧ c ∈ dom} ∪ {vars(n ) | n ∈ anc(J, n)}, where anc(J, n) is the set of n's ancestors in J, i.e., the set of all nodes on the path from root to n (if such a path exists). Let U be a uniqueness template. A join tree J = (N, E, root, λ) is U-strongly connected iff for all positive literals l ∈ N , there is a set K ⊆ {i | x = args(l) ∧ x(i) ∈ support(l)} such that UNQ(pred (l), K) ∈ U and for all negative literals l ∈ N , vars(l) ⊆ support(l). In contrast, a join tree (N, E, root, λ) is U-weakly connected iff for all (a(x), a (x )) ∈ E, there are K ⊆ {i | x(i) ∈ L} and K ⊆ {i | x (i) ∈ L} such that UNQ(a, K), UNQ(a , K ) ∈ U, where L = λ(a(x), a (x )). Connected rules. A connected rule r ensure that a grounding of r is fully determined either by the assignment to the head's variables (strongly connected rule) or to the variable of any literal in r's body (weakly connected rule). This is done by exploiting uniqueness annotations and the rule's structure. In the following, let U be a uniqueness template.
We say that a rule r is strongly connected for U iff there exist join trees J 1 , . . . , J n such that (a) the trees cover all literals in body(r), and (b) for each 1 ≤ i ≤ n, J i is strongly connected for U. We call J 1 , . . . , J n a witness for the strong connectivity of r with respect to U. A strongly connected rule r guarantees that for any two groundings r , r of r, if head (r ) = head (r ), then r = r .
Given a rule r, a set of literals L, and a uniqueness template U, we say that a literal l ∈ body(r) is (r, U, L)-strictly guarded iff (1) vars(l) ⊆ l ∈L∩body + (r) vars(l ) ∪ {x | (x = c) ∈ cstr (r) ∧ c ∈ dom}, and (2) there is a positive literal a(x) ∈ L ∩ body + (r) and an annotation UNQ(a, K) ∈ U such that {x(i) | i ∈ K} ⊆ vars(l). We say that a rule r is weakly connected for U iff there exists a join tree J = (N, E, root, λ) such that (a) J is weakly connected for U, (b) N ⊆ body + (r), and (c) all literals in body(r)\N are (r, U, N )-strictly guarded. We call J a witness for the weak connectivity of r with respect to U. A weakly connected rule r guarantees that for any two groundings r , r of r, if body(r , i) = body(r , i) for some i, then r = r .   Head-Guarded Paths. A pair of head-connected non-empty directed paths (P 1 , P 2 ) is (D, U)-head guarded iff one of the following conditions hold: • if P 1 = P 2 , then all rules in P 1 are weakly connected for U, or • if P 1 = P 2 , then there is an annotation DIS (pr , pr ) ∈ D, a set K ⊆ {1, . . . , |a|}, and a bijection ν : K → {1, . . . , |pr |} such that P 1 ν-downward links to pr and P 2 ν-downward links to pr . Given two ground paths P 1 and P 2 corresponding to P 1 and P 2 , the first condition ensures that P 1 = P 2 whereas the second ensures that P 1 or P 2 are not in the ground graph.
Tail-Guarded Paths. A pair of tail-connected non-empty directed paths (P 1 , P 2 ) are (D, U)-tail guarded iff one of the following conditions hold: • if P 1 = P 2 , then all rules in P 1 are strongly connected for U, or • if P 1 = P 2 , there is an annotation DIS (pr , pr ) ∈ D, a set K ⊆ {1, . . . , |a|}, and a bijection ν : K → {1, . . . , |pr |}, such that P 1 ν-upward links to pr and P 2 ν-upward links to pr . 2) Exact Grounding: We now introduce the exact grounding of a PROBLOG program p given a p-probabilistic assignment. The exact grounding encodes the PROBLOG semantics.
Let p be a PROBLOG program and f be a p-probabilistic assignment. Furthermore, let µ be the mapping from predicate symbols in p to N: µ(a) = max t∈paths(p,a) (w (t)), where paths(p, a) is the set of all directed paths that ends in a in p's dependency graph and the weight of each path is We remark that µ is a valid stratification for the program p. From more details about logic programming with stratified negation we refer the reader to [2].
The functions g f (p, j, i), g f (p, j), and g f (p) are defined as follows: ∀l ∈ body + (r). lΘ ∈ g f (p, 0, i − 1)∧ body − (r) = ∅ ∧ µ(pred (head (r))) = 0} Furthermore, the functions g f (p, r, j, i), g f (p, r, j), and g f (p, r) are defined as follows: The fact below follows directly from g f 's definition and the notion of well-founded models for stratified logic programs [2].

3) Relaxed Grounding:
Here we introduce the notion of relaxed grounding. This is a key notion for our acyclicity and correctness proofs and it is also a key component of our compilation from PROBLOG programs to poly-tree Bayesian Networks.
Given a PROBLOG acyclic program p, the relaxed grounding of p is a set M of ground atoms and rules containing all possible ground atoms and rules that can be derived in any ground instance of p. We remark that a relaxed grounding is an over-approximation of the ground atoms and/or rules that could be derived by the ground instances of p.
The fact below follows directly from ground 's definition and the definition of acyclic PROBLOG programs.
Fact B.2. For any acyclic PROBLOG program p and any p-probabilistic assignment f , g f (p) ⊆ ground (p) and g f (p, r) ⊆ ground (p, r).

4) Ground Graphs:
Let Σ be a first-order signature, dom be a finite domain, and p be a (Σ, dom)-acyclic PROBLOG program. The ground graph of p, denoted gg(p), is the directed graph (N, E) defined as follows: • There is one node a(c) in N per literal a(c) or ¬a(c) used in a ground rule r ∈ ground (p, r) for some r ∈ p.
For each rule r ∈ p, ground rule s ∈ ground (p, r), and position 1 ≤ j ≤ |body(r )|, there is a node (r, s, j).
or body(s, j) = ¬b(v). There is an edge from (r, s, j) to a(c) if head (s) = a(c).

5) Proofs about Templates:
Here we prove preliminary results about the semantic relationships enforced by the ordering, disjointness, and uniqueness templates.
Proposition B.1. Let Σ be a first-order signature, dom be a finite domain, p be a (Σ, dom)-PROBLOG program, O be a Σ-ordering template, and be a well-founded partial order over 2 Σ . If p complies with O with respect to and ORD(A) ∈ O, then if pr 1 (a 1 , a 2 ), pr 2 (a 2 , a 3 ), . . . , pr n−1 (a n−1 , a n ) are in ground (p) and {pr 1 , . . . , pr n−1 } ⊆ A, then a 1 = a n .
Proof. Let Σ be a first-order signature, dom be a finite domain, p be a (Σ, dom)-PROBLOG program, O be a Σordering template, and be a well-founded partial order over 2 Σ . We assume that p complies with O with respect to , ORD(A) ∈ O, pr 1 (a 1 , a 2 ), . . . , pr n−1 (a n−1 , a n ) are in ground (p), and {pr 1 , . . . , pr n−1 } ⊆ A. We now prove, by induction over , that the transitive closure of the unions of the relations induced by pr 1 , . . . , pr n−1 over ground (p) is a strict partial order over dom |pr | /2 . From this, it follows that if pr 1 (a 1 , a 2 ), pr 2 (a 2 , a 3 ), . . . , pr n−1 (a n−1 , a n ) are in ground (p), then a 1 = a n .
Base Case. Let A be a set such that there is no A A such that p, |= ORD(A ). From this, ORD(A) ∈ O, and p complies with O with respect to , it follows that (1) for all pr ∈ A, there is no rule r in p such that pred (head (r)) = pr and body(r) = ∅, and (2) the transitive closure of the relation R = pr ∈A {(c, v) | ∃r ∈ p. ((head (r) = pr(c, v) ∨ ∃v . head (r) = v ::pr(c, v)) ∧ body(r) = ∅) ∧ |c| = |v| = |pr | /2} is strict partial order. From this and {(c, v) | ∃pr ∈ A. pr (c, v) ∈ ground (p) ∧ |c| = |v| = |pr | /2} ⊆ R, it follows that the transitive closure of the union of the relations induced by pr over ground (p) is a strict partial order over dom |pr | /2 .

Induction
Step. Assume that the relation induced by any A ≺ A over ground (p) is a strict partial order over dom |pr |/2 if p, |= ORD(A ), where pr is any predicate symbol in A . Without loss of generality, we assume that there is at least one A ≺ A such that p, |= ORD(A ) (otherwise the proof is the same as in the base case). We now prove that also the relation induced by A over ground (p) is a strict partial order over dom |pr | /2 . Let pr , A , pr 1 be such that A = (A \{pr 1 })∪{pr }, A ≺ A, p, |= ORD(A ), and pr 1 ∈ A . Note that the previous values always exist. We now prove that also the relation induced by A over ground (p) is a strict partial order over dom |pr | /2 . Since pr ∈ A, A = (A \ {pr 1 }) ∪ {pr }, pr 1 ∈ A , and ORD(A) ∈ O, it follows that for all rules r in p such that pred (head (r)) = pr, there are sequences of variables x and y and an i, head (r) = pr (x, y), body(r, i) = pr 1 (x, y), and |x| = |y|. From this, it follows that the From the induction hypothesis, it follows that the transitive closure of pr ∈A {(v, w) | pr (v, w) ∈ ground (p)} is a strict partial order over dom |pr |/2 . From this, pr 1 ∈ A , } is a strict partial order over dom |pr |/2 . This completes the proof of our claim.
Proposition B.2. Let Σ be a first-order signature, dom be a finite domain, p be a (Σ, dom)-PROBLOG program, D be a Σ-disjointness template, and be a well-founded partial order over Σ 2 . If p complies with D with respect to and DIS (pr , pr ) ∈ D, then there is no tuple v such that pr (v) ∈ ground (p) and pr (v) ∈ ground (p).
Proof. Let Σ be a first-order signature, dom be a finite domain, p be a (Σ, dom)-PROBLOG program, D be a Σdisjointness template, and be a well-founded partial order over Σ 2 . Furthermore, we assume that p complies with D with respect to and DIS (pr , pr ) ∈ D. We prove, by induction over , that for any DIS (pr , pr ) ∈ D, there is no tuple v such that pr (v) ∈ ground (p) and pr (v) ∈ ground (p). Base Case. Let (pr , pr ) be a pair in Σ 2 such that there is no (pr 1 , pr 1 ) ≺ (pr , pr ) and p, |= DIS (pr , pr ). From this, DIS (pr , pr ) ∈ D, and p complies with D, it follows that (1) there are no rules r ∈ p such that body(r) = ∅ and pred (head (r)) = pr or pred (head (r)) = pr , and (2) the sets A = {c | pr (c) ∈ p ∨ ∃v .v ::pr (c) ∈ p} and A = {c | ∃r ∈ p. head (r) = pr (c) ∨ ∃v .v ::pr (c) ∈ p} are disjoint. From this, it follows that there is no tuple v such that pr (v) ∈ ground (p) and pr (v) ∈ ground (p).

Induction
Step. Assume that there is no tuple v such that pr 1 (v) ∈ ground (p) and pr 1 (v) ∈ ground (p) for any (pr 1 , pr 1 ) ≺ (pr , pr ) such that p, |= DIS (pr 1 , pr 1 ). We now prove that there is no tuple v such that pr (v) ∈ ground (p) and pr (v) ∈ ground (p). There are four cases: • There are no rules r ∈ p such that body(r) = ∅ and pred (head (r)) = pr , and there is a (pr , pr 1 ) ∈ Σ 2 such that (a) DIS (pr , pr 1 ) ∈ D, (b) (pr , pr 1 ) ≺ (pr , pr ), and (c) for all rules r ∈ p such that head (r) = pr (x) there is 1 ≤ i ≤ |body(r)| such that body(r, i) = pr 1 (x). From (pr , pr 1 ) ≺ (pr , pr ), DIS (pr , pr ) ∈ D, and the induction's hypothesis, it follows that there is no tuple v such that pr (v) ∈ ground (p) and pr 1 (v) ∈ ground (p). Furthermore, the relation associated with pr is a subset of the relation associated to pr 1 . Therefore, there is no tuple v such that pr (v) ∈ ground (p) and pr (v) ∈ ground (p). • There are no rules r ∈ p such that body(r) = ∅ and pred (head (r)) = pr , and there is a (pr 1 , pr ) ∈ Σ 2 such that (a) DIS (pr 1 , pr ) ∈ D, (b) (pr 1 , pr ) ≺ (pr , pr ), and (c) for all rules r ∈ p such that head (r) = pr (x) there is 1 ≤ i ≤ |body(r)| such that body(r, i) = pr 1 (x). From (pr 1 , pr ) ≺ (pr , pr ), DIS (pr 1 , pr ) ∈ D, and the induction's hypothesis, it follows that there is no tuple v such that pr 1 (v) ∈ ground (p) and pr (v) ∈ ground (p). Furthermore, the relation associated with pr is a subset of the relation associated to pr 1 . Therefore, there is no tuple v such that pr (v) ∈ ground (p) and pr (v) ∈ ground (p). • There is a (pr 1 , pr 1 ) ∈ Σ 2 such that (a) DIS (pr 1 , pr 1 ) ∈ D, (b) (pr 1 , pr 1 ) ≺ (pr , pr ), and (c) for all rules r, r ∈ p such that head (r) = pr (x) and head (r ) = pr (x ), there are 1 ≤ i ≤ |body(r)|, 1 ≤ i ≤ |body(r )| such that body(r, i) = pr 1 (x), body(r , i ) = pr 1 (x ). From (pr 1 , pr 1 ) ≺ (pr , pr ), DIS (pr 1 , pr 1 ) ∈ D, and the induction's hypothesis, it follows that there is no tuple v such that pr 1 (v) ∈ ground (p) and pr 1 (v) ∈ ground (p). Furthermore, the relation associated with pr is a subset of the relation associated with pr 1 and the relation associated with pr is a subset of the relation associated with pr 1 . Therefore, there is no tuple v such that pr (v) ∈ ground (p) and pr (v) ∈ ground (p). This completes the proof of our claim. Proposition B.3. Let Σ be a first-order signature, dom be a finite domain, p be a (Σ, dom)-PROBLOG program, U be a Σ-uniqueness template, and be a well-founded order over Σ. If p complies with U with respect to and UNQ(pr , K) ∈ U, then for all tuples pr (v), pr (w) ∈ ground (p), if v(i) = w(i) for all i ∈ K, then v = w.
Proof. Let Σ be a first-order signature, dom be a finite domain, p be a (Σ, dom)-PROBLOG program, U be a Σuniqueness template, and be a well-founded partial order over U. Furthermore, we assume that p complies with U with respect to and UNQ(pr , K) ∈ U. We prove, by induction over , that for all UNQ(pr , K) ∈ U, and all tuples pr (v), pr (w) ∈ ground (p), if v(i) = w(i) for all i ∈ K, then v = w. Without loss of generality, in the following we assume that K = {1, . . . , |pr |}. If this is not the case, then our claim holds trivially.
Base Case. Let pr be a predicate such that there is no pr ≺ pr . From this and UNQ(pr , K) ∈ U, it follows that there are no rules r in p such that body(r) = ∅ and pred (head (r)) = pr , and for all w, v in A = {c | pr (c) ∈ p ∨ ∃v.v::pr (c) ∈ p}, if v(i) = w(i) for all i ∈ K, then v = w. From this and {c | pr (c) ∈ ground (p)} ⊆ A, it follows that for all tuples pr (v), pr (w) ∈ ground (p), if v(i) = w(i) for all i ∈ K, then v = w.

Induction
Step. Assume that the claim holds for any pr ≺ pr and K ⊆ {1, . . . , |pr |} such that UNQ(pr , K) ∈ U (we denote this induction hypothesis as (♣)). We now prove that the claim holds for pr as well. Without loss of generality, we assume that there is at least one rule r such that body(r) = ∅ and pred (head (r)) = pr (otherwise the proof is identical to the base case). Assume, for contradiction's sake, that there are two ground atoms pr (v), pr (w) ∈ ground (p) such that v(i) = w(i) for all i ∈ K but v = w. There are two cases: • pr (v) and pr (w) are generated by two ground instances of the same rule r. From v = w, it follows that there is j ∈ K such that v(j) = w(j). From this and the fact that both atoms are generated by the same rule r, it follows that there is a variable x such that x ∈ {x(i) | i ∈ K} and x = x(j), where x = args(head (r)). From this and pr ∈ U, it follows that x ∈ l∈bound(head(r),K,body + (r),µ ) vars(l). We claim that the value of x is determined by the values of the variables whose positions are in K. From this and the fact that v and w agree on all values whose positions are in K, it follows that v = w, leading to a contradiction. We now prove our claim that the value of x is determined by the values of the variables whose positions are in K. The value of the variable x is determined by the grounding of one of the atoms in bound (head (r), K, body + (r), µ ). We first slightly modify the definition of bound . We denote by bd 0 (h, K, L, µ {b(y)}. It is easy to see that (1) bound (head (r), K, body + (r), µ ) = i∈N bd i (h, K, L, µ ), and (2) the fix-point is always reached in a finite amount of steps (bounded by |body + (r)|). We now prove by induction on i that the groundings of the literals in bd i (h, K, L, µ ) is always determined by the values of the variables in u(args(head (r)), K). From this, our claim trivially follows. For the base case, let i = 0. Then, for any literal b(y) ∈ bd 0 (h, K, L, µ ), it follows that (a) b ≺ pr , and (b) u(y, µ (b)) ⊆ u(args(head (r)), K). From this, p complies with U, and the induction's hypothesis (♣), it follows that the variables in UNQ(b, µ (b)) uniquely determine the grounding of b(y). From this and u(y, µ (b)) ⊆ u(args(head (r)), K), it follows that the variables in u(args(head (r)), K) uniquely determine the grounding of b(y). For the induction's step, assume that the claim hold for all j < i (we denote this induction hypothesis as (♠)). Let b(y) ∈ bd i (h, K, L, µ ) (without loss of generality, b(y) ∈ bd i−1 (h, K, L, µ )). From this, it follows that b pr and there is a l ∈ bound i−1 (h, K, L, µ ) such that u(y, µ (b)) ⊆ vars(l ). From the induction hypothesis (♠), it follows that the grounding of l is directly determined by the grounding of the values of the variables in u(args(head (r)), K). Furthermore, from b pr , p, |= UNQ(b, µ (b)), and the induction hypothesis (♣), it follows that the values of the variables in u(y, µ (b)) uniquely determine the grounding of b(y). Therefore, the values of the variables in u(args(head (r)), K) uniquely determine the grounding of b(y). This completes the proof of the claim. • pr (v) and pr (w) are generated by ground instances of two different rules r 1 and r 2 . From this, UNQ(pr , K) ∈ U, and K = {1, . . . , |pr |}, it follows that it follows that there is a value i ∈ K such that args(head (r 1 )) ∈ dom, args(head (r 2 )) ∈ dom, and args(head (r 1 )) = args(head (r 1 )). Therefore, there is an i ∈ K such that v(i) = w(i). This contradicts the fact that v(i) = w(i) for all i ∈ K. This completes the proof of our claim.

6) Proofs about Propagation Maps:
Here we prove some results about propagation maps, which we afterwards use in proving the main result.
Proposition B.4. Let Σ be a first-order signature, dom be a finite domain, p be a (Σ, dom)-PROBLOG program, r be a rule in p, and l be the i-th literal in body(r). Furthermore, let µ be the (r, l)-vertical map. Given a rule r ∈ ground (p, r), then b(j) = h(µ(j)) for any j such that µ(j) is defined, where h = args(head (r )) and b = args(body(r , i)).
Proof. Let Σ be a first-order signature, dom be a finite domain, p be a (Σ, dom)-PROBLOG program, r be a rule in p, and l be the i-th literal in body(r). Furthermore, let µ be the (r, l)-vertical map and r ∈ ground (p, r). From the definition of ground (p, r), it follows that there is an assignment Θ from variables to elements in dom such that r = rΘ. From this, b(j) = Θ(args(l)(j)) and h(µ(j)) = Θ(args(head (r))(µ(j))). Note that from the definition of (r, l)-vertical map it follows that args(l)(j) = args(head (r))(µ(j)). From this, b(j) = h(µ(j)) whenever µ(j) is defined.
Proposition B.5. Let Σ be a first-order signature, dom be a finite domain, p be a (Σ, dom)-PROBLOG program, r be a rule in p, l be the i-th literal in body(r), and l be the j-th literal in body(r). Furthermore, let µ be the (r, l, l )-horizontal map. Given a rule r ∈ ground (p, r), then b 1 (k) = b 2 (µ(k)) for any k such that µ(k) is defined, where b 1 = args(body(r , i)) and b 2 = args(body(r , j)).
Proof. Let Σ be a first-order signature, dom be a finite domain, p be a (Σ, dom)-PROBLOG program, r be a rule in p, l be the i-th literal in body(r), and l be the jth literal in body(r). Furthermore, let µ be the (r, l, l )horizontal map and r ∈ ground (p, r). From the definition of ground (p, r), it follows that there is an assignment Θ from variables to elements in dom such that r = rΘ. From this, b 1 (j) = Θ(args(l)(j)) and b 2 (µ(j)) = Θ(args(l )(µ(j))).
Proof. Let Σ be a first-order signature, dom be a finite domain, p be a (Σ, dom)-PROBLOG program, P = pr 1 be a directed path in graph(p), and ν : N → N be a mapping. Furthermore, let P = a 1 → (r 1 , s 1 , i 1 ) → a 2 → (r 2 , s 2 , i 2 ) → . . . → (r n−1 , s n−1 , i n−1 ) → a n be a directed path in gg(p) corresponding to P . Assume that P ν-downward links to l, where l is the k-th literal in r j . From this, it follows that the function µ := µ • µ j • . . . • µ 1 satisfies µ(m) = ν(m) for all m for which ν(k) is defined, where for 1 ≤ h ≤ j, µ h is the vertical map connecting body(r h , i h ) and r h , and µ is the horizontal map connecting body(r j+1 , i j+1 ) with l. By repeatedly applying Proposition B.4 to the rules in P , we have that b 1 (m) = b j (φ(m)) whenever φ(m) is defined, where b 1 = args(body(s 1 , i 1 )), b j = args(body(s j , i j )), and φ = µ j • . . . • µ 1 . Moreover, by applying Proposition B.5, we have that b j (m) = v 2 (µ (m)) whenever µ (m) is defined, where b j = args(body(s j , i j )) and v 2 = args(body(s j , k)). Therefore, we have that b 1 (m) = v 2 (µ(m)) whenever µ (m) is defined (by composing the previous results). From this and µ(m) = ν(m) for all m for which ν(m) is defined, it follows that b 1 (m) = v 2 (ν(m)) whenever µ (m) is defined.

7) Proofs about Connected Rules:
We now prove that, for strongly connected rules, the grounding of a rule's head uniquely determines the grounding of the rule's body (Proposition B.8), whereas for weakly connected rules the grounding of one of the atoms in the body determines the head's grounding (Proposition B.9).
Proposition B.8. Let Σ be a first-order signature, dom be a finite domain, p be a (Σ, dom)-PROBLOG program, r be a rule in p, and U be a Σ-uniqueness template. If p complies with U and r is strongly connected for U, then for all r 1 , r 2 ∈ ground (p, r), if head (r 1 ) = head (r 2 ), then r 1 = r 2 .
Proof. Let Σ be a first-order signature, dom be a finite domain, p be a (Σ, dom)-PROBLOG program, r be a rule in p, and U be a Σ-uniqueness template. Furthermore, we assume that (1) p complies with U, and (2) there are join trees J 1 , . . . , J n such that (a) the trees cover all literals in body(r), and (b) for each 1 ≤ i ≤ n, J i is strongly connected for U. Finally, let r 1 , r 2 ∈ ground (p, r) be two ground rules such that head (r 1 ) = head (r 2 ). Assume, for contradiction's sake, that r 1 = r 2 . Therefore, there is a position 1 ≤ i ≤ |body(r)| such that body(r 1 , i) = body(r 2 , i). Let J = (N, E, root, λ) be one of the join trees that cover l = body(r, i). We claim that the grounding of head (r) determines the grounding of all literals in J. From this, it follows that body(r 1 , i) = body(r 2 , i) leading to a contradiction.
We now prove our claim that the grounding of head (r) determines the grounding of all literals in J. Let V (J, i) be the set of all the nodes in J at distance at most i from the root root. Furthermore, we denote by ground (r, r , J, i) the set {body(r , j) | body(r, j) ∈ V (J, i)}. We prove, by induction on i, that for all i and all ground rules r 1 and r 2 instances of r, if head (r 1 ) = head (r 2 ), then ground (r, r 1 , J, i) = ground (r, r 2 , J, i). From this, it follows that the grounding of head (r) determines the grounding of all literals in J.
Base case. For i = 0, there is a j such that V (J, 0) = {body(r, j)}. From this, it follows that ground (r, r 1 , J, 0) = {body(r 1 , j)} and ground (r, r 2 , J, 0) = {body(r 2 , j)}. Furthermore, anc(J, body(r, j)) = ∅. There are two cases depending on whether body(r, j) is a positive literal or not: 1) If body(r, j) is a positive literal of the form a(x), then body(r 1 , j) = a(c 1 ) and body(r 2 , j) = a(c 2 ). From the fact that J is strongly connected for U, it follows that there is a set of variables K ⊆ {i | x(i) ∈ support(a(x))} such that UNQ(a, K) ∈ U. From support(a(x)) = vars(head (r)) ∪ {x | (x = c) ∈ cstr (r)∧c ∈ dom} and head (r 1 ) = head (r 2 ), it follows that the values assigned to the variables associated to the indexes in K are the same in r 1 and r 2 . From this, UNQ(a, K) ∈ U, p complies with U, {a(c 1 ), a(c 2 )} ⊆ ground (p), and Proposition B.3, it follows c 1 = c 2 and ground (r, r 1 , J, 0) = ground (r, r 2 , J, 0). 2) If body(r, j) is a negative literal of the form ¬a(x), then body(r 1 , j) = ¬a(c 1 ) and body(r 2 , j) = ¬a(c 2 ). From the fact that J is strongly connected for U, it follows that vars(¬a(x)) ⊆ support(¬a(x)). From this, support(¬a(x)) = vars(head (r)) ∪ {x | (x = c) ∈ cstr (r)∧c ∈ dom}, and head (r 1 ) = head (r 2 ), it follows that the values of the variables in support(¬a(x)) are the same in r 1 and r 2 . From this, it follows that c 1 = c 2 and ground (r, r 1 , J, 0) = ground (r, r 2 , J, 0).
Proposition B.9. Let Σ be a first-order signature, dom be a finite domain, p be a (Σ, dom)-PROBLOG program, r be a rule in p, and U be a Σ-uniqueness template. If p complies with U and r is weakly connected for U, then for all r 1 , r 2 ∈ ground (p, r), if there is an 1 ≤ i ≤ |body(r)| such that body(r 1 , i) = body(r 2 , i), then r 1 = r 2 .
Proof. Let Σ be a first-order signature, dom be a finite domain, p be a (Σ, dom)-PROBLOG program, r be a rule in p, and U be a Σ-uniqueness template. Furthermore, we assume that p complies with U and that r is weakly connected for U, namely there is a join tree J = (N, E, root, λ) such that (a) J is weakly connected for U, (b) N ⊆ body + (r), and (c) all literals in body(r) \ N are (r, U, N )-strictly guarded. Let r 1 , r 2 ∈ ground (p, r) be two ground rules such that there is an 1 ≤ i ≤ |body(r)| such that body(r 1 , i) = body(r 2 , i), and let l be the literal body(r, i). There are two cases: 1) body(r, i) ∈ N . Given a node n in a join tree J, we denote by adjacent(n, i), where i ∈ N, the sub-tree obtained by considering only the nodes reachable from n using at most i edges. We claim that for all nodes in adjacent(l, j), the corresponding ground atoms in r 1 and r 2 are the same. From this and the fact that there is a j such that adjacent(l, j) = J, it follows that for all i ∈ {j | body(r, j) ∈ N }, body(r 1 , i) = body(r 2 , i). From this and the fact that the literals in body(r) \ N are (r, U, N )-strictly guarded, it follows that for all i ∈ {j | body(r, j) ∈ body(r) \ N }, body(r 1 , i) = body(r 2 , i) (since vars(l) ⊆ l ∈N ∩body + (r) vars(l ) ∪ {x | (x = c) ∈ cstr (r)∧c ∈ dom} for any literal l in body(r)\N ). Therefore, body(r 1 ) = body(r 2 ). 2) body(r, i) ∈ N . From this and the fact that r is weakly connected, it follows that there a j such that body(r, j) = a(x), body(r, j) ∈ N , and a UNQ(a, K) ∈ U such that {x(i) | i ∈ K} ⊆ vars(body(r, i)). From this, p complies with U, body(r 1 , i) = body(r 2 , i), {body(r 1 , j), body(r 2 , j)} ⊆ ground (p), and Proposition B.3, it follows that body(r 1 , j) = body(r 2 , j). We proved above that if body(r 1 , j) = body(r 2 , j) and body(r, j) ∈ N , then body(r 1 ) = body(r 2 ). Therefore, body(r 1 ) = body(r 2 ). From vars(head (r)) ⊆ l∈body + (r) vars(l) and body(r 1 ) = body(r 2 ), it follows that head (r 1 ) = head (r 2 ). Therefore, We now prove, by induction on j, that for all nodes in adjacent(l, j), the corresponding ground atoms in r 1 and r 2 are the same.
Base Case. The sub-tree adjacent(l, 0) contains only the node l = body(r, i). Since body(r 1 , i) = body(r 2 , i), the claim holds for the base case.
Induction step. Assume now that the claim holds for all j < j. We now prove that the claim holds also for j. The sub-tree adjacent(l, j) is obtained by extending adjacent(l, j −1) with either edges of the form n 1 L1 − − → n 1 , where n 1 ∈ adjacent(l, j − 1), or n 2 L2 − − → n 2 , where n 2 ∈ adjacent(l, j − 1). In both cases, from the induction hypothesis, the ground literals corresponding to n 1 and n 2 are l 1 and l 2 and they are the same in r 1 and r 2 . From the definition of weakly connected join tree, there are variables K 1 ⊆ L 1 and K 2 ⊆ L 2 such that UNQ(pred (n 1 ), K 1 ) ∈ U and UNQ(pred (n 2 ), K 2 ) ∈ U. From this, p complies with U, the fact that the value of K 1 and K 2 are fixed by l 1 and l 2 , and Proposition B.3, it follows that the ground atoms corresponding to n 1 and n 2 are the same in r 1 and r 2 (because the values in K 1 and K 2 determines all values in n 1 and n 2 ).

8) Acyclicity Proof:
We are now ready to prove our first key result, namely that the ground graph associated to an acyclic PROBLOG program is a forest of poly-trees, i.e., its undirected version does not contain simple cycles (which are cycles without repetitions of edges and vertices other than the starting and ending vertices).
Proposition B.10. Let Σ be a first-order signature, dom be a finite domain, and p be a (Σ, dom)-acyclic PROBLOG program. The graph gg(p) is a forest of poly-trees, i.e., its undirected version does not contain simple cycles.
Proof. Let Σ be a first-order signature, dom be a finite domain, and p be a (Σ, dom)-acyclic PROBLOG program. We prove that the undirected version of gg(p) is acyclic. Assume, for contradiction's sake, that this is not the case, namely there is a simple cycle C := n 1 → n 2 → . . . → n k → n 1 in the undirected version of gg(p). There are two cases: (1) there is a directed simple cycle in gg(p) that directly corresponds to C, or (2) there are n directed paths P 1 , . . . , P n in gg(p) that induce a simple cycle C in the undirected version of gg(p) (and P 1 , . . . , P n does not correspond to any directed simple cycle in ggp). From the first case, it follows that there is a directed cycle in graph(p), whereas from the second case, it follows that there is an undirected cycle in graph(p).
Undirected Cycle. Assume that C does not directly correspond to any directed simple cycle in gg(p). From this, it follows that there are n directed paths P 1 , . . . , P n in gg(p) such that P 1 , . . . , P n correspond to the simple cycle C in the undirected version of gg(p). From this, it follows that P 1 , . . . , P n form an undirected cycle in gg(p). Therefore: 1) For 1 ≤ j ≤ n, there is a directed path D j := 2) For all 1 ≤ j ≤ n, 1 ≤ h < n j , s h ∈ ground (p, r h ) and head (s h ) = a h+1 (c h+1 ), where P j := a 1 (c 1 ) → (r 1 , s 1 , . . . , D n is a directed simple cycle, then C would contain loops (contradicting our assumption that C is a simple cycle). Since p is acyclic and D 1 , . . . , D n form an undirected cycle in graph(p) that is not a directed simple cycle, it follows that there is an ordering template O, a disjointness template D, and a uniqueness template U such that (1) p complies with O, D, and U and (2) there is an unsafe structure S that covers D 1 , . . . , D n and is (O, D, U)-guarded. We assume that there are values i, a, b, c such that 1) S = D a , D b , D c , U , 2) a = i, b = (i + 1)%n, and c = (i + 2)%n (i.e., P a , P b , and P c are adjacent in the cycle), and 3) U is the undirected path containing all D i 's that are different from D a , D b , and D c . Note that the previous assumption is without loss of generality: we can always pick the directed paths in gg(p) inducing C in such a way that they match the guarded structure S.
Let P a be a 1 (a 1 ) → (r 1 , s 1 , i 1 ) → a 2 (a 2 ) → (r 2 , s 2 , We claim that s h = s h for any 1 ≤ h ≤ n a . From this, it follows that P a = P b . This contradicts the fact that P 1 , . . . , P n induces a simple cycle in the undirected version of gg(p) (because the cycle is not simple). We now prove, by induction on d, that s d = s d and Base Case. Assume that d = 1. From r 1 = r 1 , r 1 is weakly connected for U, body(s 1 , i 1 ) = body(s 1 , i 1 ) = a 1 (c 1 ), s d ∈ ground (p, r d ), s d ∈ ground (p, r d ) , and Proposition B.9, it follows that s 1 = s 1 . From this, a 1 (a 1 ) = head (s 1 ), and b 1 (b 1 ) = head (s 1 ), it follows that a 1 (a 1 ) = b 1 (b 1 ).

Induction
Step. Assume that the claim holds for all d < d. We now prove that s d = s d and a d ( it follows that there is an annotation DIS (pr , pr ) ∈ D a set K ⊆ {1, . . . , |a|}, and a bijection ν : K → {1, . . . , |pr |} such that D a ν-downward links to pr and D a ν-downward links to pr . From D a ν-downward links to pr , P a is a ground instance of D a , and Proposition B.6, it follows that there is a positive literal pr (v) in the body of one of the ground rules such that a 1 (a 1 )(k) = v(ν(K)) for any k ∈ K. From this and the definition of ground , it follows that pr (v) ∈ ground (p). From D b ν-downward links to pr , P b is a ground instance of D b , and Proposition B.6, it follows that there is a positive literal pr (v ) in the body of one of the ground rules such that b 1 (b 1 )(k) = v (ν(K)) for any k ∈ K. From this and the definition of ground , it follows that pr (v ) ∈ ground (p). Finally, from the fact that P a and P b are head-connected, it follows that a 1 (a 1 ) = b 1 (b 1 ). From this, a 1 (a 1 )(k) = v(ν(K)) for any k ∈ K, and b 1 (b 1 )(k) = v (ν(K)) for any k ∈ K, it follows that v = v . From this, pr (v) ∈ ground (p) and pr (v) ∈ ground (p). This contradicts Proposition B.2, DIS (pr , pr ) ∈ D, and p complies with D. We claim that s h = s h for any 1 ≤ h ≤ n c . From this, it follows that P c = P b . This contradicts the fact that P 1 , . . . , P n induces a simple cycle in the undirected version of gg(p) (because the cycle is not simple). We now prove, by induction on d, that and Proposition B.8, it follows that s 1 = s 1 . From this, a 1 (a 1 ) = head (s 1 ), and b 1 (b 1 ) = head (s 1 ), it follows that b n b (b n b ) = c n b (c n b ).

Induction
Step. Assume that the claim holds for all d < d. We now prove that s n b −d = s n b −d and From the induction's hypothesis, it follows that s n b −d+1 = s n b −d+1 . From this and gg's definition, it follows that follows that there is an annotation DIS (pr , pr ) ∈ D, a set K ⊆ {1, . . . , |a|}, and a bijection ν : K → {1, . . . , |pr |}, such that D b ν-upward links to pr and D c ν-upward links to pr . From D b ν-upward links to pr , P b is a path in the ground graph corresponding to D b , and Proposition B.7, it follows that a positive literal pr (v) in the body of one of the ground rules such that b n b (b n b )(k) = v(ν(K)) for any k ∈ K. From this and the definition of ground , it follows that pr (v) ∈ ground (p). From D c ν-upward links to pr , P c is a path in the ground graph corresponding to D c , and Proposition B.7, it follows that a positive literal pr (v ) in the body of one of the ground rules such that c nc (c nc )(k) = v (ν(K)) for any k ∈ K. From this and the definition of ground , it follows that pr (v ) ∈ ground (p). Finally, from the fact that P b and P c are tail-connected, it follows that b n b (b n b ) = c nc (c nc ). From this, b n b (b n b )(k) = v(ν(K)) for any k ∈ K, and c nc (c nc )(k) = v (ν(K)) for any k ∈ K, it follows that v = v . Therefore, pr (v) ∈ ground (p) and pr (v) ∈ ground (p). This contradicts Proposition B.2, DIS (pr , pr ) ∈ D, and p complies with D. This completes the proof of our claim. 9) Auxiliary Results: Here we prove two auxiliary results that help in establishing that programs are acyclic. In particular, Proposition B.11 states pre-conditions that allows reducing the guardedness of a complex undirected structure to the guardedness of simpler structures. Similarly, Proposition B.12 states pre-conditions that allows reducing the guardedness of a complex directed structure to the guardedness of a sequence of simpler structures. Note that Proposition B.12 can be easily extended to support (1)  Proof. Let p be a PROBLOG program, O be an ordering template, D be a disjointness template, U be a uniqueness template, C be an undirected cycle in graph(p), and S = D 1 , D 2 , D 3 , U be an undirected structure. We assume that (1) p complies with O, D, and U, (2) C is equivalent to D 1 , U 1 , U, U 2 , D 3 , D 2 , (3) S is (O, D, U)-guarded. We define the undirected unsafe structure S = D 1 , D 2 , D 3 , U 1 , U, U 2 . From our assumption C is equivalent to D 1 , U 1 , U, U 2 , D 3 , D 2 . Thus, S covers C. Furthermore, since S and S agree on all directed paths, which are the only ones that determine whether an undirected structure is guarded, it follows that S is (O, D, U)-guarded In the following, we say that a directed cycle is guarded by a set of predicates O and a bijection ν iff the definition of guarded cycle is satisfied for the specific bijection ν.

B. Relaxed Acyclic Programs
Acyclic PROBLOG programs as defined above are very restrictive. For instance, they cannot encode rules like those in Section V. We now design relaxed acyclic programs, a larger fragment of PROBLOG where these examples can be encoded.
The key components of this new fragment are two syntactic transformations over PROBLOG programs that, while not preserving the program's semantics, preserve certain key aspects of the program's structure. Intuitively, a PROBLOG program p is a relaxed acyclic program if the program obtained from p by applying the transformations is an acyclic PROBLOG program.
Finally, we develop a procedure for compiling any relaxed acyclic PROBLOG program into a poly-tree Bayesian Network. Since any acyclic program is a relaxed acyclic program as well, this procedure can be applied also to acyclic programs.
Given a program p and a rule r ∈ p, [r] p denotes the set {r ∈ p | r r}. We say that a rule r is maximal in a program p iff there is no rule r ∈ p such that r r . The kernel of [r] p , denoted k([r] p ), is the rule r defined as follows: head (r ) = head (r), |body(r )| = |body(r)|, cstr (r ) = cstr (r), and for all 1 ≤ i ≤ |body(r )|, then body(r , i) = a i (c i ) if for all rules r ∈ [r] p (1) |body(r )| ≥ i and (2) body(r , i) is a positive literal and body(r , i) = ¬a i (c i ) otherwise, where a i = pred (body(r, i)) and c i = args(body(r, i)).
The maximal projection of p, denoted p ⇓ , is {k([r] p ) | ¬∃r ∈ p. r r }. A maximal partition PP of p is a subset of P(p) such that: (1) for each R ∈ PP , R = [r] p for some maximal rule r ∈ p, and (2) for each R 1 , R 2 ∈ PP , R 1 ∩R 2 = ∅. A maximal partition P P induces a maximal assignment ν PP : p → PP such that ν PP (r) = R, where R ∈ PP and r ∈ R if r is maximal, and ν PP (r) = ∅ otherwise.
The syntactic transformation α, which removes all nonmaximal rules, takes as input a PROBLOG program p and returns as its maximal projection p ⇓ .
2) CPT-like predicates: We now present CPT-like predicates, a special kind of probabilistic structure that can be formalized using annotated disjunctions. While general annotated disjunctions cannot be used in our encoding, since they introduce, in general, cycles in the underlying Bayesian Network, CPT-like predicates can be still encoded as polytrees.
Let Σ be a first-order signature, dom be a finite domain, pr be a predicate symbol in Σ of arity |pr |, p be a (Σ, dom)-PROBLOG program, and K be a set of distinct integer values such that for all i ∈ K, 1 ≤ i ≤ |pr |. Given a tuple t, we denote by t ↓ {i1,...,in} the tuple (t(i 1 ), . . . , t(i n )).
We say that pr is K-fixed domain with respect to p iff for all rules r ∈ p, the following conditions hold: • if pred (head (r)) = pr , then args(head (r)) ↓ K is a tuple in dom |K| , and • if pred (body(r, j)) = pr , for some 1 ≤ j ≤ |body(r)|, then args(body(r, j)) ↓ K is a tuple in dom |K| . We denote by pdom(pr , p, K) the set of |K|-tuples representing all constant values associated with the positions in K. Namely, pdom(pr , p, K) = {args(head (r)) ↓ K | r ∈ p} ∪ {args(body(r, j)) ↓ K | r ∈ p ∧ 1 ≤ i ≤ |body(r)|}. Finally, given an atom a(x) and a K, we denote by β(a(x), K) the atom a(x ↓ K ).
Given a program p, the function µ p,D,U associates to each predicate symbol pr in Σ the maximal set K such that pr is (K, D, U)-CPT-like with respect to p. The syntactic transformation β p,D,U takes as input a PROBLOG program p and it returns as output the program p ⇓ (pr 1 ,µ p,D,U (pr 1 )),...,(pr n ,µ p,D,U (pr n )) , where pr 1 , . . . , pr n are all predicate symbols in Σ.
Note that p is defined on a different vocabulary than p. The program p is defined over the "reduced vocabulary" obtained by applying β to the atoms in p.
3) Relaxed Acyclic PROBLOG programs: A relaxed acyclic (Σ, dom)-PROBLOG program is a (Σ, dom)-PROBLOG program p such that there are a Σ-ordering template O, a Σdisjointness template D, and a Σ-uniqueness template U such that α(β p,D,U (p)) is (O, D, U)-acyclic. An aciclicity witness for a program p is a tuple (O, D, U) such that α(β p,D,U (p)) is a (O, D, U)-acyclic PROBLOG program.
Given a relaxed acyclic (Σ, dom)-PROBLOG program p, we associate to each rule r in α(β p,D,U (p)), the set [r] p of rules in p defined as follows: The set [r] p contains all rules in p that are represented by the rule r in α(β p,D,U (p)).
4) Compilation to Bayesian Networks: Given a relaxed acyclic PROBLOG program p, its encoding as a Bayesian Network BN = (N, E, cpt), denoted bn(p), is defined by Algorithm 2.
5) Encoding's acyclicity: Here, we prove that Algorithm 2 produces a Bayesian Network that is a forest of poly-trees. Note that Algorithm 2 produces a forest of poly-trees and not just a single poly-tree because some predicates symbols may be independent. For instance, the program consisting of the rules a(x) ← b(x) and c(x) ← d(x) corresponds to two polytrees (one per rule).
Proposition B.13. Let Σ be a first-order signature, dom be a finite domain, p be a (Σ, dom)-relaxed acyclic PROBLOG program, and (O, D, U) be a witness for p's acyclicity. The Bayesian Network (N, E, cpt) produced by Algorithm 2 on input p is a forest of poly-trees.
Proof. Let Σ be a first-order signature, dom be a finite domain, p be a (Σ, dom)-relaxed acyclic PROBLOG program, and (O, D, U) be a witness for p's acyclicity. Furthermore, let BN = (N, E, cpt) be the Bayesian Network produced by Algorithm 2 on input p. There is a one-to-one mapping from paths in the ground graph gg(α(β p,D,U (p)))) and paths in the Bayesian Network produced by Algorithm 2. Namely, there is a path from a(c) to a (c ) in gg(α(β p,D,U (p)))) iff Algorithm 2: Constructing the Bayesian Network. The sub-routines tree, CPT , and CPT ⊕ are shown in Algorithm 3.
Creates the nodes. for r ∈ p do for r ∈ ground (p, r) do there is a path from X[a(c)] to X[a (c )] in BN . Assume that there is a cycle in the undirected version of BN . From this, it follows that there is an undirected cycle in gg(α(β p,D,U (p)))). This, however, contradicts Proposition B.10 (since p is relaxed acyclic, then α(β p,D,U (p))) is acyclic and there are no undirected cycles in gg(α(β p,D,U (p))))).

6) Bayesian Networks:
A Bayesian Network BN is a tuple (N, E, cpt), where N is the set of nodes, E is the set of edges, cpt is a function associating to each node n ∈ N its Conditional Probability Table. For each node n ∈ N , we denote by D(n) its domain, i.e., the possible values it can have. Note that D(n) can be immediately derived from cpt(n). We denote by p(n) the set of n's parents, i.e., p(n) = {n | n → n ∈ E}. Furthermore, we denote by ancestors(n) the set of n's ancestors, i.e., ancestors(n) = p(n) ∪ n ∈p(n) ancestors(n ).
A BN -total assignment is a total function ν that associates to each n ∈ N a value in n ∈ D(n), whereas a BNpartial assignment is a partial function ν that associates to each n ∈ N , where N ⊆ N , a value in n ∈ D(n). The probability defined by BN given ν, written BN (ν) is [Σ y1 . . . Σ ym (Π n∈N cpt(n)) (Y 1 = y 1 , . . . , Y m = y m )] (X 1 = v 1 , . . . , X n = v n ), where dom(ν) = {X 1 , . . . , X n }, N \ dom(ν) = {Y 1 , . . . , Y m }, and v i = ν(X i ) for 1 ≤ i ≤ n. 7) Correctness Proof: Before presenting our correctness proof, we introduce some machinery. Let p be a relaxed acyclic PROBLOG program, (O, D, U) be a witness for p, and BN = (N, E, cpt) be the Bayesian Network produced by Algorithm 2 having p and (O, D, U) as inputs. For each rule atom a(c) ∈ ground (p), we denote by a(c)↓ p the atom obtained by applying the transformations α and β, whereas we denote by a(c)↑ p the constants not used in the transformed program, namely a(c)↑ p is c ↓ {1,...,|c|}\µ p,D,U (a) . Furthermore, given a rule r ∈ p (respectively a ground rule s ∈ ground (p, r)), we denote by r↓ p (respectively s↓ p ) the rule obtained by applying the transformations α and β. If µ p,D,U (a) = ∅, then a(c)↑ p = . We say that the kernel of BN , denoted K(BN ), is the set of variables {X[r, ∅, a(c)] ∈ N | ∃v. r = v::a(c)}. Note that all nodes n ∈ K(BN ) are boolean random variables by construction, namely D(n) = { , ⊥}. Given a BN -total assignment ν, we say that ν is consistent iff for all variables n ∈ N \K(BN ), cpt(n)(ν(P 1 ), . . . , ν(P m ), ν(n)) = 1, where p(n) = {P 1 , . . . , P m }. Furthermore, we say that ν is a model for a state s, written ν |= s, iff a(c) ∈ s ⇔ ν(X[a(c)↓ p ]) = a(c)↑ p .
We first prove a simple results that connect the original program p and its transformed version α(β(p)).
Proposition B.14. Let Σ be a first-order signature, dom be Algorithm 3: Auxiliary functions used in Algorithm 2.
Proof. Let Σ be a first-order signature, dom be a finite domain, p be a (Σ, dom)-relaxed acyclic PROBLOG program, (O, D, U) be a witness for p, s be a (Σ, dom)-structure, and p be the program α(β p0,D,U (p 0 )).
We first prove our first claim. Let a ∈ ground (p). From this, it follows that there is an i such that a ∈ ground (p, i). We now prove our claim by induction on i. The base case is a ∈ ground (p, 0). From this, it follows that a is either a ground atom or a probabilistic ground atom. From this and the definition of α and β, a↓ p = a. From this, it follows that a ∈ p and, therefore, a ∈ ground (p ). For the induction step, assume that our claim holds for all j < i, we now show that it holds also for i. The only interesting case is a ∈ ground (p, i) \ ground (p, i − 1). From this, it follows that there is a rule r and a ground rule s such that all body + (s) ⊆ ground (p, i−1). From this, r↓ p ∈ p , the fact that the transformation does not introduce new positive literals, and the induction hypothesis, it follows that {b↓ p | b ∈ body + (s)} ⊆ ground (p ). From this and ground 's definition, it follows that a↓ p ∈ ground (p ).
The proof of our second claim is similar to the first one.
Here are now ready to prove the two key lemmas for the encoding's correctness.
Proposition B.15. Let Σ be a first-order signature, dom be a finite domain, p be a (Σ, dom)-relaxed acyclic PROBLOG program, (O, D, U) be a witness for p, s be a (Σ, dom)structure, and BN = (N, E, cpt) be the Bayesian Network generated by Algorithm 2 having p and (O, D, U) as input. There is a p-probabilistic assignment f such that prob(f ) = k and g f (p) = s iff there is a BN -total assignment ν such that BN (ν) = k, ν is consistent, and ν |= s.
Proof. Let Σ be a first-order signature, dom be a finite domain, p be a (Σ, dom)-relaxed acyclic PROBLOG program, (O, D, U) be a witness for p, s be a (Σ, dom)-structure, and BN = (N, E, cpt) be the Bayesian Network generated by Algorithm 2 having p and (O, D, U) as input. We now prove both directions of our claim.
(⇒). Let f be a p-probabilistic assignment f such that prob(f ) = k and g f (p) = s. Furthermore, let ν be the following BN -total assignment: The assignment ν is well-defined since (1) 2). Furthermore, the assignment ν is consistent by construction. Indeed, for all variables n ∈ N \ K(BN ), the corresponding entry in the CPT is 1.
We still have to prove that g f (p) = s. From Proposition B.16, ν's consistency, f (v::a(c)) = ν(X[{v::a(c)}, ∅, a(c)]), it follows that a(c) ∈ g f (p) iff ν(X[a(c)↓ p ]) = a(c)↑ p . From this and ν |= s, it follows g f (p) = s. as input, f be a p-probabilistic assignment, and ν be a consistent BN -variable assignment such that ν(X[v::a(c), ∅, a(c)]) = f (v::a(c)) for all v::a(c) ∈ p. Furthermore, let p be the acyclic PROBLOG program obtained after applying the α and β transformations. We claim that a(c) ∈ g f (p, µ(a)) iff ν(X[a(c) ↓ p ]) = a(c) ↑ p . From this, a(c) ∈ g f (p) iff a(c) ∈ g f (p, j, i) for some j and i, and a(c) ∈ g f (p) iff a(c) ∈ g f (p, µ(a)), it follows that a(c) ∈ g f (p, j, i), for some j and i, iff ν(X[a(c)↓ p ]) = a(c)↑ p . However, there may be some nodes in BN that do not correspond to any ground rule or atom in g f (p, r) or g f (p).
INF for PROBLOG is #P -hard. This follows from the #P -hardness of inference on arbitrary Bayesian networks (BNs) [47], which can be encoded in PROBLOG. We now show that inference for PROBLOG programs is #P -hard even in terms of data complexity. We do this using a reduction from the #SAT problem (counting the number of satisfying assignments of a propositional formula φ), which is #Phard [56].
Proposition B.19. INF is #P -hard in terms of data complexity for PROBLOG programs.
Proof. We show this by reducing the #SAT problem to inference for a PROBLOG program p where (1) the formula can be encoded in edb(p), and (2) the rules are fixed. Let φ be a propositional formula.
First-order Signature. Let Σ be the signature containing the following predicate symbols: • e of arity 1, which is used to store the identifiers associated to all sub-expressions of φ, • state of arity 1, which is used to store the propositions in the model, • sat of arity 1, which is used to denote whether an expression is satisfiable or not, • conj of arity 3 which is used to encode conjunctions, • disj of arity 3 which is used to encode disjunctions, • neg of arity 2 which is used to encode negations, and • prop of arity 2 used to encode propositions. Rules. We now define a fixed set of rules encoding the semantics of propositional logic.
Reduction. There are 2 n(φ) grounded instances of R ∪ E , where n(φ) is the number of predicate symbols in φ, each one with probability 1 /2 n(φ) . The grounded instances represent all possible assignments of and ⊥ to the proposition symbols in φ. It is easy to see that sat(id φ ) can be derived in a grounded instance iff it represents a model for φ. Therefore, the probability R∪E (id φ ) is k /2 n(φ) , where k is the number of models that satisfy φ.
Note that the encoding shown in the previous proof can be tweaked to work for acyclic PROBLOG programs but only for propositional formulae without repetitions of propositional symbols. We remark that the #SAT problem restricted to formulae without repetitions is no longer #P -hard. Indeed, it can be solved in PTIME as follows: given a formula φ without repetitions, we can construct a poly-tree boolean Bayesian Network BN encoding φ in O(|φ|), where the nodes associated to sub-formulae of the from p have a uniform probability distribution (i.e., p is with probability 1 /2 and ⊥ with probability 1 /2). Then, the probability associated to the root of φ is going to be k /2 n(φ) , where k is the number of satisfying assignments. Since the inference on BN can be done in linear time in |BN | and |BN | ∈ O(|φ|), then the whole problem is in PTIME.

10) Expressiveness:
Here we show that any BN that consists of a forest of poly-trees can be represented as a relaxed acyclic program.
Proposition B.20. Any BN that is a forest of poly-trees can be represented as a relaxed acyclic PROBLOG program.
Proof. Let bn be a BN that is a forest of poly-trees. We now construct the corresponding relaxed acyclic PROBLOG program. In particular, for each random variable X in bn, we show how to equivalently encode it as PROBLOG rules. Without loss of generality, we assume there is a unique mapping id from random variables in bn to predicate symbols identifiers. With a slight abuse of notation, we use X to refer both to the random variable and to the corresponding symbol id (X).
Boolean Random Variables with parents. Let X be a boolean random variable X with parents p(X) = {Y 1 , . . . , Y n }, cpt(X) be the function associated with X, and v 1 , . . . , v m be all possible assignments to the variables in p(X). We introduce m fresh predicate symbols sw X,v1 , . . . , sw X,vm . For each v i , we introduce the probabilistic atom c i ::sw X,vi , where cpt(X)(v i , ) = c i . Finally, for each v i , we also introduce the following rules: X ← Y 1 (v i (1)), . . . , Y n (v i (n)), sw (l 1 ), sw X,vi . . .
Non-Boolean Random Variables with parents. Let X be a non-boolean random variable X with domain {q 1 , . . . , q m } and parents p(X) = {Y 1 , . . . , Y n }, cpt(X) be the function associated with X, and v 1 , . . . , v m be all possible assignments to the variables in p(X). We introduce m fresh predicate symbols sw X,v1 , . . . , sw X,vm . For each v i , we introduce the probabilistic atom c i ::sw X,vi , where cpt(X)(v i , ) = c i . Finally, for each v i , we also introduce the following rules: p i 1 ::X(q 1 ); . . . ; p i m ::X(q m ) ← Y 1 (v i (1)), . . . , Y n (v i (n)), sw (l 1 ), sw X,vi . . . p i 1 ::X(q 1 ); . . . ; p i m :: if v ∈ { , ⊥}, l 1 , . . . , l 2 i−1 are all possible values in { , ⊥} i−1 , sw (l 1 , . . . , l i−1 ) is the list of literals sw X,v1 (l 1 ), . . . , sw X,vi−1 (i − 1), and cpt(v i , q j ) = p i j . Correctness of the encoding. The encoding presented above encodes the CPTs for the random variables. The probability that a random variable X has value v is exactly the same as the probability associated with the ground literal X(v) (with the notation defined above). The encoding for variables without parents directly encodes the corresponding CPTs. For variables with parents, the only non-standard part is the use of sw (l 2 i−1 ), sw X,vi . Note, however, that the literals in sw (l 2 i−1 ) do not influence the derivation since there is a rule for any possible values for them. We need them only for the encoding. Therefore, also the encoding of random variables with parents directly encodes the corresponding CPTs.
Relaxed Acyclicity. Let p be the program produced by the above construction. It is easy to see that all predicates associated with non-boolean random variables are CPT-like (as we just encoded their CPTs). Therefore, the program β(p) is obtained by removing all constant values associated with the domains of non-boolean random values. Finally, the program α(β(p)) collapses the rules for random variables with parents into a single rule (this follows from our construction and the use of sw (l 2 i−1 ), sw X,vi in the rules' bodies). The acyclicity of p = α(β(p)) follows from (1) p does not contain freevariables (i.e., both the literals and the ground atoms are only propositional facts), (2) bn is a forest of poly-trees, and (3) each predicate symbol sw X,vi occurs only in the rule of X.
From (1), it follows that all rules are both strongly and weakly connected. From (2) and (3), it follows that (a) there are no directed cycles in graph(p), and (b) for all undirected cycles U in graph(p), there are U , U such that U is equivalent to U · U and U is P r,i ←− P r,i −→ P for some P, P , r, i. Since all rules are both strongly and weakly connected, it directly follows that the undirected unsafe structure P r,i −→ P , P r,i −→ P , P , U is guarded. Therefore, p is acyclic and p is a relaxed acyclic PROBLOG program. all rules in PL(φ) are both strongly and weakly connected for U, it follows that there is always unguarded unsafe structure S that can be obtained from S by removing the rules in PL(φ). This contradicts the fact that p is a relaxed acyclic program.
Here, we show that for acyclic ATKLOG models, ANGERONA has PTIME data complexity.
Proposition C.7. Let C be a system configuration and f be the PDP shown in Figure 4. For any acyclic C-ATKLOG model ATK , any action (u, q) such that q is a literal query compatible with p, and any run r ∈ runs(C, f ) such that (1) all sentences in knowledge(r.h, u), for any u ∈ r.U , are literal queries compatible with p, and (2) all secrets in r.S are literal queries compatible with p, the algorithm shown in Figure 4 has PTIME data complexity.
Proof. Let B be the PROBLOG program obtained from ATK . The data complexity of f is its complexity when only the database r.db and edb(B) change. The algorithm in Figure 4 calls three times the secure procedure and twice the pox procedure. The set knowledge(h, u) can be constructed in O(|h|). From this, it follows that the program p has size O(|edb(B)| + |rules(B)| + |h|). Furthermore, since all queries are literal queries, B is a relaxed acyclic PROBLOG program, and Proposition C.6, it follows that p is a relaxed acyclic PROBLOG program as well. From this and Proposition B.18, the inference can be performed in O(r 2 · e r · max (2, r) 2+r ), where r ∈ O(|rules(B)| + (|r| + |edb(K)|) |rules(K)| ) and e ∈ O(|edb(B)|). Since rules(B), r, and K are fixed, then the data complexity of the secure procedure is O(|edb(B)| k ), for some k ∈ N. From this and the fact that Algorithm 4 three times the secure procedure and twice the pox procedure per secret in r.S, it follows that the data complexity of Algorithm 4 is PTIME.

D. Completeness Proof
We first introduce the notion of unconditionally secrecypreserving query. Informally, a query u , q is unconditionally secrecy-preserving given a run r and a secret u, ψ, l iff disclosing the result of u , q in any run r ∼ u r does not violate the secret.
We say that a PDP is complete if it authorizes all unconditionally secrecy-preserving queries. ANGERONA is complete. This directly follows from (1) Proposition C.2, (2) the use of exact inference procedures for PROBLOG programs, and (3) the fact that ANGERONA directly checks whether queries are unconditionally secrecy-preserving or not.