Talk:Clause (logic)

Similarity between a Clause and a Maxterm

Would it be worth mentioning the similarity between a Clause and a Maxterm. They both appear to be the disjunction of literals. The only difference I can see is that Clauses can be written with the $\{l_{1},\ldots ,l_{n}\}$ notation and they can be empty. Egriffin 21:12, 24 May 2007 (UTC)

Why only a disjunction?

Seems like someone wrote this with some particular application in mind. Completely unreferenced. Tijfo098 (talk) 07:56, 18 April 2011 (UTC)

Well, because in logic, a "clause" is defined like that. You might just as well ask why "+" is used "only for addition". I'll add a reference. --Stephan Schulz (talk) 08:02, 18 April 2011 (UTC)

You need to read more than one book. [1] [2] [3] [4]. It appears that the shorthand from "disjunctive clause" to "clause" is mainly (if not only) practiced in the automated theorem proving / logic programming circles. [5] But even in that field, there are books how don't do this [6] (given previously) [7] [8]. (And a more appropriate analogy is defining arithmetic operation to mean only addition.) Tijfo098 (talk) 15:46, 18 April 2011 (UTC)

Sorry, I see nothing in your examples that disagrees with the definition given. $A_{1}\vee \ldots \vee A_{n}\leftarrow B_{1},\ldots ,B_{m}$ (and several other related forms) is just a convenient notation for $A_{1}\vee \ldots \vee A_{n}\vee \neg B_{1}\vee \ldots \vee \neg B_{m}$. Sometimes its useful for illustrative purposes to write a clause as an implication with disjunctive head, or as a conditional with a unit head and positive/negative conditions. But these are all equivalent to simple disjunctions via De Morgan's laws. Your last addition (an edit conflict with my original reply) adds "conjunctive clause" as a different concept. However, this is decidedly rare, and does not imply that the unqualified "clause" is used to refer to non-disjunctive clauses. It's also a book about graph theory, not primarily about logic. --Stephan Schulz (talk) 16:08, 18 April 2011 (UTC)

Can you give me the context from your book in which this def appears? Is it in the context of CNF? Because that would explain it. [9] [10]. Tijfo098 (talk) 16:07, 18 April 2011 (UTC)

IIRC, it precedes the definition of CNF (which is, again, interchangeably expanded "Clause Normal Form" and "Conjunctive Normal Form", because the differences are merely representational). I left the book at home this morning, if you need to know more I can check later. --Stephan Schulz (talk) 16:13, 18 April 2011 (UTC)

Well, in the DNF every clause is a conjunction. But SAT-solvers and similar automated tool usually deal only with CNF (see the two refs above). So, it makes sense for a book that has "Mechanical Theorem Proving" in the tile to be geared towards that. But there are math logic books which don't do that; the first ref I gave in my post here: "Disjunctive and conjunctive clauses are simply called clauses." [11] Tijfo098 (talk) 16:20, 18 April 2011 (UTC)

Certainly in logic programming (where the inputs are CNF or Horn) a clause frequently means a disjunction, but that isn't the same as always meaning a disjunction. In particular in disjunctive normal form the clauses are conjunctions. —David Eppstein (talk) 17:00, 18 April 2011 (UTC)

I just went through a number of logic books (Handbook of Mathematical Logic, Handbook of Philosophical Logic, Hinman, Enderton), and found that they use the term "clause" in a vague, metamathematical sense that has no connection whatsoever with this article. They do not have "clause" in their indices. However, Ebbinghaus/Flum/Thomas, Rautenberg and Hedman define the term essentially as in this article. There is a subtle problem that makes it unclear whether clauses are a more general concept than just disjunctive clauses or not. And that problem goes back to the original paper on resolution. (I found this through Ebbinghaus et al's book.)

Here is the definition:

2.10 Clauses. A finite set of (possibly empty) literals is called a clause. [...]

The context was such that these sets represented disjunctions of literals. Now if one dualises everything it's not clear whether to call the resulting sets of (dualised, i.e. negated or un-negated) literals "clauses" or something like "co-clauses". Ebbinghaus et al stays close enough to the original definition to reproduce the ambiguity. Hedman proceeds as this article does: "We refer to a disjunction of literals as a clause. For convenience, we write each clause as a set." Rautenberg, on the other hand, defines without an equally clear context: "A finite, possibly empty set of literals is called a (propositional) clause." So Hedman diverges in one direction from the original definition (the same as our article), and Rautenberg in the other. I think the Ebbinghaus et al approach is the best for an encyclopedia. Unless we choose to make the two interpretations explicit, but this might cause undue weight or OR problems. Hans Adler 17:14, 18 April 2011 (UTC)

Actually, Melvin Fitting does define "dual clause" in the context of resolution, but says the notion is non-standard and most useful in semantic tableaus. p. 28 in 2nd ed. (In the 1st edition of his book, which is more likely to be held by your library, it's on p. 25). Tijfo098 (talk) 06:02, 19 April 2011 (UTC)

By the way, Hedman defines it in the context of resolution/CNF: [12] as well. Tijfo098 (talk) 06:31, 19 April 2011 (UTC)

Someone even defined term to mean the dual of clause [13], but not the Wikipedia article. Tijfo098 (talk) 07:06, 19 April 2011 (UTC)

The Germans are more logical and have de:Disjunktionsterm (linked here) and de:Konjunktionsterm :-) Tijfo098 (talk) 07:29, 19 April 2011 (UTC)

(edit conflict) I've checked John Harrison's book which aims to fulfill the same role as Chang and Lee. On p. 80 Harrison writes:

“ We found a ‘set of sets’ representation useful in transforming a formula into CNF, and we’ll use it in the DP and DPLL procedures themselves. An implicit ‘set of sets’ representation of a CNF formula is often referred to as clausal form, and each conjunct is called a clause. ”

Italics his. So, yeah, it's defined that way, but in a specific context—CNF and for a specific purpose. So, perhaps merging this with conjunctive normal form or renaming it to clause (conjunctive normal form) or clause (automated theorem proving) would clarify the scope of this definition/article. Tijfo098 (talk) 17:20, 18 April 2011 (UTC) PS: This def appears in the Davis–Putnam procedure section in Harrison. As far as I can tell, he does not define clause anywhere else; p. 80 is only one listed in the book's index under "clause". Tijfo098 (talk) 17:28, 18 April 2011 (UTC)

The 2000+ citations paper on Chaff algorithm [14] also defines clause wrt CNF, but at least explains well why:

“ Most solvers operate on problems for which f is specified in conjunctive normal form (CNF). This form consists of the logical AND of one or more clauses, which consist of the logical OR of one or more literals. The literal comprises the fundamental logical unit in the problem, being merely an instance of a variable or its complement. (In this paper, complement is represented by ¬.) All Boolean functions can be described in the CNF format. The advantage of CNF is that in this form, for f to be satisfied (sat), each individual clause must be sat. ”

-- So either clause (conjunctive normal form) or clause (satisfiability) seems a correct title. Tijfo098 (talk) 20:05, 18 April 2011 (UTC)

Well, I've probably read a few hundred papers and several of books in automated theorem proving. Interpreting clause as "disjunctive clause" is pretty universal there. So "conjunctive normal form" is to restricted. "Satisfiability" is very often used as short-hand for "Boolean satisfiability" (i.e. propositional SAT), and thus does not cover the first-order case. Many older papers and books in ATP even define a "formula" as a set of clauses (thus implicitly assuming CNF, and not supporting the full language of FOF). As far as I can tell, the disjunctive case is also used near exclusively in (deductive) logic programming. So we use a DAB quantifier that covers (at least) ATP and LP. Maybe "Clause (deduction)"? Or leave it as-is with a note that clause often/usually denotes the disjunctive case and have a small section on "conjunctive clauses"? --Stephan Schulz (talk) 06:49, 19 April 2011 (UTC)

FOL and/or Gentzen calculus

I checked a recent book on cut elimination, which has a sizable portion on Resolution (logic), and they define (Def 3.3.7 p. 35): A clause is an atomic sequent. By Definition 3.1.9 (p. 12) A sequent A1,...,An ⊢ B1,...,Bm is called atomic if the Ai, Bj are atomic formulas. Which means by the def of sequent (same page) and that of atomic formula (prev page) that a clause is semantically an implication:

P1(...) ∧ P2(...) ∧ ... ∧ Pn(...) ⇒ Q1(...) ∨ Q2(...) ∨ ... ∨ Qm(...)

So it's not just the right-hand side of it, which is the definition given here for FOL, except when the left-hand side is empty, i.e. the right-hand side is a tautology. Tijfo098 (talk) 20:59, 18 April 2011 (UTC)

See above. P1(...) ∧ P2(...) ∧ ... ∧ Pn(...) ⇒ Q1(...) ∨ Q2(...) ∨ ... ∨ Qm(...) is equivalent to (or just another way of writing) ¬P1(...) ∨ ¬P2(...) ∨ ... ∨ ¬Pn(...) ∨ Q1(...) ∨ Q2(...) ∨ ... ∨ Qm(...). Note the conjunction on the left hand of the implication and the fact that A⇒B is ¬A∨B. --Stephan Schulz (talk) 21:10, 18 April 2011 (UTC)

Not quite. The current wiki article does not allow negation of first-order literals (predicates) in a clause. Tijfo098 (talk) 21:17, 18 April 2011 (UTC)

A literal is either an atom or a negated atom. P(...) is an atom. ¬P(...) is a negative literal (and P(...) is the positive literal as well as the atom). --Stephan Schulz (talk) 21:33, 18 April 2011 (UTC)

Revisiting Definition

The page on DNF contradicts this one. As a temporary fix, I have edited the page to mention both definitions. If consensus is to change back to the CNF-centric definition, please make sure that corresponding changes are made at that article. 129.93.4.37 (talk) 16:57, 26 October 2015 (UTC)

External links

Why is "Clause simultaneously translated in several languages and meanings" among the external links? 109.153.241.223 (talk) 15:07, 10 July 2016 (UTC)