Questions tagged [conjunctive-normal-form]
A formula is in conjunctive normal form (CNF) if it is a conjunction of clauses, where a clause is a disjunction of literals.
205
questions
1
vote
1
answer
601
views
Convert $A⟺B⟺C$ into Conjunctive Normal Form.
Eliminate implications and bi-conditionals using formulas:
$A⟺B⟺C$
Attempt:
$≡ (A⟹B)∧(B⟹A)⟺C$
$≡ (((A⟹B)∧(B⟹A))⟹C)∧(C⟹((A⟹B)∧(B⟹A)))$
$≡ ¬((A⟹B)∧(B⟹A))∨C ∧ ¬C∨((A⟹B)∧(B⟹A))$
$≡ ¬((¬A∨B)∧(¬B∨A))∨C ...
- 25
2
votes
2
answers
455
views
Converting to conjunctive normal form?
How to convert to conjunctive normal form?
If i have a formula:
$(\neg Q\land P) \lor (\neg Q\land R) \lor (Q \land \neg P \land \neg R) \lor (\neg P \land \neg R)$
The formula is in disjunctive ...
- 23
0
votes
1
answer
41
views
How many subsets of size $n$ in $S=\{x_1,\dots ,x_{2n}\}$ under restrictions
Let $S=\{x_1,\dots ,x_{2n}\}$. How many subsets of size $n$ are in $S$ such that $\forall1\le i\le n: x_i$ and $x_{n+i}$ are not in the same set.
I ran into this problem when thinking how many ...
- 375
2
votes
0
answers
44
views
I don't know that this solution is right
I have the statement ∃xP(x) ↔ ∃xQ(x) and I have to write it in prenex normal form.
First I rewrote it as two conditionals:
∃xP(x) ↔ ∃xQ(x)
≡(∃xP(x) → ∃xQ(x))∧ (∃xQ(x) → ∃xP(x))
Then I renamed the ...
- 21
2
votes
2
answers
375
views
Why Does Order of Negation Matter in First Order Logic Resolution?
Consider the situation in which we have $f(A)$ as a given and are attempting to show that $\exists x f(x)$.
Using resolution, we negate the conclusion, convert everything to CNF, and attempt to ...
- 125
6
votes
2
answers
7k
views
How to compute CNF from truth table
How can I write a propositional formula with variables p, q, r in a CNF that has 3 models v1, v2, v3:
I've failed to find any related sources.
- 163
1
vote
1
answer
136
views
Is Predicate Resolution the Only Way To Reduce The Size CNF Clauses?
I have a CNF formula like $(x_1∨x_2∨x_3') ∧ (x_1' ∨ x_4 ∨ x_2)$ ...
Perhaps I want to see if the equation is equivalent to a CNF equation containing a single literal ($x_2$ for example).
I already ...
- 21
1
vote
3
answers
48
views
How to convert (F⇒(H⇒G))⇒(F⇒(G⇒H)) to Conjunctive Normal Form?
I've expanded the formula to:
$$(F \wedge H \wedge\neg G) \vee (\neg F \vee\neg G \vee H)$$
but don't know how to switch the first set to or and the middle or to an and.
- 21
0
votes
2
answers
106
views
What paper proved the completeness of Ordered Resolution?
I am having trouble finding online the original proof of the completeness of Ordered Resolution. Does anyone happen to know where it exists?
Thanks!
- 43
0
votes
1
answer
316
views
How to convert this formula to CNF
I have the following formula and want to turn it into CNF without creating a truth table:
~((X -> ~(Y or Z)) and ((X and Y) or ~Z))
I was doing the following ...
- 5
1
vote
2
answers
155
views
Constructive proof layers-norm (propositional logic)
I have to write a constructive proof that for every propositional formula has an equivalent formula in Layers-Norm
We define Layer-Norm for propositional formulas as follows:
Literals are in Layer-...
- 115
0
votes
1
answer
126
views
Task about Conjunctive and Disjunctive normal form.
Happy new year to all!
I have a question related to my Discrete Mathematics examination:
Consider the following (parametrized) propositional formula $𝜑_𝑛$:
($p_1$V$p_{2n+1}$) & (!$p_1$V!$p_2$)...
1
vote
1
answer
473
views
Simplifying boolean expression to minimum CNF
I have the boolean expression,
$$(a\not\to b)\lor(c\not\to d)\lor(a\not\to d)\lor(b\not\to d)$$
Can I simplify this to,
$$ (a \vee c \vee b ) \wedge (a \vee \neg d) \wedge (\neg b \vee \neg d) $$
...
- 35
0
votes
1
answer
665
views
Converting to DNF from CNF
I'm having a bit of a problem when trying to convert this CNF formula to DNF:
\begin{align}
& \left(a_1 \vee \neg a_2 \vee \neg a_3 \vee ... \vee \neg a_K \right) \wedge \\
& \left(\neg a_1 \...
- 1
0
votes
1
answer
213
views
CNF simplification
I would like to know if it is possible to simplify the CNF equation. I have this equation -
$$
(x_{1} \lor x_2 \lor \lnot x_3 \lor \lnot x_4) \land (x_1 \lor \lnot x_2 \lor x_3 \lor \lnot x_4) \land (...
- 3