Automated reasoning for attributed graph properties

Abstract

Graphs are ubiquitous in computer science. Moreover, in various application fields, graphs are equipped with attributes to express additional information such as names of entities or weights of relationships. Due to the pervasiveness of attributed graphs, it is highly important to have the means to express properties on attributed graphs to strengthen modeling capabilities and to enable analysis. Firstly, we introduce a new logic of attributed graph properties, where the graph part and attribution part are neatly separated. The graph part is equivalent to first-order logic on graphs as introduced by Courcelle. It employs graph morphisms to allow the specification of complex graph patterns. The attribution part is added to this graph part by reverting to the symbolic approach to graph attribution, where attributes are represented symbolically by variables whose possible values are specified by a set of constraints making use of algebraic specifications. Secondly, we extend our refutationally complete tableau-based reasoning method as well as our symbolic model generation approach for graph properties to attributed graph properties. Due to the new logic mentioned above, neatly separating the graph and attribution parts, and the categorical constructions employed only on a more abstract level, we can leave the graph part of the algorithms seemingly unchanged. For the integration of the attribution part into the algorithms, we use an oracle, allowing for flexible adoption of different available SMT solvers in the actual implementation. Finally, our automated reasoning approach for attributed graph properties is implemented in the tool AutoGraph integrating in particular the SMT solver Z3 for the attribute part of the properties. We motivate and illustrate our work with a particular application scenario on graph database query validation.

Appendices

Some details on AutoGraph

Definition 30

(Z3 Signature)

$$\begin{aligned} \textit{sorts:}\;&\mathsf {bool},\mathsf {int},\mathsf {string} \\ \textit{opns:}\;&\mathsf {true}:{}\rightarrow \mathsf {bool} \\&\mathsf {false}:{}\rightarrow \mathsf {bool} \\&\mathsf {not}:\mathsf {bool} \rightarrow \mathsf {bool} \\&\mathsf {and}:\mathsf {bool} \;\mathsf {bool} \rightarrow \mathsf {bool} \\&\mathsf {or}:\mathsf {bool} \;\mathsf {bool} \rightarrow \mathsf {bool} \\&\mathsf {xor}:\mathsf {bool} \;\mathsf {bool} \rightarrow \mathsf {bool} \\&\mathsf {implies}:\mathsf {bool} \;\mathsf {bool} \rightarrow \mathsf {bool} \\&\mathsf {eq\_{bool}}:\mathsf {bool} \;\mathsf {bool} \rightarrow \mathsf {bool} \\&\mathsf {ifthenelse\_{bool}}:\mathsf {bool} \;\mathsf {bool} \;\mathsf {bool} \rightarrow \mathsf {bool} \\&\mathsf {zero}:{}\rightarrow \mathsf {int} \\&\mathsf {succ}:\mathsf {int} \rightarrow \mathsf {int} \\&\mathsf {pred}:\mathsf {int} \rightarrow \mathsf {int} \\&\mathsf {minus}:\mathsf {int} \rightarrow \mathsf {int} \\&\mathsf {add}:\mathsf {int} \;\mathsf {int} \rightarrow \mathsf {int} \\&\mathsf {sub}:\mathsf {int} \;\mathsf {int} \rightarrow \mathsf {int} \\&\mathsf {mul}:\mathsf {int} \;\mathsf {int} \rightarrow \mathsf {int} \\&\mathsf {mod}:\mathsf {int} \;\mathsf {int} \rightarrow \mathsf {int} \\&\mathsf {rem}:\mathsf {int} \;\mathsf {int} \rightarrow \mathsf {int} \\&\mathsf {power}:\mathsf {int} \;\mathsf {int} \rightarrow \mathsf {int} \\&\mathsf {eq\_{int}}:\mathsf {int} \;\mathsf {int} \rightarrow \mathsf {bool} \\&\mathsf {gt}:\mathsf {int} \;\mathsf {int} \rightarrow \mathsf {bool} \\&\mathsf {lt}:\mathsf {int} \;\mathsf {int} \rightarrow \mathsf {bool} \\&\mathsf {ge}:\mathsf {int} \;\mathsf {int} \rightarrow \mathsf {bool} \\&\mathsf {le}:\mathsf {int} \;\mathsf {int} \rightarrow \mathsf {bool} \\&\mathsf {ifthenelse\_{int}}:\mathsf {bool} \;\mathsf {int} \;\mathsf {int} \rightarrow \mathsf {int} \\&\mathsf {empty}:{}\rightarrow \mathsf {string} \\&\mathsf {concat}:\mathsf {string} \;\mathsf {string} \rightarrow \mathsf {string} \\&\mathsf {length}:\mathsf {string} \rightarrow \mathsf {int} \\&\mathsf {contains}:\mathsf {string} \;\mathsf {string} \rightarrow \mathsf {bool} \\&\mathsf {indexOf}:\mathsf {string} \;\mathsf {string} \;\mathsf {int} \rightarrow \mathsf {int} \\&\mathsf {replace}:\mathsf {string} \;\mathsf {string} \;\mathsf {string} \rightarrow \mathsf {string} \\&\mathsf {prefixOf}:\mathsf {string} \;\mathsf {string} \rightarrow \mathsf {bool} \\&\mathsf {suffixOf}:\mathsf {string} \;\mathsf {string} \rightarrow \mathsf {bool} \\&\mathsf {at}:\mathsf {string} \;\mathsf {int} \rightarrow \mathsf {string} \\&\mathsf {extract}:\mathsf {string} \;\mathsf {int} \;\mathsf {int} \rightarrow \mathsf {string} \\&\mathsf {eq\_{string}}:\mathsf {string} \;\mathsf {string} \rightarrow \mathsf {bool} \\&\mathsf {ifthenelse\_{string}}:\mathsf {bool} \;\mathsf {string} \;\mathsf {string} \rightarrow \mathsf {string} \end{aligned}$$

Furthermore, we assume sufficient operations for constructing values of $\mathsf {string}$ as terms such as $\mathsf {a},\dots ,\mathsf {z},\mathsf {0},\dots ,\mathsf {9},\mathsf {-},\mathsf {SPACE}:{}\rightarrow \mathsf {string}$.

Categorical preliminaries and properties of GraphsSTA

Lemma 11

(GraphsSTA: Characterization of the Monomorphisms, Epimorphisms, and Isomorphisms) A graph morphism $f:G\rightarrow G'$ from the category GraphsSTA is a mono(morphism) (epi(morphism)) (iso(morphism)), if each of its components is injective (surjective) (bijective), respectively. And, for isomorphisms, we additionally require that the reversed implication from Definition  11 holds as well, i.e., for all $\sigma \in \mathcal {V}_{\Sigma _{A_2},\Sigma _{A_2}}$: $\sigma \models f_{ AX }(\varPhi _1)$ implies $\sigma \models \varPhi _2$.

Proof

(idea) Due to the componentwise characterization.

Definition 31

($\mathcal {E}$-$\mathcal {M}$-Factorization) Given a category, a set $\mathcal {E}$ of epimorphisms, and a set $\mathcal {M}$ of monomorphisms. The category has $\mathcal {E}$-$\mathcal {M}$ -Factorizations, if

• (existence) for each $f:A\rightarrow C$ there are $(e:A\twoheadrightarrow K)\in \mathcal {E}$ and s.t. $m\circ e=f$ and

• (uniqueness) for $(e':A\twoheadrightarrow K')\in \mathcal {E}$ and with $m'\circ e'=f$ there is with $i\circ e=e'$ and $m'\circ i=m$.

Definition 32

(Jointly Epimorphic Morphisms [13, Definition A.16, p. 334]) Two morphisms $e_1:A_1\rightarrow B$ and $e_2:A_2\rightarrow B$ of a category are Jointly Epimorphic, if any two morphisms $g,h:B\rightarrow C$ are equal whenever $g\circ e_i=h\circ e_i$ (for each $1\le i \le 2$).

Pair Factorization (cf. [13, Definition 5.25, p. 122]) has the intuition that any two morphisms $f_1$ and $f_2$ with common codomain C coincide (in the sense of mapping to the same elements) on a well-defined subgraph K of C. That K does not include further elements (on which the two morphisms do not coincide) is expressed by stating that the morphisms $e_1$ and $e_2$ are jointly epimorphic and the coincidence is expressed by stating that m is a monomorphism together with the commutation.

Definition 33

($\mathcal {E'}$-$\mathcal {M}$-Pair Factorization) For a given category, a set $\mathcal {E'}$ of pairs $(f_1,f_2)$ of jointly epi morphisms, and a set $\mathcal {M}$ of monomorphisms. The category has $\mathcal {E'}$-$\mathcal {M}$ -Pair Factorizations, if for each two morphisms $f_1:A_1\rightarrow C$ and $f_2:A_2\rightarrow C$ there are $(e_1:A_1\rightarrow K,e_2:A_2\rightarrow K)\in \mathcal {E'}$ and s.t. $m\circ e_i=f_i$ (for each $1\le i\le 2$).

Definition 34

(Binary Coproduct) A category has binary coproducts, if for every $A_i$ (with $1\le i\le 2$) there are $f_i:A_i\rightarrow C$ (for each $1\le i\le 2$) s.t. (the following universal property holds) for all $g_i:A_i\rightarrow X$ there is a unique $h:C\rightarrow X$ with $h\circ f_i=g_i$ (for each $1\le i\le 2$).

Lemma 12

(GraphsSTA has Binary Coproducts)

Proof

(idea) The binary coproduct C with morphisms $f_1$ and $f_2$ from Definition  34 is constructed componentwise using the disjoint union, as usual.

For the category GraphsSTA, we use as $\mathcal {E}$ the set of all epimorphisms, as $\mathcal {M}$ the set of all monomorphisms, and as $\mathcal {E'}$ the set of all pairs of jointly epimorphic morphisms.

Lemma 13

(GraphsSTA has $\mathcal {E}$-$\mathcal {M}$-Factorization)

Proof

(idea) The morphisms e and m, required according to Definition 31, are constructed componentwise for a morphism f.

Lemma 14

(GraphsSTA has $\mathcal {E'}$-$\mathcal {M}$-Pair Factorization)

Proof

(idea) Analogously to [13, Remark 5.26, p. 122], we construct the $\mathcal {E'}$-$\mathcal {M}$-Pair Factorizations using $\mathcal {E}$-$\mathcal {M}$-Factorizations (based on Lemma 13) and binary coproducts (based on Lemma 12).

Proofs

Proof of Lemma 2

Part1 ($\subseteq$).

$$\begin{aligned}&G\in \llbracket \exists (i_C,\vee S)\rrbracket \\&\quad \Longrightarrow i_G\models \exists (i_C,\vee S)\\ \end{aligned}$$

for some q:C G

$$\begin{aligned} \Longrightarrow q\models \vee S \end{aligned}$$

for some $c\in S$

$$\begin{aligned}&\Longrightarrow \, q\models c\\&\quad \Longrightarrow \, q\circ i_C\models \exists (i_C,c)\\&\quad \Longrightarrow \, i_G\models \exists (i_C,c)\\&\quad \Longrightarrow \, G\in \llbracket \exists (i_C,c)\rrbracket \\&\quad \Longrightarrow \, G\in \bigcup \{\llbracket \exists (i_C,c)\rrbracket \mid c\in S\} \end{aligned}$$

Part2 ($\supseteq$).

$$\begin{aligned} G\in \bigcup \{\llbracket \exists (i_C,c)\rrbracket \mid c\in S\} \end{aligned}$$

for some $c\in S$

$$\begin{aligned}&\Longrightarrow \, G\in \llbracket \exists (i_C,c)\rrbracket \\&\Longrightarrow \, i_G\models \exists (i_C,c) \end{aligned}$$

for some

$$\begin{aligned}&\Longrightarrow \, q\models c\\&\Longrightarrow \, q\models \vee S\\&\Longrightarrow \, q\circ i_C\models \exists (i_C,\vee S)\\&\Longrightarrow \, i_G\models \exists (i_C,\vee S)\\&\Longrightarrow \, G\in \llbracket \exists (i_C,\vee S)\rrbracket \end{aligned}$$

Proof of Lemma 5

Part1 ($\subseteq$).

for some

for some

$$\begin{aligned}&\Longrightarrow q_2\models c \text { and }q_1=q_2\circ m\\&\Longrightarrow \, q_2\circ i_{C_2}\models \exists (i_{C_2},c)\\&\Longrightarrow \, i_G\models \exists (i_{C_2},c)\\&\Longrightarrow \, G\in \llbracket \exists (i_{C_2},c)\rrbracket \end{aligned}$$

Part2 ($\supseteq$).

$$\begin{aligned}&G\in \llbracket \exists (i_{C_2},c)\rrbracket \\&\Longrightarrow i_G\models \exists (i_{C_2},c) \end{aligned}$$

for some

Proof of Lemma 6

Part1 (C is an element).

$$\begin{aligned}&C\in \llbracket \exists (i_C,\wedge \{\lnot \exists (m_1,c_1),\dots ,\lnot \exists (m_n,c_n)\})\rrbracket \\&\quad \Longleftarrow i_C\models \exists (i_C,\wedge \{\lnot \exists (m_1,c_1),\dots ,\lnot \exists (m_n,c_n)\}) \end{aligned}$$

for

$$\begin{aligned} \Longleftarrow&id _{C} \models \wedge \{\lnot \exists (m_1,c_1),\dots ,\lnot \exists (m_n,c_n)\} \end{aligned}$$

for each $1\le i\le n$ simultaneously

$$\begin{aligned}&\Longleftarrow id _{C} \models \lnot \exists (m_i,c_i)\\&\Longleftarrow id _{C} \not \models \exists (m_i,c_i) \end{aligned}$$

there is no such that $q_i\models c_i$ and $q_i\circ m_i=q$

$$\begin{aligned} \Longleftarrow m_i\text { is no isomorphism} \end{aligned}$$

Part2 (unique least element).

$$\begin{aligned}&C'\in \llbracket \exists (i_C,\wedge \{\lnot \exists (m_1,c_1),\dots ,\lnot \exists (m_n,c_n)\})\rrbracket \\&\Longrightarrow i_{C'}\models \llbracket \exists (i_C,\wedge \{\lnot \exists (m_1,c_1),\dots ,\lnot \exists (m_n,c_n)\})\rrbracket \end{aligned}$$

for some

$$\begin{aligned}&\Longrightarrow q\models \wedge \{\lnot \exists (m_1,c_1),\dots ,\lnot \exists (m_n,c_n)\}\\&\Longrightarrow C\subseteq C' \end{aligned}$$

Proof of Lemma 3

Part1 ($\subseteq$).

for some

for some

$$\begin{aligned} \Longrightarrow q_2\models c' \text { and }q_1=q_2\circ m \end{aligned}$$

(2)

also

$$\begin{aligned}&q_1\models \wedge S\\&\Longrightarrow q_2\circ m\models \wedge S\\&\Longrightarrow q_2\models shift (m,\wedge S) \\&\Longrightarrow q_2\models c'\wedge shift (m,\wedge S) \\&\Longrightarrow q_2\circ m\models \exists (m,c'\wedge shift (m,\wedge S))\\&\Longrightarrow q_2\circ m\circ i_C\models \exists (i_C,\exists (m,c'\wedge shift (m,\wedge S)))\\&\Longrightarrow i_G\models \exists (i_C,\exists (m,c'\wedge shift (m,\wedge S)))\\&\Longrightarrow G\in \llbracket \exists (i_C,\exists (m,c'\wedge shift (m,\wedge S)))\rrbracket \end{aligned}$$

Part2 ($\supseteq$).

$$\begin{aligned}&G\in \llbracket \exists (i_C,\exists (m,c'\wedge shift (m,\wedge S)))\rrbracket \\&\quad \Longrightarrow i_G\models \exists (i_C,\exists (m,c'\wedge shift (m,\wedge S))) \end{aligned}$$

for some

$$\begin{aligned}&\Longrightarrow q_1\models \exists (m,c'\wedge shift (m,\wedge S)) \end{aligned}$$

for some

$$\begin{aligned}&\Longrightarrow q_2\models c'\wedge shift (m,\wedge S) \text { and }q_1=q_2\circ m\\&\Longrightarrow q_2\models c'\text { and }q_2\models shift (m,\wedge S) \\&\Longrightarrow q_2\circ m\models \exists (m,c') \end{aligned}$$

also

Proof of Lemma 8

Part1.1 (if).

$$\begin{aligned}&covered (\mathcal {S}) = covered (\mathcal {S} ') \\&\quad \Longrightarrow covered (\mathcal {S}) \subseteq covered (\mathcal {S} ') \end{aligned}$$

because $covered (\mathcal {S}-\mathcal {S} ') \subseteq covered (\mathcal {S})$

$$\begin{aligned}&\Longrightarrow covered (\mathcal {S}-\mathcal {S} ') \subseteq covered (\mathcal {S} ') \\&\Longrightarrow covered (\mathcal {S}-\mathcal {S} ')- covered (\mathcal {S} ') =\emptyset \end{aligned}$$

Part1.2 (only if).

$$\begin{aligned}&covered (\mathcal {S}-\mathcal {S} ')- covered (\mathcal {S} ') =\emptyset \\&\Longrightarrow covered (\mathcal {S}-\mathcal {S} ') \subseteq covered (\mathcal {S} ') \end{aligned}$$

because $covered (\mathcal {S})- covered (\mathcal {S} ') \subseteq covered (\mathcal {S}-\mathcal {S} ')$

$$\begin{aligned}&\Longrightarrow covered (\mathcal {S})- covered (\mathcal {S} ') \subseteq covered (\mathcal {S} ') \\&\Longrightarrow ( covered (\mathcal {S})- covered (\mathcal {S} '))- covered (\mathcal {S} ') =\emptyset \\&\Longrightarrow covered (\mathcal {S})- covered (\mathcal {S} ') =\emptyset \\&\Longrightarrow covered (\mathcal {S}) \subseteq covered (\mathcal {S} ') \end{aligned}$$

because $\mathcal {S} '\subseteq \mathcal {S}$ implies $covered (\mathcal {S} ') \subseteq covered (\mathcal {S})$

$$\begin{aligned}&\Longrightarrow covered (\mathcal {S}) = covered (\mathcal {S} ') \end{aligned}$$

Part2.

$$\begin{aligned}&\vee \{\exists (i_C,c)\mid \langle C,c\rangle \in \mathcal {S}-\mathcal {S} '\}\\&\quad \wedge \lnot \vee \{\exists (i_C,c)\mid \langle C,c\rangle \in \mathcal {S} '\}\text { is refutable}\\&\Longleftrightarrow \llbracket \vee \{\exists (i_C,c)\mid \langle C,c\rangle \in \mathcal {S}-\mathcal {S} '\}\\&\quad \wedge \lnot \vee \{\exists (i_C,c)\mid \langle C,c\rangle \in \mathcal {S} '\}\rrbracket =\emptyset \\&\Longleftrightarrow \llbracket \vee \{\exists (i_C,c)\mid \langle C,c\rangle \in \mathcal {S}-\mathcal {S} '\}\rrbracket \\&\quad \cap \llbracket \lnot \vee \{\exists (i_C,c)\mid \langle C,c\rangle \in \mathcal {S} '\}\rrbracket =\emptyset \\&\Longleftrightarrow covered (\mathcal {S}-\mathcal {S} ') \\&\quad \cap (\{G\mid G\text { is a graph}\}- covered (\mathcal {S} '))=\emptyset \\&\Longleftrightarrow covered (\mathcal {S}-\mathcal {S} ')- covered (\mathcal {S} ') =\emptyset \end{aligned}$$

Proof of Lemma 9

• Part1 (if). Fix some $\langle C,\wedge \emptyset \rangle \in \mathcal {S}$.

  Assume for the contradiction $covered (\mathcal {S}) = covered (\mathcal {S}-\{\langle C,\wedge \emptyset \rangle \})$. Hence, for each $G\in covered (\langle C,\wedge \emptyset \rangle )$ there is some other $\langle C',\wedge \emptyset \rangle \in \mathcal {S}$ s.t. $G\in covered (\langle C,\wedge \emptyset \rangle )$.

  Note that $C\in covered (\langle C',\wedge \emptyset \rangle )$. Hence, we are able to pick some $\langle C',\wedge \emptyset \rangle$ s.t. $C\in covered (\langle C',\wedge \emptyset \rangle )$.

  Hence, there is a monomorphism .

  This is a contradiction.

• Part2 (only if). Fix distinct $\langle C,\wedge \emptyset \rangle \in \mathcal {S}$ and $\langle C',\wedge \emptyset \rangle \in \mathcal {S}$.

  Assume for the contradiction that is a monomorphism.

  Hence $covered (\langle C,\wedge \emptyset \rangle ) \subseteq covered (\langle C',\wedge \emptyset \rangle )$.

  Hence $covered (\mathcal {S}) = covered (\mathcal {S}-\{\langle C,\wedge \emptyset \rangle \})$.

  Hence $\mathcal {S}$ is not compact.

  This is a contradiction.

Proof of Corollary 1

• Let $\mathcal {S}$ be nonambiguous, (sound,) complete, minimally representable.

• We show that $\mathcal {S}$ is compact.

• Fix some $\langle C,c\rangle \in \mathcal {S}$.

• We show that $covered (\mathcal {S}) \ne covered (\mathcal {S}-\{\langle C,c\rangle \})$.

  • We show that $C\in covered (\mathcal {S})$.

    From minimally representability we have that $C\models p$.

    From completeness we that $C\in covered (\mathcal {S})$.

  • We show that $C\notin covered (\mathcal {S}-\{\langle C,c\rangle )$.

    Assume for the contradiction that $\langle C',c'\rangle \in \mathcal {S}-\{\langle C,c\rangle$ such that $C\in covered (\langle C',c'\rangle )$.

    Then, $covered (\langle C',c'\rangle ) \cap covered (\langle C,c\rangle ) \ne \emptyset$ contradicts nonambiguity because $\langle C',c'\rangle \ne \langle C,c\rangle$.

Lemma 15

(Satisfaction is a Congruence) Let $c_1$ and $c_2$ be conditions from $\mathcal {C}_{C}$ such that $\{q\mid q\models c_1\}=\{q\mid q\models c_2\}$. Then all following items are satisfied.

• $\{q\mid q\models \wedge (S\cup \{c_1\})\} =\{q\mid q\models \wedge (S\cup \{c_2\})\}$ for all finite $S\subseteq \mathcal {C}_{C}$.

• $\{q\mid q\models \lnot c_1\} =\{q\mid q\models \lnot c_2\}$.

• for every .

Proof of Lemma 15

Fix $c_1,c_2\in \mathcal {C}_{C}$.

Assume (A) that $\{q\mid q\models c_1\}=\{q\mid q\models c_2\}$. In each case, we show only one direction wlog.

• Fix some $S\subseteq \mathcal {C}_{C}$ that is finite.

  Fix some such that $q\models \wedge (S\cup \{c_1\})$.

  Hence, $q\models \wedge S$ and $q\models c_1$.

  From (A) we have that $q\models c_2$.

  Hence, $q\models \wedge (S\cup \{c_2\})$.

• Fix some such that $q\models \lnot c_1$.

  Hence, not $q\models c_1$.

  From (A) we have that not $q\models c_2$.

  Hence, $q\models \lnot c_2$.

• Fix some .

  Fix some such that .

  Hence, there is some such that $q\models c_1$ and $q\circ m=q'$.

  From (A) we have that $q\models c_2$.

  Hence, .

Proof of Lemma 4

The construction steps of $[\cdot ]$ replace subterms.

By structural induction relying on Lemma 15, it is sufficient to consider how one condition $c_1$ is replaced by another condition $c_2$ over same graph in the sense of $\{q\mid q\models c_1\}=\{q\mid q\models c_2\}$.

We verify for all five steps of the operation $[\cdot ]$ that the property is rephrased equivalently.

• Step 1: The unfolding of abbreviations is sound by default.

• Step 2: We assume that has been replaced by $c_2$.

  We perform an induction on $c_1$.

  • Case: $c_1=\lnot c_1'$ and, hence, for some $c_2'$

    As induction hypothesis, we assume that $\{q\mid q\models c_1'\}=\{q\mid q\models c_2'\}$. We have to show , which is the direct consequence from Lemma 15.

  • Case: $c_1{=}\wedge \{c_{0,1},\dots ,c_{n,1}\}$ and, hence, $c_2{=}\wedge \{c_{0,2},\dots ,c_{n,2}\}$ for some $c_{0,2}$, ..., $c_{n,2}$ As induction hypothesis we assume that $\{q\mid q\models c_{i,1}\}=\{q\mid q\models c_{i,2}\}$ (for $0\le i\le n$) We have to show , which is the direct consequence from Lemma 15.

  • Case: and, hence, $c_2=\exists (m\circ i,c_1')$

    We have to show , which holds directly application of Definition 16.

• Step 3: We show that if is empty. This is trivially the case because $\{q\mid q\models \vee \emptyset \}$ is also empty.

• Step 4: The mentioned replacement rules

  $\lnot (\wedge S){\mathop {=}\limits ^{\cdot }}\vee \{\lnot c\mid c\in S\}$,

  $\lnot (\vee S){\mathop {=}\limits ^{\cdot }}\wedge \{\lnot c\mid c\in S\}$, and

  $\lnot \lnot c{\mathop {=}\limits ^{\cdot }}c$

  are obviously sound in the sense of:

  $\{q\mid q\models lhs \}=\{q\mid q\models rhs \}$.

• Step 5: The mentioned replacement rules

  $\wedge (S\cup \{\wedge S'\}){\mathop {=}\limits ^{\cdot }}\wedge (S\cup S')$,

  $\vee (S\cup \{\vee S'\}){\mathop {=}\limits ^{\cdot }}\vee (S\cup S')$,

  $\wedge (S\cup \{\vee S'\}){\mathop {=}\limits ^{\cdot }}\vee \{\wedge (S\cup \{c\})\mid c\in S'\}$, and

  $\vee (S\cup \{\wedge S'\}){\mathop {=}\limits ^{\cdot }}\wedge \{\vee (S\cup \{c\})\mid c\in S'\}$

  are obviously sound in the sense of:

  $\{q\mid q\models lhs \}=\{q\mid q\models rhs \}$.