Tell me more ×
Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It's 100% free, no registration required.
up vote 0 down vote favorite
1

I need to convert this statement to CNF (Conjunctive normal form):

$\qquad \left((\forall x.\, P(x)) \implies Q(a)\right)\implies \left((\exists y.\, P(y)) \implies Q(a)\right)$

I got this answer:

$\qquad \begin{align} &\left((\forall x.\, P(x)) \lor (\forall y.\, \neg P(y))\right) \\ \land &\left((\forall x.\, P(x)) \lor Q(a) \right)\\ \land &\left(\neg Q(a) \lor (\forall y.\, \neg P(y))\right) \end{align}$

Is it correct? Is there any useful site that I can use to convert statements to CNF?

share|improve this question
It is not clear whether $\forall x$ resp $\forall y$ binds only $P(\_)$ or the respective implications $P(\_) \implies Q(a)$. Please check whether we got it right. – Raphael♦ Feb 2 at 21:15
1  
Are you certain you intend to use conjunctive normal form? For first-order logic, clausal normal form seems to make more sense. (Also, "check my homework"-type questions are boring. Do you have any conceptual problems?) – Raphael♦ Feb 2 at 21:18

migrated from stackoverflow.com Feb 2 at 17:05

Know someone who can answer? Share a link to this question via email, Google+, Twitter, or Facebook.

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.