Probabilistic logic programs are logic programs in which some of the clauses are annotated with probabilistic facts. The behaviour of relations in these clauses can be very complex, leading to scalability issues. Asymptotic representations, in which queries are completely independent of the domain size and which approximate a probabilistic logic program on large domains, allow us to gain an understanding on how a probabilistic logic programs will behave for increasing domain sizes, and can be computed without actually having to execute the logic program. In particular, every probabilistic logic program under the distribution semantics is asymptotically equivalent to an acyclic probabilistic logic program consisting only of determinate clauses over probabilistic facts. We present asymptoticplp, a Prolog implementation of an algorithm which computes this. The transformation proceeds in several, modular steps which are of independent interest. These steps include rewriting the probabilistic logic program to a formula of least fixed point logic and then applying asymptotic quantifier elimination on the formula. Quantifier-free first-order formulas are then rewritten as acyclic determinate stratified DATALOG formulas, which together with the original probabilistic facts form a (probabilistic) logic program.
The asymptotic theory of finite structures has been studied for more than half a century,
beginning with the 1969 work of Glebskii et al. [
In the succeeding years, least fixed point logic as investigated by Blass et al. was related to
logic programs, and in 1991 Abiteboul and Vianu [
Probabilistic logic programming under the distribution semantics, established independently
in the early 1990s by Poole [
By viewing a probabilistic logic program as a deterministic Datalog program over independent
probabilistic facts, the distribution semantics allows the rich theory developed by logicians over
decades of studying finite models to be brought to bear on the analysis of probabilistic logic
programs. In particular, the second author [6, Theorem 27] recently showed that the analysis of
Blass et al. [
The relevance of this can be seen by considering the complexity of inference: In general, computing the probability of atomic queries even in acyclic probabilistic logic programs is intractable in the size of the underlying domain, as it generalises first-order model counting, which is known to be intractable. However, if the probabilistic logic program is determinate, then the situation changes completely. In this case, the probability of an atomic query is actually completely independent of the size of the underlying domain and can therefore be calculated in constant time, disregarding the domain entirely.
In this contribution, we report on asymptoticplp, an implementation in SWI-Prolog of the transformation of a probabilistic logic program into an asymptotically equivalent determinate program. We outline the relevant theory, describe the system as it is available and with its current limitations as a research prototype, explain the rationale behind the algorithms used for its individual steps and briefly discuss our experiences and the relevance of the implementation to probablistic logic programming and beyond.
Our outline of the theory closely follows [
This paper follows the notation of Ebbinghaus and Flum [
Let be a first-order formula. An occurrence of a variable in is called bound if it is in the scope of a quantifier annotated with that variable and free otherwise. is called free in if it occurs freely. We use the notation (1, . . . , ) for to assert that every free variable in is from 1, . . . , . We also abuse notation and write (⃗, ⃗) for an atomic formula with constants ⃗ and free variables ⃗, even though they don’t necessarily appear in that order. A formula with no free variables is called a sentence, and a set of sentences is called a theory. Sentences making up a given theory are also called its axioms.
Since tuples such as 1, . . . , occur frequently and their exact length is often not important, we use the notation ⃗ to indicate a tuple of arbitrary finite length in many contexts.
If is a vocabulary, then an -structure consists of a finite non-empty set , the domain of , along with an interpretation of the relation symbols and constants of as relations and elements of respectively. If is a relation symbol and a constant, then we and for their respective interpretations in . Let be an -structure, let (1, . . . , ) be a ifrst-order -formula and let 1, . . . , be a tuple of elements of the domain of . Then we write |= (1, . . . , ) whenever (1, . . . , ) holds with respect to the interpretation of 1, . . . , for 1, . . . , and call a model of (1, . . . , ).
Our terminology for logic programs is taken from Ebbinghaus and Flum [
A general logic program in a vocabulary is a finite set Π of clauses of the form ← 1, . . . , , where ≥ 0, is an atomic formula and 1, . . . , are literals. We call the head and 1, . . . , the body of the logic program. The intensional relation symbols are those that occur in the head of any clause of a program, while the relation symbols occurring only in the body of clauses are called extensional. We write (, Π) ext for the extensional vocabulary, or ext where the logic program is clear from context.
An acyclic logic program is one in which no intensional relation symbol occurs in the body of any clause (This is at first glance a stronger condition than the usual definition of acyclicity, but by successively unfolding head atoms used in the body of a clause, every acyclic logic program in the usual sense can easily be brought to this form).
A pure Datalog program is a general logic program in which no intensional relation symbol appears within any negated literal. To afix a meaning to a pure Datalog program, consider it as a function which take as input a finite ext-structure and returns as output an extension Π of to . Starting from an empty interpretation of the relation symbols not in ext, we successively expand them by applying the rules of Π . We give an informal description of this process:
Let (⃗) be the head of a clause and 1(⃗, ⃗), . . . , (⃗, ⃗) the body, and let ⃗ be a tuple of elements of the domain of length equal to ⃗. Then whenever there is a tuple ⃗ such that |= (⃗, ⃗) for every , we add (⃗) to the interpretation of the relation symbol of the atom . Successively proceed in this manner until nothing can be added by applying any of the clauses of Π . Since the domain of is finite, this is bound to happen eventually.
As the restriction for no intensional relation symbol to occur negated in the body of a clause turns out to be too strong for many practical applications, we consider a generalisation to stratifiable Datalog programs. A general logic program Π in a vocabulary is called a stratifiable Datalog program if there is a partition of into subvocabularies ext = 0, . . . such that the following holds:
The corresponding logic programs Π 1, . . . , Π , where Π is defined as the set of clauses whose head atom starts with a relation symbol from , are pure Datalog programs, and the extensional vocabulary of Π is contained in 0 ∪ · · · ∪ − 1.
If Π is a stratifiable Datalog program in and an ext-structure, then is obtained by applying Π 1, . . . , Π successively.
A (pure/stratifiable) Datalog formula is an expression of the form (Π , )⃗, where Π is a (pure/stratifiable) Datalog program, an intensional relation symbol and ⃗ a tuple of variables. We say that a Datalog formula holds in an ext-structure for a tuple of elements ⃗ of the same length as ⃗, written |= (Π , )⃗, if (⃗) is true in Π.
Our discussion on probabilistic logic programming considers a probabilistic logic program under
the distribution semantics, as a stratifiable Datalog program over probabilistic facts. This covers
several diferent equally expressive formalisms [
Definition 1. A probabilistic logic program consists of probabilistic facts and deterministic rules, where the deterministic part is a stratifiables Datalog program. We consider it in our framework of abstract distribution semantics as follows:
ℛ is given by relation symbols ′ for every probabilistic fact :: (⃗), with ′ := . Their arity is just the arity of .
is given by the vocabulary of the probabilistic logic program and additionally the ′ in ℛ.
Let Π be the stratifiable Datalog program obtained by prefixing the program {′(⃗) ← (⃗)|′ ∈ ℛ} to the deterministic rules of the probabilistic logic program.
Then for a ∈ ∖ℛ is given by (Π , )⃗.
Notation. Although we have allowed second-order variables in the inductive definitions above, we will assume from now on unless mentioned otherwise that LFP formulas do not have free second-order variables.
We will now proceed briefly to discuss fixed point logics, which extend ordinary first-order
logic with support for recursion. Modelling Datalog programs within fixed-point logic has a
long history in database theory, starting with work by Abiteboul and Vianu in the late 1980s
[
As atomic second-order formulas occur, as subformulas of least fixed point formulas, we will introduce second-order variables.
Definition 2. Assume an infinite set of second-order variables, indicated customarily by uppercase letters from the end of the alphabet, each annotated with a natural number arity. Then an atomic second-order formula is either a (first-order) atomic formula, or an expression of the form (1, . . . , ), where is a second-order variable of arity and 1, . . . , are constants or (first-order) variables.
Definition 3. A formula is called positive in a variable if is in the scope of an even number of negation symbols in .
A formula in least fixed point logic or LFP formula over a vocabulary ℛ is defined inductively as follows: 1. Any atomic second-order formula is an LFP formula. 2. If is an LFP formula, then so is ¬ . 3. If and are LFP formulas, then so is ∨ 4. If is an LFP formula, then so is ∃ for a first-order variable . 5. If is an LFP formula, then so is [LFP⃗, ]⃗, where is positive in the second-order variable and the lengths of the string of first-order variables ⃗ and the string of terms ⃗ coincide with the arity of .
An occurrence of a second-order variable is bound if it is in the scope of an LFP quantifier LFP⃗, and free otherwise.
Fixed point semantics have been used extensively in logic programming theory, and we will exploit this when relating the model theory of LFP to probabilistic logic programming below.
We first associate an operator with each LFP formula : Definition 4. Let (⃗, ⃗, , ⃗ ) be an LFP formula, with the length of ⃗ equal to the arity of , and let be an ℛ-structure with domain . Let ⃗ and ⃗ be an interpretation of ⃗ and ⃗ respectively. Then we define the operator : P() → P() as follows: () := {︁⃗ ∈ | |= (⃗, ⃗, , ⃗)}︁ .
Since we have restricted Rule 5 in Definition 3 to positive formulas, is monotone for all (i. e. ⊆ () for all ⊆ ). Therefore we have: Fact 1. For every LFP formula (⃗, ⃗, , ⃗ ) and every ℛ-structure on a domain and interpretation of variables as in Definition 4, there is a relation ⊆ such that = () and that for all ′ with ′ = (′) we have ⊆ ′.
Definition 5.
We call the from Fact 1 the least fixed point of (⃗, ⃗, , ⃗ )
Now we are ready to define the semantics of least fixed point logic: Definition 6. By induction on the definition of an LFP formula, we define when an LFP formula (⃗, ⃗) is said to hold in an ℛ-structure for a tuple ⃗ from the domain of and relations ⃗ of the correct arity:
The first-order connectives and quantifiers ¬, ∨ and ∃ as well as ∧ and ∀ defined from them in the usual way are given the usual semantics.
An atomic second order formula (⃗, ⃗) holds if and only if (⃗, ⃗) ∈ . [LFP⃗, ]⃗ holds if and only if ⃗ is in the least fixed point of (⃗,).
Least fixed point logics are related to logic programming by the following fact [ 7, Theorem 9.1.1]: Fact 2. For every stratifiable Datalog formula (Π , )⃗ as above, there exists an LFP formula (⃗) over the extensional vocabulary ℛ of Π such that for every ℛ-structure and every tuple ⃗ of elements of of the same length as ⃗, |= (⃗) if and only if |= (Π , )⃗.
As we are interested in the asymptotic behaviour of formulas, we introduce the notion of abstract families of distributions: Definition 7. A family of distributions for a relational vocabulary is a sequence (︀ ())︀ ∈N of probability distributions on the set Ω of all -structures with domain {1, . . . , } ⊆ N.
Such families are induced by logical formulas (or logic programs) and probabilistic facts as follows.
Definition 8. Let be a relational vocabulary, ℛ ⊆ , and let (ℛ) be a logical language over
ℛ. Then an abstract -distribution over ℛ (with vocabulary ) consists of the following data:
For every ∈ ℛ a number ∈ Q ∩ [
For every ∈ ∖ℛ, an (ℛ)-formula of the same arity as .
In the following we will assume that all vocabularies are finite. The semantics of an abstract distribution is only defined relative to a domain , which we will also assume to be finite. The formal definition is as follows: Definition 9. Let (ℛ) be a logical language over ℛ and let be a finite set. Let be an abstract -distribution over ℛ. Let Ω be the set of all ℛ-structures with domain . (), is defined as follows: Then the probability distribution on Ω induced by , written For all ∈ Ω , if ∃⃗∈⃗∃∈∖ℛ : (⃗) ⇎ (⃗), then ()({}) := 0 Otherwise, ()({}) := ∏︀ (|{⃗∈⃗|(⃗)}|) × ∏︀ (1 − )|{⃗∈⃗|¬(⃗)}|
∈ℛ ∈ℛ
In other words, all the relations in ℛ are independent with probability and the relations in ∖ ℛ are defined deterministically by the (ℛ)-formulas . We will illustrate that with an example.
Example 1. Let ℛ = {, }, = {, , }, for a unary relation a binary relation and a unary relation . Then an abstract distribution over () has numbers and which encode probabilities. Consider the first-order distribution with = ∃ (() ∧ (, )). For any () is obtained by making an independent choice of () or ¬() for every domain , ∈ , with a probability of (). Similarly, an independent choice of (, ) or ¬ (, ) is made for every pair (, ) from 2, with a probability of (, ). Then, for any possible ℛ-structure, the interpretation of is determined by ∀() ↔ ().
We introduce our notion of asymptotic equivalence for families of distributions: Definition 10. Two families of distributions (()) and (′()) are asymptotically equivalent if lim sup |()() − ′()()| = 0 →∞⊆ Ω
Definition 11. Let (ℛ) be an extension of the class of quantifier-free ℛ-formulas. Then (ℛ) has asymptotic quantifier elimination if every abstract (ℛ) distribution is asymptotically equivalent to a quantifier-free distribution over (ℛ).
Building on prior work by Glebskii et al. [
To obtain a characterisation within probabilistic logic programming, however, we need to translate quantifier-free first order formulas back to stratifiable Datalog.
In fact, they can be mapped to a subset of stratifiable Datalog that is well-known from logic programming: Definition 12. A Datalog program, Datalog formula or probabilistic logic program is called determinate if every variable occurring in the body of a clause also occurs in the head of that clause.
Example 2. Examples of determinate clauses in this sense are () :− () or (, ) :− (). Indeterminate clauses include () :− () or () :− (, ).
Determinacy corresponds exactly to the fragment of probabilistic logic programs identified as projective by Jaeger and Schulte [9, Proposition 4.3].
Indeed, Ebbinghaus and Flum’s [
This leads to the main result of this subsection, the implemented transformation. Theorem 2. Every probabilistic logic program is asymptotically equivalent to an acyclic determinate probabilistic logic program.
asymptoticplp is an SWI-Prolog program, available at https://swish.swi-prolog.org/p/asymptoticPLP.pl and entirely written in SWI-Prolog.
The main entry point into the program is the predicate compute_lp_form/3, to be used with the first argument instantiated to the deterministic part of the program to be approximated, and the second argument instantiated to the query predicate. The third argument is then bound to a determinate logic program such that when readding the probabilistic facts, the resulting probabilistic logic program is asymptotically equivalent to the original program on large domains with respect to the query predicate.
Programs are represented as lists of clauses of the form head− vars− body, where variables are rendered as ordinary lowercase Prolog atoms.
Example 3. Consider the example of connectedness in a probabilistic graph. Here, we have a random graph with edge relation edge/2, true for any pair of nodes with fixed probability ∈ (0, 1). This can be expressed with a probabilistic fact such as 0.5 :: edge(X,Y ). Connectedness of two nodes is then expressed by the usual Datalog clauses, c o n n e c t e d ( X , Y ) : − c o n n e c t e d ( X , Z ) : − e d g e ( X , Y ) .
c o n n e c t e d ( X , Y ) , e d g e ( Y , Z ) .
In the representation used by the system, the program is given by the list [ c o n n e c t e d − [x , y ] − [ edge − [x , y ] ] ,
c o n n e c t e d − [x , z ] − [ c o n n e c t e d − [x , y ] , edge − [y , z ] ] ]
Informally, we can argue that in a suficiently large random graph, there will always be for any two nodes and a third node such that is adjacent to and is adjacent to . Thus, we expect that asymptotically, any two nodes will be connected.
This is confirmed by computation in the system, which returns connected− [x,y]− [], its notation for a clause with empty body which is unconditionally true.
Example 4. A probabilistic logic programming classic is the “friends-smokers model”. In this program, there is a random graph of friendship connections between diferent people. Additionally, there is a certain baseline probability of anyone starting smoking. Then, whenever a person befriends another and that person smokes, there is a certain probability that this person also takes up smoking. We thus have a random graph with edge relation friends /2, true for any pair of nodes with fixed probability ∈ (0, 1). This can be expressed with a probabilistic fact such as 0.3 :: friends (X,Y ).
Using the syntactic sugar of probabilistic clauses, we can write the remaining model as follows: 0 . 1 : : smokes ( X ) . 0 . 2 : : smokes ( X ) : −
f r i e n d s ( X , Y ) , smokes ( Y ) .
This encodes a probabilistic logic program with auxiliary predicates u/1 and v/2 as follows: smokes ( X ) : − smokes ( X ) : − u ( X ) .
f r i e n d s ( X , Y ) , smokes ( Y ) , v ( X , Y ) .
Informally, we can see that in a suficiently large group of people in which everyone has a certain chance to smoke and to be your friend, there is bound to be someone who smokes and is your friend; in fact, there are bound to be any number of such people, and one of them will convince you to take up smoking.
This is confirmed by computation in the system, which returns smokes− [x]− [], its notation for a clause with empty body which is unconditionally true.
However, consider an altered model where only nice people have friends: smokes ( X ) : − smokes ( X ) : − f r i e n d s ( X , Y ) : − 0 . 1 : : u ( X ) . 0 . 2 : : v ( X , Y ) . 0 . 3 : : w( X , Y ) .
u ( X ) . f r i e n d s ( X , Y ) , smokes ( Y ) , v ( X , Y ) .
n i c e ( X ) , w( X , Y ) .
In this model, the reasoning above only works for nice people. This leads us to conclude that the only people who smoke are either those who take up the habit on their own accord, or are nice enough to have friends.
This is again confirmed by the system, which delivers a program equivalent to [smokes− [x]− [u− [x]], smokes− [x]− [nice− [x]]].
As explained in greater detail in Section 4, the system procedes by converting the input program into an equivalent least fixed point formula and then using asymptotic quantifier elimination to eliminate all uses of the fixed point quantifier and all classical existential and universal quantifiers in the resulting formula. Since to the best of our knowledge this is the ifrst implementation of both conversion to formulas and asymptotic quantfier elimination, asymptoticplp also provides predicates that perform those steps in isolation.
To understand how these are invoked, one needs only to understand the representation used for formulas of first-order logic and for least fixed point quantifiers. We tried to facilitate use by adopting a natural syntax, which is best understood from example: l f p ( c o n n e c t e d , edge − [x , y ] or e x i s t s ( [ a t ] , c o n n e c t e d − [x , a t ] and edge − [ a t , y ] ) ) Existential and universal quantifiers are written using the term constructors exists /2 and forall /2, which take as their first argument a list of bound variables (potentially more than one to avoid unnecessary nesting of quantifiers) and as their second argument a formula. Boolean connectives use the infix constructors and/2 and or/2 and the term constructor not/1.
The least fixed point quantifier is represented by the constructor lfp /2, which takes as its ifrst argument the predicate with respect to which the fixed point is computed, and as its second argument a formula.
So the example formula above is the translation of Example 3 to a formula of least fixed point logic, and can be computed in the system using the predicate compute_lp_lfp/3, whose first argument is the logic program to be translated and whose second argument holds the target predicate, in this case connected.
Similarly, the system allows direct access to the asymptotic quantifier elimination algorithm for least fixed point formulas using the predicate compute_lfp_form/2, which takes as its first argument the least fixed point formula to be converted and binds the second argument to an asymptotically equivalent quantifier-free formula. The predicate reduced_quant_elim/2 behaves identically, but only works for first-order formulas. It is provided separately because of the relatively greater interest in the asymptotic theory of first-order logic by logicians and combinatoricists, and allows for optimisations to be added for this case in particular.
The system is currently a research prototype, with some limitations that should be overcome before it is more widely deployed. Constants in clause heads or bodies are not currently supported by the system. Furthermore, the single-letter atoms a, b, c, d, e, f, g and h are used by the system for substituting variables, and no two variable names should difer from each other by merely prefixing one of those letters. To be safe, it is recommended to begin variable names with letters later in the alphabet. Alternatively, or if in larger examples the system requires more variables to substitute, the system can also be invoked with the query predicate compute_lp_form/4, where the third argument holds the list of names to be used for forming substitute variables. Also, the system currently does not support overloading of predicate names within the probabilistic logic program, as it refers to predicates simply by name rather than with associated arities.
The algorithm proceeds in several stages, which have been described separately in the classical ifnite model theory literature. The overarching structure can be seen in the pseudo-code below. (Π 1, . . . , Π ) = S t r a t i f i c a t i o n ( Π ) f o r i =1 t o n
For i n t e n s i o n a l p r e d i c a t e s of Π , i n t e n s i o n a l p r e d i c a t e s 1, . . . , of Π f o r < Φ ( ) = L P _ t o _ S L F P ( Π , ) Φ ( ) = s u b s t i t u t e ( 1, . . . , , Φ (1), . . . , Φ () , Φ ( ) ) Φ = Φ( ) Ψ = S L F P _ t o _ L F P ( Φ ) Ψ 0 = ⊥ While Ψ + ≢ Ψ Ψ + = AQE ( S t e p ( Ψ ) ) Ψ = Ψ +
In the first part of the process, the logic program and query predicate are converted into a formula of least fixed point logic, a realisation of Fact 2.
This procedure has several stages. First, the program is explicitly stratified. Then, LP_to_SLFP
converts every stratum to a formula in simultaneous least fixed point logic . Simultaneous least
ifxed point logic is an intermediate formalism, in which the fixed point iteration is applied to a
number of first-order formulas simultaneously. Since this aligns closely with the operational
semantics of Datalog, constructing the equivalent formula in simultaneous least fixed point logic
reduces to an essentially syntactic rewrite. The procedure employed by us is a generalisation of
Clark’s Completion [
Predicates from lower strata are then successively substituted until the final stratum has been converted into a simultaneous least fixed point logic formula all of whose predicates lie in the extensional vocabulary of Π .
SLFP_to_LFP then converts the simultaneous least fixed point formula into an ordinary least ifxed point formula in the sense of Subsection 2.4.
While simultaneous fixed points do not increase the expressivity of fixed point logic, their
removal comes at a cost. There are two classical ways to replace them with ordinary fixed point
quantifiers, either increasing the arities of the predicates involved or increasing the nesting
depth of the fixed point quantifiers. Following Kreutzer [ 11, page 40], we have decided to
implement the latter algorithm going back to Bekić [
Following the asymptotic analysis of Blass et al. [
We first turn to the elimination of the least fixed point constructor. The algorithm implicit
in Blass et al. [
Given a first-order formula, AQE computes an asymptotically equivalent quantifier-free
one. Several classical algorithms for this can be found in the theoretical literature. In terms of
complexity, an optimal approach was given by Grandjean [
Although Grandjean [
Thus, we simplify the formulas considerably as we unfold the iteration rule and can reduce checking the termination condition of the iteration to checking the satisfiability of a quantifierfree formula, which can easily be implemented using SAT-solving techniques.
The system presented here allows users to test the asymptotic behaviour of probabilistic logic programs on large domains statically without running them on large databases. This is particularly important for probabilistic logic programs since the complexity of probabilistic inference makes querying large domains with general programs intractable. The asymptotically equivalent determinate programs computed by the system evaluate queries independently of domain size, thereby allowing queries to be approximated statically without access to a particular domain. Thus, one could see the present system as a contribution to scalable approximate inference, with an approximation that converges to the correct result with exponential speed as the domain size increases.
Equally, static analysis of a probabilistic logic program can also be seen as a form of verification of certain properties. From this point of view, asymptoticplp allows for a “sanity check” that the behaviour of a program on large domains matches the behaviour expected by the programmer. For instance, a program that predicts disease transmission in a group of people may well be expected to predict increased infection rate with an increase in population size. This can easily be verified with asymptoticplp. Overall, static analysis tools for probabilistic logic programs are scarce, and therefore we hope that this system may inspire other approaches to be implemented efectively.
While the worst-case complexity of computing the asymptotically equivalent quantifier-free
formulas for a given formula in least fixed point logic is EXPTIME-complete [
Beyond the relevance for probabilistic logic programming proper, this system is to the best of our knowledge the first practical implementation of any decision or quantifier elimination procedure for the theory of almost all finite structures, whether for first-order logic or for ifxed point logic. It can be hoped that researchers in finite model theory, database theory and the combinatorics of random graphs find it useful to be able to evaluate the asymptotics of properties of random graphs efectively.
The encouraging runtime for sample programs also points to the importance of interleaving iteration and quantifier elimination steps, an insight that may inspire similar eforts aimed at evaluating least fixed point formulas in other theories with first-order quantifier elimination but daunting complexity, such as the theory of the rational order or the theory of real-closed and algebraically closed fields.
Similar results on limiting approximations have been obtained for formalisms outside of
probabilistic logic programming. This includes Cozman and Maua’s Bayesian networks
specifications [
Our approach to implementation is not immediately transferable to relational Bayesian networks since it is based on the clear distinction between logical and probabilistic part inherent in probabilistic logic programs, as well as on the sophisticated logical description of Datalog semantics developed in the literature. Additionally, arguably the key contribution of our implementation concept is the ability to deal with recursive programs via fixed point logic, while Bayesian networks and similar formalisms based on directed graphical models are inherently acyclic.
Currently, an important limitation of the system is that it does not natively support named
domain constants in probabilistic logic programs. As explained by Ebbinghaus and Flum [
Performance could be improved by replacing the current satisfiability check within the termination condition with a state-of-the-art SAT solver, which could simply be grafted into the definition of the notsat /1 predicate.
Overall, the system provides a tool for modellers and deployers of probabilistic logic programs statically to evaluate the behaviours of programs on large domains, while at the same time providing insights into the relevance of quantifier elimination for the eficient evaluation of least fixed point formulas. While the current limitations, particularly the lack of support for constants in formulas, somewhat limit its scope, the prototype shows the promise of the method despite the seemingly prohibitive worst-case complexity of the problem.
During the work leading up to this publication, the second author was supported by LMUexcellent, funded by the Federal Ministry of Education and Research (BMBF) and the Free State of Bavaria under the Excellence Strategy of the Federal Government and the Länder. logistic regression models, CoRR abs/2103.15140 (2021). arXiv:2103.15140. [19] V. Koponen, Conditional probability logic, lifted bayesian networks, and almost sure quantifier elimination, Theor. Comput. Sci. 848 (2020) 1–27. doi: 10.1016/j.tcs.2020. 08.006. [20] F. Weitkämper, Statistical relational artificial intelligence with relative frequencies: A contribution to modelling and transfer learning across domain sizes, CoRR abs/2202.10367 (2022). arXiv:2202.10367. [21] V. Koponen, F. Weitkämper, Asymptotic elimination of partially continuous aggregation functions in directed graphical models, Information and Computation 293 (2023) 105061. doi:10.1016/j.ic.2023.105061. [22] V. Koponen, F. Weitkämper, On the relative asymptotic expressivity of inference frameworks, CoRR abs/2204.09457 (2022). doi:10.48550/arXiv.2204.09457. arXiv:2204.09457.