Interactive study tool

First-Order Logic

Translate statements to FOL and CNF, then follow a resolution proof. Work through each exercise, check it instantly, and use the explanation to close any gaps.

✓ Answers stay in this browser · no network calls

Vocabulary and CNF recipe

G(x): x has a gene; C(x): x is a carrier; D(x): x exhibits the condition; F(x)/M(x): father/mother of x.

  1. Eliminate ⇒ and ⇔.
  2. Push negation inward.
  3. Standardize variables apart.
  4. Skolemize existentials.
  5. Drop universal quantifiers and distribute ∨ over ∧.

1. Translate a disjunction

“Anyone with the gene either exhibits the condition or is a carrier.”

2. Split a conjunction

“If someone exhibits the condition, both parents have the gene.”

3. Preserve “at least one”

“If someone is a carrier, at least one parent has the gene.”

4. Complete a resolution proof

To prove D(v)⇒(G(M(F(v)))∨G(F(F(v)))), negate the goal using a fresh constant a: D(a), ¬G(M(F(a))), ¬G(F(F(a))). Choose the key resolvent at each stage.