Additional test for Resolution

[JNAOB]

CLOSE #258

Ein zusätzlicher Test überprüft, ob die Klauseln der generierten ResolutionInst kein Atom sowohl positiv als auch negativ beinhalten.

Hier ist die Stelle im Code, die derzeit dafür sorgt, dass der Test erfüllt wird.

[jvoigtlaender]

Ein Ergebnis von literals enthält selbst nie Duplikate? Also es kann nicht zum Beispiel auch passieren, dass darin Positive "A" und dann nochmal Positive "A" auftritt? Wenn das auftreten könnte, würde es hier dann auch zurückgewiesen, obwohl keine Tautologie vorliegt. (Also zumindest der Funktionsname wäre dann etwas dubios.)

[JNAOB]

Derzeit ist das noch so, in einem anderen PR wurde das geändert.

#274 (comment)

Allerdings stellt sich die Frage, ob dieser PR überhaupt gemergt wird.

[jvoigtlaender]

Sehe ich das richtig, dass damit #258 dann geschlossen werden könnte?

Dann sollte wahrscheinlich in dem Zuge auch gleich an Stelle dieses TODO-Kommentars:

logic-tasks/src/Formula/Resolution.hs

Line 56 in 5e914dd

lits = map Positive $ atomics c1 -- TODO: Should `literals` be used here?

tatsächlich dort literals eingesetzt werden.