Neue Frage

Linear clause form

gefragt 2017-08-25 12:14:14 +0200

Dieser Post ist als Wiki-Post markiert

Das ist ein Wiki-Beitrag. Jeder mit Karma >75 darf diesen Beitrag verbessern.

aktualisiert 2017-08-25 12:14:14 +0200

arsinux Gravatar-Bild

as an answer can I just write {!a, !c}, {!d, b} as is written in the solution of question 1_a of exam of 2015.10.15?


bearbeiten retag Als beleidigend melden schließen löschen

2 Antworten


geantwortet 2017-08-25 12:33:45 +0200

PS Gravatar-Bild

I found that question in the exam of February 15, 2017 but not in the exam you mentioned.

No, that would not be an appropriate answer in my opinion. Of course, what you list is an equivalent clause form, but one cannot see how you have computed it and how that would only lead to a linear blow-up, if you would apply your algorithm to other formulas.

If you just compute a CNF, you know the effort would be exponential in the worst case which has to be avoided by abbreviating subformulas with new variables. So, you should abbreviate the subformulas one by one and then you should generate clauses for the obtained abbreviations as given in the example solutions.

Remark: It is clear that in this example, the linear clause form transformation generates a way bigger clause set. However, for practical examples that is not so, it is a matter of scaling that does not really show up with small exam problems. Nevertheless, the procedures are extremely important in practice.

bearbeiten Als beleidigend melden löschen publish Link mehr

geantwortet 2017-08-25 12:31:46 +0200

Unlike Disjunctive Normal Form and Conjunctive Normal Form, Linear Clause Form is not just a syntactic specification but a strict procedure of converting formulae in propositional logic.

It's precise procedure has been defined in your lecture notes. The key idea is that you introduce a variable for each node in the syntax tree. You then add conjunctions of equivalences. Each equivalence uses (up to) three variables. It ensures that the variable of a node has the same value as the result of the logic connective and the (up to) two children of the node.

Algorithmically, it creates a list of equivalences and then converts them to a conjunction where the equivalences are expressed in CNF.

bearbeiten Als beleidigend melden löschen publish Link mehr

Ihre Antwort

Du kannst deinen Eintrag bereits als Gast verfassen. Deine Antwort wird zwischengespeichert, bis du dich eingeloggt oder registriert hast.
Bitte nur konstruktive Antworten auf diese konkrete Frage posten.
Falls du eine Frage stellen willst, dann stelle eine neue Frage.
Für kurze Diskussionen und Nachfragen benutze bitte die Kommentar-Funktion.
Deine Fragen und Antworten kannst du jederzeit nachbearbeiten und verbessern.
Gute Fragen und Antworten kannst du mit einem Upvote oder Downvote bewerten.

Schreibe deine Antwort auf diese Frage

[Vorschau ausblenden]


1 Follower


Gefragt: 2017-08-25 12:14:14 +0200

Gesehen: 29 mal

Letztes Update: Aug 25