4
1.0
\(\def\future{\mathord{\raise0.1em{\Diamond}}}\) \(\def\always{\mathord{\raise0.05em{\Box}}}\) \(\def\next{\mathord{\raise0.15em{\scriptsize\bigcirc}}}\)
Vilka av följande är sant om Horn-klausuler?
Vad är sant för SLD-resolution?
Tag klausulmängden \(U=\{p(a,a),\lnot p(a,a)\}\). Vilka av följande är sant?
Antag att \(A\) är en valid satslogisk formula. Vilka av göljande gäller då i LTL?
Antag att \(A\) är en satisfierbar satslogisk formula. Är \(\future A\) då valid i LTL?

Nedanstående kod är det du lämnar in som en del av laborationen. Dubbelkolla att allt ser ut att stämma!