Diskussion:Horn-Formel

Es sollte noch ein wenig auf Horn-Klauseln /-Formeln in der Prädikatenlogik erster Stufe eingegangen werden. Momentan sieht es ein wenig seltsam aus, wenn zuerst gesagt wird, das Horn-Klauseln aussagenlogische Klauseln sind, später aber von Prolog die Rede ist. --zeno 16:52, 30. Jun 2005 (CEST)

Sprache

Hm, was ist denn mit dem Bearbeitungskommentar "Sch Dreck ist ja falsch" [1] gemeint? Die damit eingebrachte Formulierung "das heißt eine Konjunktion = durch Und-Verknüpfung von Disjunktionen = Oder-verknüpften einfachen Termen)" ist ungrammatisch, und eine Horn-Formel ist eine KNF, deren jedes Konjunkt eine Disjunktion mit höchstens einem unverneinten Literal ist... Siehe auch die Beispiele in Horn-Formel#Darstellungsformen_von_Horn-Klauseln oder, wenn der "Sch Dreck"-Kommentator externe Quellen wünscht, http://www-ai.cs.uni-dortmund.de:8765/lexikon/theorie/logik/node2.html#Hornformel (Definition 1.6) und beliebige andere. Ich stelle daher einmal die grammatische Version wieder her. --GottschallCh 09:23, 12. Okt. 2007 (CEST)

Das ist nach http://www-ai.cs.uni-dortmund.de:8765/lexikon/lexikon.html von Uschi Robers 6.2.1998 geschrieben und sieht nach Studienarbeit o.ä. aus, Der server gehört aber dem ai-Institut. Ist also als Quelle nur bedingt brauchbar, etwa als unwidersprochene Meinung in einer wissenschaftlichen Bearbeitung.

Mir ging es vor allem um die omataugliche Formulierung. In der Bezeiehung ist die anschliessende Erklärung mit Besipiel und Hornklauselabsatz ein diskutierbarer Ansatz. Der Hinweis auf den Uniserver bietet mit seiner KNF und DNF eine Abküfi-Formulierung, die eigentlich nicht WP-tauglich ist. Andererseits schwirren in verschiedenen Prolog-Handbüchern widersprüchliche Definitionen rum, gegen die eine WP-Formulierung eine Begriffsfindung geschimpft werden könnte. Mir wäre ne Quelle lieber, die man als anerkannte Lehrmeinung bezeichnen kann, also etwa ein Uni-Lehrbuch. Ich werd mal mit den Dortmunder Uni-Mitarbeitern versuchen weiterzukommen. --SonniWP✉✍ 12:31, 12. Okt. 2007 (CEST)

Erfüllbarkeit

Der Abschnitt Erfüllbarkeit sollte überarbeitet werden, erst spricht man davon, dass es einen Markierungsalgorithmus gibt. Und dann kommt auf einmal zur Sprache, dass Horn-SAT P-Vollständig ist. Desweiteren wird hier die P-Vollständigkeit erläutert. --DangerGround

Ausserdem ist der verlinkte Artikel zu HORNSAT eine Weiterleitung auf diesen Artikel selbst (Horn-Formel), folglich sollte man diesen Algorithmus evtl. in dem Abschnitt zur Erfüllbarkeit erläutern. --DangerGround 22:38, 18. Aug. 2009 (CEST)

Überarbeitung und Quellen

Ich habe den grössten Teil überarbeitet (die letzten beiden Abschnitte bisher noch nicht). Störende Überschneidungen mit Markierungsalgorithmus sehe ich nicht. Dhanyavaada 17:09, 27. Sep. 2009 (CEST)

Änderung in Tabelle

Hab mal in der Tabelle "x1..xn sind alle nicht wahr" in "sind nicht alle wahr geändert"

$x1\wedge \dots \wedge xn\to 0$ ist nicht erfüllt wenn irgend eine der verundeten Variablen nicht wahr ist. Eine reicht also aus.

Kommentar kann wieder weg wenn die Änderung angenommen ist, wusste nur erstmal nicht, wo ich das hinkippen soll. (nicht signierter Beitrag von 195.160.172.2 (Diskussion | Beiträge) 02:48, 1. Feb. 2010 (CET))

Die betreffende Zeile in der Tabelle bezieht sich auf Formeln, in denen wirklich kein nichtnegiertes Literal auftritt. Die Bemerkung über den Wahrheitswert ist zwar richtig, aber es geht um HORN-Formeln. --TeesJ 08:40, 4. Feb. 2010 (CET)

Auch für Hornformeln gilt die normale Logik. "nicht a oder nicht b" bedeutet, dass mindestens eines von beiden falsch ist, nicht notwendigerweise beide. Sollte etwas anderes als normale logische Evaluierung gemeint sein, dann sollte das kenntlich gemacht werden. (nicht signierter Beitrag von 78.34.232.253 (Diskussion) 00:17, 12. Mai 2010 (CEST))

Die Überschrift der von Dir geänderten Spalte lautet: In Worten. Das heißt, es ist keineswegs die normale logische Evaluierung gemeint, sondern die sprachliche Umschreibung dessen, was die Zielklausel als Horn-Formel darstellt, und das ist auch kenntlich gemacht. Bitte die erste Zeile der Tabelle in Zukunft unverbessert lassen! --TeesJ 19:30, 15. Mai 2010 (CEST)

Keine mir denkbare Interpretation ("sprachliche Umschreibung") der Zielklausel entspricht allerdings "x_1,...,x_n sind alle nicht wahr". Die Zielklausel, interpretiert als Aussagenlogische Formel, bedeutet "x_1, ... , x_n sind nicht alle wahr". Die Zielklausel, interpretiert als Abfrage in der logischen Programmierung (PROLOG), bedeutet "sind x_1, ... , x_n wahr?". Erfüllbarkeit entsprechend. Offenbar bin ich nicht der erste, der darüber stolpert. Aufgrund des obigen Diskussionsbeitrages korrigiere ich den Artikel jetzt noch nicht, aber bitte das im Artikel erläutern, wenn "In Worten" etwas anderes als die von mir erläuterten Interpretationen bedeuten. Ansonsten ist dieser Eintrag nämlich falsch. --78.34.200.80 04:33, 16. Mai 2010 (CEST)

Bitte um Entschuldigung, die letzte Spalte meint tatsächlich "Implikation in Worten". Ich korrigiere wunschgemäß.--TeesJ 06:00, 16. Mai 2010 (CEST)