Second intractability theorem

Theorem 4 (Second Intractability Theorem). The problem of determining whether a proposition is necessarily true in a nonmonotonic plan whose action representation employs functional operators is NP-hard. 

---