How would you describe this set in plain English:(adsbygoogle = window.adsbygoogle || []).push({});

[tex]\text{POS}_\lambda(\alpha) = \alpha_\lambda^0 \cup \{\kappa - \{\lambda\}|\kappa \in \alpha_\lambda^+\}[/tex]

where:

[itex]\lambda[/itex] is a literal

[itex]\kappa[/itex] is an [itex]\vee[/itex] clause with the set [itex]\kappa = \vee_{j\leq m}\;\lambda_j [/itex] represented as [itex] \kappa = \{\lambda_j|j \leq m \}[/itex]

[itex]\{\lambda\}[/itex] is a unit clause consisting of just a single literal [itex]\lambda[/itex]

a CNF formula [itex]\alpha[/itex] is a set [itex]\alpha = \wedge_{i\leq n}\;\kappa_i [/itex] represented as [itex] \alpha = \{\kappa_i|i \leq n \}[/itex]

a clause [itex]\kappa[/itex] is called [itex]\lambda-positive[/itex] if [itex]\lambda \in \kappa [/itex]

a clause [itex]\kappa[/itex] is called [itex]\lambda-negative[/itex] if [itex]\neg \lambda \in \kappa [/itex]

a clause [itex]\kappa[/itex] is called [itex]\lambda-neutral[/itex] if [itex]\kappa [/itex] is neither [itex]\lambda-positive [/itex] nor [itex]\lambda-negative [/itex]

if [itex]\alpha[/itex] is a set of clauses, [itex]\alpha_\lambda^+[/itex] is the set of [itex]\lambda-positive [/itex] clauses of [itex]\alpha[/itex], [itex]\alpha_\lambda^-[/itex] is the set of [itex]\lambda-negative [/itex] clauses of [itex]\alpha[/itex], and [itex]\alpha_\lambda^0[/itex] is the set of [itex]\lambda-neutral [/itex] clauses of [itex]\alpha[/itex].

At first, I was reading [itex]\text{POS}_\lambda(\alpha)[/itex] as the union of the [itex]\lambda-neutral [/itex] clauses of [itex]\alpha[/itex] with the [itex]\lambda-positive [/itex] clauses of [itex]\alpha[/itex] but excluding theunit clause[itex]\{\lambda\}[/itex]. But apparently it is intended to be read as the union of the [itex]\lambda-neutral [/itex] clauses of [itex]\alpha[/itex] with the [itex]\lambda-positive [/itex] clauses of [itex]\alpha[/itex] but with ALL of the [itex]\lambda[/itex] terms EXCLUDED from those clauses.

WHY is it read that way? Or, to put it another way, why was it not written as [itex]\text{POS}_\lambda(\alpha) = \alpha_\lambda^0 \cup \{\kappa - \lambda|\kappa \in \alpha_\lambda^+\}[/itex]. (Why did they put their [itex]\lambda[/itex] in brackets {}?) And how would you write set-builder notation for "the [itex]\lambda-positive [/itex] clauses of [itex]\alpha[/itex] but excluding just theunit clause[itex]\{\lambda\}[/itex]."

This comes from Computability, Complexity and Languages by Davis, Sigal and Weyuker, section 12.4, discussion of the Davis-Putnam rules for algorithms to manipulate CNF formulas.

**Physics Forums | Science Articles, Homework Help, Discussion**

The friendliest, high quality science and math community on the planet! Everyone who loves science is here!

# Set builder notation

**Physics Forums | Science Articles, Homework Help, Discussion**