Talk:Horn clause

Older Discussion

Not conjunctive, it should be disjunctive normal form.

Wrong. Its conjunctive. Horn form is a conjunction of clauses. A clause is a symbol or {conjunction of symbols} -> symbol. —Preceding unsigned comment added by 137.132.3.7 (talk) 15:15, 30 April 2008 (UTC)

Deletion

I deleted

"Recent research ("An Evaluation of the Effect of the Brain-Oriented Organized Knowledge Map (Bookmap) for Improving School Results", Twan Brouwers & Hans Morélis, 2003) has shown that diagrams based on Horn clauses improve the human understanding of complex matter."

because there seems to be no public domain reference for this otherwise interesting work.193.136.122.18 16:47, 19 March 2007 (UTC)

There is a link http://www.bookmap.com/SLO-report.pdf on https://pt.wikipedia.org/wiki/Cl%C3%A1usula_de_Horn, but it seems broken. - Jochen Burghardt (talk) 19:33, 2 October 2013 (UTC)

Math Formulas

This is yet another example of poorly documented symbols in mathematical formulas. It would be nice if articles would give a natural language translation of formulas or give a definition of symbols that are not listed in the Table of mathematical symbols page.

mattelfesso (talk) 03:39, 28 February 2008 (UTC)

All symbols in this article are listed in Table of mathematical symbols, apart from $\leftarrow$ which is clearly the $\rightarrow$ used in the other direction. Tizio 10:05, 28 February 2008 (UTC)

You're right! I take back my comment... mattelfesso (talk) 05:21, 15 May 2008 (UTC)

Maximum 1 Positive Literal

The german article has a nice table that shows the implications of the above are. Namely a horn clause can be:

Rule: ~A1 v ... v ~An v B      n>=1  
Fact: B  
Query: ~A1 v ... v ~An         n>=1

In Prolog:

Rule: B :- A1, .., An  
Fact: B  
Query: ?- A1, .., An

Maybe the english article could be enhanced accordingly.

Bye

Janburse (talk) 20:06, 12 April 2012 (UTC)

Recent edit

The recent edit by an anonymous editor borders on vandalism, removing about half of the article without justification. Some of the changes it introduces are worth keeping, but it would be a lot easier to revert the edit first. Unfortunately, I don't have the time to work on it now myself. Compulogger (talk) 22:56, 21 November 2012 (UTC)

I integrated the recent editor's changes into the previous version, correcting a number of mistakes along the way. Unfortunately, I seem to have lost the categories at the end. Compulogger (talk) 07:28, 22 November 2012 (UTC)

Rating

This is a very important concept. Not as much due to foundations as due to its applications in logic programming, specification, and automated reasoning. I will continue to work on this article, but many concepts can be seen in logic programming. Historically, though, Horn clauses predate logic programming and have use in model theory originally, so they deserve this separate article. Vkuncak (talk) 10:54, 22 November 2013 (UTC)

Undecideable

Since it states citation needed, I'm not sure if this is relevant but

https://www.ii.uni.wroc.pl/~jma/csl93.pdf

"A Horn Clause that Implies an Undecidable Set of Horn Clauses"

Can someone with knowledge of this please check if this is a decent citation for the statement "Horn clauses are not decideable"? --130.63.96.77 (talk) 16:57, 4 April 2017 (UTC)

Also, in the pdf itself:

• J. Marcinkowski, L. Pacholski: Undecidability of the Horn Clause Implication Problem; Proc 33rd Annual Symposium on the Foundations of Computer Science (1992). pp. 354-362
• M.Schmidt-Schauss: Implication of Clauses is Undecidable; Theoretical Com-puter Science 59 (1988), pp. 287-296.

--130.63.96.77 (talk) 17:00, 4 April 2017 (UTC)

Readbility

It would be nice if the first paragraph said what a horn clause is, in easy to understand text. — Preceding unsigned comment added by 128.16.14.238 (talk) 13:20, 18 May 2017 (UTC)

What the heck is a fact?

Intro:

A Horn clause with exactly one positive literal is a definite clause or a strict Horn clause

OK.

 a definite clause with no negative literals is a unit clause

OK.

a unit clause without variables is a fact.

What? A fact is a unit clause and therefore is has exactly one positive literal no negative literals. So a fact has no negative literals exactly one positive literals but is distinguished from a unit clause in having no "variables". So unit clauses may have "variables"?? Whether this makes any sense hinges on what the heck a "variable" is. The above is the first time "variable" has been used. All previous explanation used the term "literal" or "symbol" which is purely syntactic. What "variable" means in any of this is ambiguous and hints at some hidden semantics (ambiguously). The table should show the difference between a unit clause and a fact. — Preceding unsigned comment added by Meef4H (talk • contribs) 00:53, 29 April 2024 (UTC)

You have a point there. Indeed, the definition is based on first-order logic, without saying so. This should be fixed, thereby also explaning what "variable" means. Before this is done (I won't have time for it this week, I expect), you can get an impression about variables from the human / mortal example. A fact fitting in there could be human(socrates), where socrates is a constant. See Inference#Prolog_engine, where the classical inference example is explained. - Jochen Burghardt (talk) 11:41, 29 April 2024 (UTC)