search

fmidue / logic-tasks

0 stars 1 forks source link

umfangreicheres Beispiel für Resolution #140

Open KatinkaMeer opened 2 months ago

KatinkaMeer commented 2 months ago

Man kann ein umfangreicheres Beispiel angeben, in dem auch die Syntax gezeigt wird, für den Fall, dass man den Resolventen nicht mit einer Nummer versehen möchte.

Vorschlag: [(1,2,{A}), (3,4,{-A,-B}=6), (5,6,{-A}), ({A},{-A},{})]

vs. aktuell: [(1, 2, {A, nicht B} = 5), (4, 5, { })]

jvoigtlaender commented 2 months ago

Relevante Code-Stelle dafür ist hier: https://github.com/fmidue/logic-tasks/blob/8a9537b528e0981a048688b0df4f68cff07b3356/src/LogicTasks/Semantics/Resolve.hs#L112-L119