Questions: First-Order Logic for AI

Question 1

An AI theorem prover is given a FOL knowledge base and a query. It runs for an hour without returning a result. What does this most likely indicate?

• A. The knowledge base contains a logical contradiction
• B. The theorem prover has a bug; correct FOL provers always terminate
• C. The query may not follow from the knowledge base, and FOL's semi-decidability means the prover may never halt in this case
• D. The knowledge base is too large for FOL; it should be replaced with propositional logic

Answer: (C)

FOL is semi-decidable: if a conclusion logically follows from the premises, a complete theorem prover will eventually find a proof. But if the conclusion does NOT follow, the prover may run forever without halting — there is no general algorithm that can always determine 'this query has no proof.' This is a fundamental mathematical limit proved by Church and Turing, not a software bug. Non-halting is the expected behavior when a query has no proof in FOL, and it is one reason practical AI systems often use restricted decidable fragments instead.

Question 2

Why do practical AI systems often use Horn clause logic (the basis of Prolog) instead of full first-order logic?

• A. Horn clauses are more expressive than full FOL, allowing richer knowledge representation
• B. Horn clauses are decidable and support efficient resolution-based inference, trading expressiveness for guaranteed termination
• C. Full FOL cannot represent universal quantification, which Horn clauses handle natively
• D. Horn clauses avoid the need for a knowledge base, making systems easier to deploy

Answer: (B)

Full FOL is semi-decidable and computationally intractable in general. Horn clauses restrict logical statements to a form (head :- body, with at most one positive literal) that makes inference decidable and practically efficient via SLD resolution. You lose some expressive power — disjunctive conclusions are not directly representable — but you gain the guarantee that queries either return an answer or terminate with failure. This expressiveness-tractability tradeoff is the central design decision in FOL-based AI systems.

Question 3

First-order logic is decidable — given any FOL formula and a set of axioms, an algorithm can typically determine in finite time whether the formula follows from the axioms.

• T. True
• F. False

Answer: False

FOL is only semi-decidable: if a formula follows from the axioms, a complete theorem prover will eventually find a proof. But if it does not follow, the algorithm may loop forever without halting. Decidability — the guarantee that the algorithm always terminates with a correct yes/no answer — holds for propositional logic and certain restricted fragments of FOL (such as Horn clauses), but not for full FOL. This is a proven mathematical result, not a limitation of current technology.

Question 4

Universal instantiation allows an inference engine to derive specific conclusions from universally quantified statements — for example, deriving 'Tweety flies' from '∀x (Bird(x) ∧ ¬Penguin(x) → Flies(x))' combined with 'Bird(tweety) ∧ ¬Penguin(tweety)'.

• T. True
• F. False

Answer: True

Universal instantiation is a fundamental FOL inference rule: from ∀x P(x), you can substitute any specific term for x and conclude P(that term). Here, substituting 'tweety' for x gives 'if Tweety is a non-penguin bird, Tweety flies.' Combined with the facts Bird(tweety) and ¬Penguin(tweety) via modus ponens, we derive Flies(tweety). This type of chained reasoning — universal instantiation followed by modus ponens — is the core mechanism of FOL-based inference engines.

Question 5

What is the fundamental tradeoff between expressiveness and tractability in FOL-based AI, and how do restricted fragments like Horn clauses address it?

Model answer: Full FOL can represent predicates, quantifiers, variables, and complex relationships — but its inference problem is semi-decidable and intractable in general, meaning a theorem prover may never halt for some queries. Restricted fragments trade expressiveness for computational guarantees. Horn clauses limit each formula to at most one positive literal, enabling efficient SLD resolution and making inference decidable. Description logics make similar tradeoffs, gaining decidability while preserving enough expressiveness for ontological reasoning. The cost in both cases is the inability to directly represent certain kinds of knowledge, such as disjunctive conclusions.

The tradeoff determines which domains FOL is practical for. Where expressiveness and provable correctness matter most — formal verification, safety-critical planning — the full power of FOL is worth the computational cost. Where scale and speed matter — large knowledge graphs, real-time systems — restricted decidable fragments are essential.