I fail to find much about how to efficiently calculate whether a propositional formula entails another.

Considering the following two points...

  1. We can check, for each truth assignment which makes the first formula true, whether it also makes the second true. If all of them do, the first entails the second. It works for disjunctive normal forms, conjunctive normal forms, ... anything really. But this can be prohibitively expensive for large numbers of propositions.
  2. If we translate both formulas to disjunctive normal form we can more efficiently check for entailment, but we need to do the transformation to DNF first.

... what are the best algorithms to check entailment?

I was under the impression that this must be a problem that's long been solved, but where are the papers that deal with entailment of arbitrary propositional formulas? How do I calculate a yes/no answer without using DNFs?


Checking whether $P \Rightarrow Q$ is the same as checking that $P \land \lnot Q$ is unsatisfiable. Using the Tseytin transformation, you can convert $P \land \lnot Q$ into a form suitable for a SAT solver.

Conversely, satisfiability is a special case of your problem, since $P \Rightarrow \bot$ iff $P$ is unsatisfiable.

  • $\begingroup$ What is the advantage of transforming to CNF (which Wikipedia tells me is the result of a Tseytin transformation) and then solving as opposed to transforming to DNF and then solving? I'm more interested in understanding the algorithms, less so in quickly implementing the best practical way to solve a given problem. $\endgroup$
    – Higemaru
    Jun 16 '20 at 11:04
  • $\begingroup$ SAT solvers solve the satisfiability problem, which doesn't make much sense for DNFs (it's very easy). $\endgroup$ Jun 16 '20 at 11:05
  • $\begingroup$ The point of this answer is that your question is a special case of SAT. We already know how to solve SAT in practice – that's the area of SAT solving. $\endgroup$ Jun 16 '20 at 11:06
  • $\begingroup$ Yes, does that mean your answer includes "look at algorithms for SAT solvers" in some way? Solving my problem using DNFs seems pretty straight forward, but I thought one might be able to solve it without transforming into a normal form first. $\endgroup$
    – Higemaru
    Jun 16 '20 at 11:11
  • $\begingroup$ Satisfiability is a special case of your problem. $\endgroup$ Jun 16 '20 at 11:12

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.