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**

Join Physics Forums Today!

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

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**