General Updates on the Tuesday Morning Tutorial tutored by Max Rapp
Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.
This morning I could not quite come up with an example of a fragment of propositional logic that is decidable in polynomial time. What I intended was HORNSAT which is satisfiability over the set of Horn clauses defined as the disjunctive normal form formulas that have only one positive (not-negated) literal, i.e. “a or not b or … not c”. Horn formulas are arbitrary (including unary) conjunctions of horn clauses.
There are linear algorithms to decide whether a given Horn-formula is satisfiable, so HORNSAT is in P.
You might want to note that using equivalence between “not a or b” and “a => b” the above horn clause can be rewritten as b and … and c => a, or in Prolog notation “a :- b, …, c”.