1
$\begingroup$

In 1952 the following paper called "The Problem of Simplifying Truth Functions" was published. Quine developed the method of simplifying a truth function based on the following two theorems: enter image description here

enter image description here

The idea is to make a table of clauses of the dnf as abscissas and prime implicants as ordinates. Then we put a cross in entries where the corresponding prime implicant is subsumed by the corresponding clause. This way, if we were to choose all possible combinations of rows whose crosses in total cover all the clauses of a dnf, the minimal dnf(i.e. the simplest normal equivalent) definitely will be among the disjunctions of prime implicants corresponding to each row of each selected combination of rows. Here's an example: enter image description here

Right now, according to the theorems stated above, minimal dnf has to be among $p\bar{q} \lor \bar{p}r \lor q\bar{r}$, $\bar{q}r \lor p\bar{r} \lor \bar{p}q$.

But here's the thing: Quine didn't prove that the disjunction of the prime implicants we've constructed using this method will even be equivalent to our function. All we know is any other function cannot be a minimal dnf. But Quine stated in all his examples that all disjunctions he`d obtained were the simplest equivalents, although without any proof they'll always be such. And also I see practically everywhere where the method is used nobody bothers to check whether the obtained disjunctions of prime implicates were indeed equivalent to the function.

So is there a theorem (if there is I would like to see the proof) that all such expressions are always equivalent to the initial function, or it is not always the case and we have to check each of them?

$\endgroup$
1
  • 1
    $\begingroup$ Cross-posted to MO. $\endgroup$
    – LSpice
    Jul 20 at 17:28

0

Your Answer

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

Browse other questions tagged or ask your own question.