Strong equivalence for $\rm LP^{MLN}$ programs

TL;DR

This paper extends the concept of strong equivalence to $ m LP^{MLN}$, a probabilistic logic programming framework, by reducing the problem to classical logic equivalence checking, enabling more effective program analysis.

Contribution

It introduces a method to verify strong equivalence in $ m LP^{MLN}$ using classical logic tools and proposes reformulations of its semantics for better understanding.

Findings

Verification of strong equivalence reduces to classical logic equivalence checking.

Leverages answer set solvers for strong equivalence verification in $ m LP^{MLN}$.

Proposes reformulations of $ m LP^{MLN}$ semantics using various logical frameworks.

Abstract

Strong equivalence is a well-studied and important concept in answer set programming (ASP). $\rm LP^{MLN}$ is a probabilistic extension of answer set programs with the weight scheme adapted from Markov Logic. Because of the semantic differences, strong equivalence for ASP does not simply carry over to $\rm LP^{MLN}$. I study the concept of strong equivalence in $\rm LP^{MLN}$ with the goal of extending strong equivalence to $\rm LP^{MLN}$ programs. My study shows that the verification of strong equivalence in $\rm LP^{MLN}$ can be reduced to equivalence checking in classical logic plus weight consideration.The result allows us to leverage an answer set solver for checking strong equivalence in $\rm LP^{MLN}$. Furthermore, this study also suggests us a few reformulations of the $\rm LP^{MLN}$ semantics using choice rules, logic of here and there, and the second-order logic. I will present my work result of strong equivalence for $\rm LP^{MLN}$ and talk about my next steps for research: one is approximately strong equivalence, and another is the integration of fuzzy logic with neural network.

Tables

Table 1. Table 1: ( 𝖥 X ¯ ) X superscript ¯ subscript 𝖥 𝑋 𝑋 (\overline{{\mathsf{F}}_{X}})^{X} and ( 𝖦 X ¯ ) X superscript ¯ subscript 𝖦 𝑋 𝑋 (\overline{{\mathsf{G}}_{X}})^{X}

$X$	$TW\left({𝖥}_X\right)$	$TW\left({𝖦}_X\right)$	${\left(\overline{{𝖥}_X}\right)}^X$	${\left(\overline{{𝖦}_X}\right)}^X$
$\varphi$	$e^5$	$e^3$	$\top$	$\top$
$\left\{a\right\}$	$e^3$	$e^1$	$a$	$a$
$\left\{b\right\}$	$e^5$	$e^3$	$\top$	$\top$
$\{a,b\}$	$e^5$	$e^3$	$a\wedge b$	$a\wedge b$

Equations

$$\begin{array}[]{l}\{X\mid\text{$X$ is a (standard) stable model of $\overline{{\mathsf{F}}_{X}}$}\}.\end{array}$$

$$W_{\mathsf{F}}(X)=\{\begin{array}{ll}TW\text{/}({\mathsf{F}}_{\mathsf{X}})& \text{if X∈SM[F]};\\ 0& \text{otherwise},\end{array}$$

$$P_{\mathsf{F}}(X)=\underset{\alpha \to \infty }{\lim }\frac{W_{\mathsf{F}}(X)}{\sum _{Y\in \mathrm{SM}[\mathsf{F}]}{W}_{\mathsf{F}}(Y)}.$$

$$P_{\mathsf{F}\cup \mathsf{H}}(X)=P_{\mathsf{G}\cup \mathsf{H}}(X)$$

$$\begin{array}[]{lrcllrcl}{\mathsf{F}{}{}}&0:&\neg a&&{\mathsf{G}{}{}}&2:&\neg a\lor b\\ &2:&b\leftarrow a&&&1:&a\lor\neg a\\ &3:&a\leftarrow\neg\neg a\\ \end{array}$$

$$\mathsf{H}=\{1:a\leftarrow b,1:b\leftarrow a\}$$

Full text

1 Introduction

${\rm LP}^{\rm{MLN}}$ is a probabilistic extension of answer set programs with the weight scheme adapted from Markov Logic [7]. An ${\rm LP}^{\rm{MLN}}$ program defines the probability distribution over all “soft” stable models, which do not necessarily satisfy all rules in the program, but the more rules with the bigger weights they satisfy, the bigger their probabilities.

${\rm LP}^{\rm{MLN}}$ turns out to be highly expressive to embed several other probabilistic logic languages, as more results are built upon ${\rm LP}^{\rm{MLN}}$, it becomes more important to consider the equivalence between different ${\rm LP}^{\rm{MLN}}$ programs. As with answer set programs, ${\rm LP}^{\rm{MLN}}$ programs ${\mathsf{F}}$ and ${\mathsf{G}}$ that have the same soft stable models with the same probability distribution are not necessarily equivalent in a stronger sense. When we add the same program ${\mathsf{H}}$ to each of ${\mathsf{F}}$ and ${\mathsf{G}}$, the resulting programs may have different soft stable models and different probability distributions.

However, because of the semantic differences, strong equivalence for answer set programs does not simply carry over to ${\rm LP}^{\rm{MLN}}$. Based on this observation, I study the notion of strong equivalence for ${\rm LP}^{\rm{MLN}}$ and characterize this concept.

The paper is organized as follows: Section 2 presents the background of my research. Section 3 explains the central question of my research. Section 4 shows the main accomplishment of my current work and the plan for the future work.

2 Background: Language ${\rm LP}^{\rm{MLN}}$

An ${\rm LP}^{\rm{MLN}}$ program is a finite set of weighted formulas $w:R$ where $R$ is a propositional formula and $w$ is a real number (in which case, the weighted rule is called soft) or $\alpha$ for denoting the infinite weight (in which case, the weighted rule is called hard).

For any ${\rm LP}^{\rm{MLN}}$ program ${\mathsf{F}}$ and any set $X$ of atoms, $\overline{{\mathsf{F}}}$ denotes the set of usual (unweighted) formulas obtained from ${\mathsf{F}}$ by dropping the weights, and ${\mathsf{F}}_{X}$ denotes the set of $w:R$ in ${\mathsf{F}}$ such that $X\models R$.

Given an ${\rm LP}^{\rm{MLN}}$ program ${\mathsf{F}}$, $\rm SM[{\mathsf{F}}]$ denotes the set of soft stable models:

[TABLE]

By $\hbox{TW\/}({\mathsf{F}})$ (“Total Weight” of ${\mathsf{F}}$) we denote the expression $exp({\sum\limits_{w:R\in{\mathsf{F}}}w})$. For any interpretation $X$, the weight of an interpretation $X$, denoted $W_{{\mathsf{F}}}(X)$, is defined as

[TABLE]

and the probability of $X$, denoted $P_{\mathsf{F}}(X)$, is defined as

[TABLE]

3 Central Question: Strong Equivalence for ${\rm LP}^{\rm{MLN}}$

Strong equivalence is an important concept in the theory of answer set programming. Informally speaking, logic programs ${\mathsf{P}}$ and ${\mathsf{Q}}$ are strongly equivalent if, given any program ${\mathsf{R}}$, programs ${\mathsf{P}}\cup{\mathsf{R}}$ and ${\mathsf{Q}}\cup{\mathsf{R}}$ have the same stable models. On the other hand, Logic of Here and There (logic $HT$) is proven to be useful for a monotonic basis for checking strong equivalence [5], and equilibrium models [6] are defined as a special class of minimal models in logic $HT$.

However, because of the semantic differences, strong equivalence for answer set programs does not simply carry over to ${\rm LP}^{\rm{MLN}}$. First, weights play a role. Even for the same structure of rules, different assignments of weights make the programs no longer strongly equivalent. Also, due to the fact that soft stable models do not have to satisfy all rules, strongly equivalent answer set programs do not simply translate to strongly equivalent ${\rm LP}^{\rm{MLN}}$ programs. For instance, $\{a\lor b,\ \ \bot\leftarrow a,b\}$ is strongly equivalent to $\{a\leftarrow\hbox{not\/}\ b,\ \ b\leftarrow\hbox{not\/}\ a,\ \ \bot\leftarrow a,b\}$, but its ${\rm LP}^{\rm{MLN}}$ counterpart $\{\alpha:a\lor b,\ \ \alpha:\bot\leftarrow a,b\}$ is not strongly equivalent to $\{\alpha:a\leftarrow\hbox{not\/}\ b,\ \ \alpha:b\leftarrow\hbox{not\/}\ a,\ \ \alpha:\bot\leftarrow a,b\}$: if we add $\{\alpha:a\leftarrow b,\ \ \alpha:b\leftarrow a\}$ to each of them, $\{a,b\}$ is a soft stable model of the former (by disregarding the rule $\alpha:\bot\leftarrow a,b$) but not of the latter

I extend the notion of strong equivalence to ${\rm LP}^{\rm{MLN}}$, and show that the verification of strong equivalence in ${\rm LP}^{\rm{MLN}}$ can be reduced to equivalence checking in classical logic plus weight consideration. We also extend the logic of here and there to weighted rules, which provides a monotonic basis of checking strong equivalence. The study of strong equivalence suggests us a few reformulations of the ${\rm LP}^{\rm{MLN}}$ semantics using choice rules, logic of here and there, and second-order logic, which present us useful insights into the semantics.

Definition 1 is the notion of strong equivalence in ${\rm LP}^{\rm{MLN}}$ in terms of probability distribution.

Definition 1

${\rm LP}^{\rm{MLN}}$ programs ${\mathsf{F}}$ and ${\mathsf{G}}$ are called strongly equivalent to each other if, for any ${\rm LP}^{\rm{MLN}}$ program ${\mathsf{H}}$,

[TABLE]

for all interpretations $X$.

The following theorem shows a characterization of strong equivalence that does not need to consider adding all possible ${\rm LP}^{\rm{MLN}}$ program ${\mathsf{H}}$, which can be reduced to equivalence checking in classical logic plus weight checking.

For any ${\rm LP}^{\rm{MLN}}$ program ${\mathsf{F}}$ and any set $X$ of atoms, $\overline{{\mathsf{F}}}$ denotes the set of usual (unweighted) formulas obtained from ${\mathsf{F}}$ by dropping the weights, and ${\mathsf{F}}_{X}$ denotes the set of $w:R$ in ${\mathsf{F}}$ such that $X\models R$.

Theorem 1

For any ${\rm LP}^{\rm{MLN}}$ programs ${\mathsf{F}}$ and ${\mathsf{G}}$, program ${\mathsf{F}}$ is strongly equivalent to ${\mathsf{G}}$ if and only if there is a w-expression $c$ such that for every interpretation $X$,

$TW({\mathsf{F}}_{X})=c\times TW({\mathsf{G}}_{X})$, and 2. 2.

$(\overline{{\mathsf{F}}_{X}})^{X}$* and $(\overline{{\mathsf{G}}_{X}})^{X}$ are classically equivalent.*

where $w$-expression is in the form of $e^{c_{1}+c_{2}\alpha}$, and $c_{1}$ is a real number counting the weight of soft rules, $c_{2}$ is an integer counting the weight of hard rules.

Example 1

Consider two programs

[TABLE]

Programs ${\mathsf{F}}$ and ${\mathsf{G}}$ are strongly equivalent to each other. The following table shows ${\mathsf{F}}$ and ${\mathsf{G}}$ statisfy two conditions in Theorem 1.

From the first and the second column, it is easy to see that $TW({{\mathsf{F}}_{X}})=e^{2}\times TW({\mathsf{G}}_{X})$, so the first condition in Theorem 1 is satisfied. The third and forth column show that the second condition in Theorem 1 is satisfied. However, if we replace rule   $3:\ \ a\leftarrow\neg\neg a$   in ${\mathsf{F}}$ with   $3:\ \ a\leftarrow a$   to result in ${\mathsf{F}}^{\prime}$, then ${\mathsf{F}}^{\prime}$ and ${\mathsf{G}}$ are not strongly equivalent: for

[TABLE]

$\{a,b\}$ is a soft stable model for ${\mathsf{G}}\cup{\mathsf{H}}$ with the weight $e^{5}$, but it is not a soft stable model for ${\mathsf{F^{\prime}}}\cup{\mathsf{H}}$, so its weight is 0. In accordance with Theorem 1, $(\overline{{\mathsf{F^{\prime}}}_{\{a,b\}}})^{\{a,b\}}$ is not equivalent to $(\overline{{\mathsf{G}}_{\{a,b\}}})^{\{a,b\}}$. The former is equivalent to $\{b\leftarrow a\}$, and the latter is equivalent to $\{a\land b\}$.

Even if the programs have the same soft stable models, the different weight assignments may make them not strongly equivalent. For instance, replacing the first rule in ${\mathsf{G}}$ by $3:\neg a\lor b$ to result in ${\mathsf{G}}^{\prime}$, we have $TW({\mathsf{F}}_{\phi})=e^{1}\times TW({\mathsf{G^{\prime}}}_{\phi})$ and $TW({\mathsf{F}}_{\{a\}})=e^{2}\times TW({\mathsf{G^{\prime}}}_{\{a\}})$, so there is no $w$-expression $c$ such that $TW({\mathsf{F}}_{X})=c\times TW({\mathsf{G^{\prime}}}_{X})$.

Based on the concepts of choice rules, logic HT[4] and the second order, we present the theorem on soft stable, in which every item is equivalent to each other. Before introducing the theorem, we define the definition of choice formula and $\Delta_{\bf P^{\prime}}(F)$. For any propositional formula $F$, by $\{F\}^{\rm ch}$ we denote the choice formula $F\lor\neg F$.

Let ${\bf p}$ be the propositional signature. Let ${\bf p}^{\prime}$ be the set of atoms $p^{\prime}$ where $p\in{\bf p}$. For any formula $F$, $\Delta_{{\bf p}^{\prime}}(F)$ is defined recursively:

• •

$\Delta_{{\bf p}^{\prime}}(p)=p^{\prime}$ for any atomic formula $p\in{\bf p}$;

• •

$\Delta_{{\bf p}^{\prime}}(\neg F)=\neg F$;

• •

$\Delta_{{\bf p}^{\prime}}(F\land G)=\Delta_{{\bf p}^{\prime}}(F)\land\Delta_{{\bf p}^{\prime}}(G)$;

• •

$\Delta_{{\bf p}^{\prime}}(F\lor G)=\Delta_{{\bf p}^{\prime}}(F)\lor\Delta_{{\bf p}^{\prime}}(G)$;

• •

$\Delta_{{\bf p}^{\prime}}(F\rightarrow G)=(\Delta_{{\bf p}^{\prime}}(F)\rightarrow\Delta_{{\bf p}^{\prime}}(G))\land(F\rightarrow G)$.

Theorem on Soft Stable Models

For any ${\rm LP}^{\rm{MLN}}$ program ${\mathsf{F}}$ and ${\mathsf{G}}$, the following conditions are equivalent. By ${\mathsf{F}}^{X}$, we denote the reduct of ${\mathsf{F}}$ obtained from ${\mathsf{F}}$ by replacing every maximal subformula of ${\mathsf{F}}$ that is not satisfied by $X$ with $\bot$.

1. (a)

For any ${\rm LP}^{\rm{MLN}}$ program ${\mathsf{H}}$, programs ${\mathsf{F}}\cup{\mathsf{H}}$ and ${\mathsf{G}}\cup{\mathsf{H}}$ have the same soft stable models. 2. (b)

For any set $X$ of atoms, $(\overline{{\mathsf{F}}_{X}})^{X}$ and $(\overline{{\mathsf{G}}_{X}})^{X}$ are classically equivalent. 3. (c)

For any set $X$ of atoms, $(\{\overline{{\mathsf{F}}}\}^{\rm ch})^{X}$ and $(\{\overline{{\mathsf{G}}}\}^{\rm ch})^{X}$ are classically equivalent. 4. (d)

${\mathsf{F}}$ and ${\mathsf{G}}$ have the same set of soft $HT$ models. 5. (e)

$(\{\overline{{\mathsf{F}}}\}^{\rm ch})\leftrightarrow(\{\overline{{\mathsf{G}}}\}^{\rm ch})$ is provable in $HT$. 6. (f)

For any set $X$ of atoms, $\{p^{\prime}\rightarrow p\mid p\in{\bf p}\}$ entails $\Delta(\overline{{\mathsf{F}}_{X}})\leftrightarrow\Delta(\overline{{\mathsf{G}}_{X}})$ (in the sense of classical logic). 7. (g)

$\{p^{\prime}\rightarrow p\mid p\in{\bf p}\}$ entails $\Delta(\{\overline{{\mathsf{F}}}\}^{\rm ch})\leftrightarrow\Delta(\{\overline{{\mathsf{G}}}\}^{\rm ch})$ (in the sense of classical logic).

4 Accomplishment and Future work

4.1 Accomplishment

Theorem 1 shows a characterization of strong equivalence that does not need to consider adding all possible ${\rm LP}^{\rm{MLN}}$ programs ${\mathsf{H}}$. Similar to Proposition 2 from [3], it shows that the verification of strong equivalence in ${\rm LP}^{\rm{MLN}}$ can be reduced to equivalence checking in classical logic plus weight checking.

I am still at the beginning stage in research. I get familiar with ${\rm LP}^{\rm{MLN}}$ language by the study of strong equivalence and it indeed gives me more insight and I feel quite interested in the area of knowledge representation and reasoning. In the following, I will show two interesting topics that I will investigate in my next step.

4.2 Future work

4.2.1 Approximate strong equivalent.

We plan to extend the work to approximate strong equivalence, where the probability distributions may not necessarily be identical but allowed to be slightly different with some error bound. Approximate strong equivalent for ${\rm LP}^{\rm{MLN}}$ will have more flexibility. One application of approximate strong equivalence is weight learning in ${\rm LP}^{\rm{MLN}}$. More specifically, due to the difference of initialized value of weights and the noise existing in the data, there is no guarantee that the weight learned from the data will be exactly the same. In such case, we should allow some certain bound so that the different set of weights can be approximate strong equivalence.

4.2.2 Integration of symbolic and sub-symbolic.

In symbolic systems, knowledge is encoded in terms of explicit structure(rules) and inferences are based on this structure(rules). Neural networks provide a powerful mechanism for learning patterns from massive data. Although neural network can learn the model from data, it has difficulty with high level reasoning. The integration of these two systems can take advantage from both sides: symbolic system can do the reasoning based on model, and neural networks can learn the model from the data. One obvious advantage of this integration is that the rules defined in symbolic system can ”guide” neural network learn the relation among data. Recently, more and more studies focus on this field, such as Neural tensor network(LTN)[2], TensorLog[1] etc. For instance, LTN is an interesting framework, in which it grounds the terms with vectors representing the features of the objects and grounds the clauses with real value in the interval [0,1] representing the truth degree of the clauses. By maximizing the truth degree of the clauses, LTN encodes the knowledge into neural networks. I am applying LTN to different tasks to get some insight with the goal of inventing an integration of symbolic and subsymbolic that works well for different domains.