2: Logical Concepts and Resolution

What is the difference between syntax and semantics in logic?

Syntax defines what formulas can be written; semantics defines what they mean.

What does v |= F mean?

Formula F is satisfied by valuation v, i.e., F is true under v.

What is logical equivalence?

Two formulas F and G are logically equivalent if they have the same truth value under every valuation.

What is semantic consequence?

Formula G is a semantic consequence of F if every model of F is also a model of G (F |= G).

When is F |= G equivalent to an implication?

F |= G iff |= F → G.

What is a tautology?

A formula that is always true under any valuation.

What is a contradiction?

A formula that is always false under any valuation.

What is a satisfiable formula?

A formula that is true under at least one valuation.

What is an unsatisfiable formula?

A formula that is false under all valuations.

What is a contingent formula?

A formula that is true under some valuations and false under others.

What does |= F mean?

F is valid (true under all valuations).

What is substitution in propositional logic?

Replacing all instances of a propositional variable in a formula with another formula.

Does substitution preserve validity?

Yes.

Does substitution preserve unsatisfiability?

Yes.

Does substitution preserve satisfiability?

No, satisfiable formulas can become unsatisfiable after substitution.

Does substitution preserve logical equivalence?

Yes, if F ≡ G, then F[P := H] ≡ G[P := H].

What is the rule for interchanging equivalents?

If F ≡ G, then replacing F with G in any formula H preserves equivalence.

What is the implication equivalence for P → Q?

¬P ∨ Q.

What is the contraposition rule?

P → Q ≡ ¬Q → ¬P.

What is the double negation law?

P 𠪪P.

What are De Morgan's laws?

¬(P ∧ Q) ≡ ¬P ∨ ¬Q, and ¬(P ∨ Q) ≡ ¬P ∧ ¬Q.

What is the excluded middle?

P ∨ ¬P ≡ ⊤.

What is the contradiction law?

P ∧ ¬P ≡ ⊥.

Why are truth tables inefficient for large formulas?

They have 2^n rows for n variables, growing exponentially.

What is resolution in propositional logic?

A rule that allows deriving a conclusion from two clauses containing complementary literals.

What is a refutation?

A resolution proof that derives ⊥ (a contradiction).

How do you prove F is valid using refutation?

Show that ¬F |= ⊥.

How do you prove F |= G using refutation?

Show that F ∧ ¬G |= ⊥.

What is a clause?

A disjunction of literals.

What is CNF?

A conjunction of disjunctions of literals.

What are the steps to convert a formula to CNF?

1. Eliminate ↔ and →, 2. Push negations inward using De Morgan, 3. Eliminate double negation, 4. Distribute ∨ over ∧.

What is NNF (Negation Normal Form)?

A formula using only ¬, ∧, ∨ with ¬ only in front of variables.

What is the empty disjunction equivalent to?

⊥ (false).

What is the empty conjunction equivalent to?

⊤ (true).

What does it mean that resolution is refutation-complete?

If a set of clauses is unsatisfiable, resolution can derive ⊥.

How can CNFs be simplified?

Remove duplicate literals, tautological clauses, and subsumed clauses.

Is CNF unique?

No, the same formula can have multiple equivalent CNFs.