Talk:Logic for Computer Science/Propositional Logic

From Wikibooks, the open-content textbooks collection

There seems to be a flaw in the proof that resolution is complete (see the second theorem under Properties of Propositional Resolution). The problem comes at the statement:

First, notice that

.

Taken literally, this is false. For instance, consider . Then φ^p = {q} = Res(φ^p) and , so the right-hand side of the above formula is . The author seems to have used subsumption, that is, if some clause is a superset of another, remove that clause. With this addition, which is more or less a new inference rule, the two sides do become equal if the right-hand side has been fully reduced by subsumption. Another possibility would be to define the "=" in the statement to mean logical equivalence as defined by truth tables. Either of these would require further exposition. Even then, however, the proof is too brief. It took me some hours to "notice" that the statement is true, even after thinking about subsumption. I believe, therefore, that the proof should be expanded to make it clearer, as follows (I have found it convenient to define "closure", which is in a sense the opposite of subsumption):

First, I would add, earlier in the section, the following.

Fact X: A CNF formula is satiisfiable if and only if the foumula created by replacing every occurrance of some variable p by and vice versa is satisfiable.

This is a useful fact in itself, and one that my students, anyhow, would often not see for themselves. Then, in the proof or elsewhere, I would define the closure cl(φ) to be the formula obtained by adding to φ every superset of the clauses in cl(φ). I would then change the proof, starting with the observation that if cl(φ) contains neither nor lnotp, neither does cl(φ), since the new formula can only produce longer clauses than the old one, not shorter. Also, I would note that if φ is closed, then so is Res(φ). After defining φ^p (as an operation on any formula), I would observe that if φ is closed, then so is φ^p. (I might give each of these facts a one-sentence proof.) I would then say

Claim: If cl(φ) is closed, then :Res(φ^p) = (Res(φ))^p..

Note that this is just a simpler way to write the statement that I first mentioned. Then,

Proof: First, consider any .

--Stefan Burr 15:59, 20 Jun 2005 (UTC)

Go a head and make the changes! MShonle 01:21, 21 Jun 2005 (UTC)

I think the horn clause example is faulty. It says:

Special case for which SAT is in polynomial time. Example:

A Horn clause is a disjunction of literals of which at most one is positive.

But in the example both p and r are positive literals!

Magnus Jonsson 21:03, 12 February 2006 (UTC)

[edit] Informal presentation needed?

Sorry if this is an incorrect assumption as I am unsure of the intended audience of this book, but it seems to me that if someone is already familiar with the syntax and semantics of set theory, and comfortable reading and understanding formal mathematical definitions, then surely they will be intimately familiar with propositional logic. Even having a chapter on propositional logic tells me that this chapter is probably meant for someone who is also unfamiliar with higher-order logics and discrete math concepts.

I would probably give an introduction and truth tables for logical connectives; and the nature of compound vs atomic statements. Maybe a little bit of history on logic and expand further upon the domain of problems that propositional logic can solve as opposed to higher order logics; and give an overview of these categories - separated from the formal definitions of concepts.

[edit] Minor points

I'm no expert, but the second numbered line describing CNF seems wrong to me:

2. Note that φ is true when is false. Hence, negate ψ using DeMorgan's laws.

Shouldn't it be "φ is true when is true"? Or "φ is true when ψ is false"? 75.162.244.167 (talk) 06:01, 2 September 2009 (UTC)