The formal language is a context-free language. A context-free grammar with start nonterminal symbol $S$ isThe production rule for $A$ nests one $a$ on the left and one $b$ on the right on each recursive use, so $A$ generates exactly $a^m{b}^m$ for $m\ge 0$. Similarly, $B$ generates exactly $b^n{c}^n$ for $n\ge 0$. The start production rule concatenates these words, yieldingConversely, every choice of nonnegative integers $m,n$ is achieved by using the recursive production rules exactly $m,n$ times before their epsilon productions. Hence this context-free grammar generates precisely the required formal language, including all cases where either count is zero.

The formal language is not a regular language. Let $K$ denote it and consider the infinitely many prefixesFor any $i\ne j$, append the word $z_i=(bc{)}^i$. Then $u_i{z}_i\in K$, whereas $u_j{z}_i\notin K$: the latter word has $j$ occurrences of $a$ and $i$ occurrences of $c$, and every word of $K$ has equal numbers of those two symbols.

Thus $u_i$ and $u_j$ are not Myhill-Nerode equivalent. There are infinitely many Myhill-Nerode equivalence classes, so the Myhill-Nerode theorem rules out a finite-state automaton recognizing $K$. Equivalently, if two such prefixes left a deterministic finite automaton in the same automaton state, appending $z_i$ could not distinguish their acceptance, giving the same contradiction.

The formal language is a regular language. A regular expression for it isThe first Kleene star independently chooses $m$ copies of the word $ab$, and the second independently chooses $n$ copies of $bc$. Their concatenation produces exactly the required words. Either count may be zero, including both counts zero, which gives the empty word. By Kleene theorem, the regular expression establishes regularity.

Every generated word satisfieswhere ${\#}_a,{\#}_b$ count occurrences of the indicated terminal symbols. To see this, follow the unique chain of $S$ occurrences in a parse tree. Each use of $S\to UST$ introduces one $a$ from $U$, at least one $b$ from its rightmost $T$, and possibly one further $b$ from $U\to aT$. Each use of $S\to ST$ adds one $b$ and no $a$. The terminating $S\to \epsilon$ contributes neither. Hence no generated word has more $a$ symbols than $b$ symbols.

Also, for every $n\ge 0$, the word $a^n{b}^n$ is generated: apply $S\to UST$ exactly $n$ times, choose $U\to a$ each time, then use $S\to \epsilon$ and all remaining $T\to b$.

Suppose $L(G)$ were a regular language, and let $p\ge 1$ be a pumping length from the pumping lemma for regular languages. Apply it to $w=a^p{b}^p$. Every allowed decomposition $w=xyz$ with $|xy|\le p$ and $|y|>0$ has $y=a^r$ for some $r\ge 1$. Pumping twice giveswhich violates the proved counting inequality and hence is not generated. This contradicts the pumping lemma for regular languages. Therefore $L(G)$ is not a regular language. Ambiguity was not used: the obstruction is the unbounded constraint on symbol counts.

Use the standard conversion of a context-free grammar to a pushdown automaton, implementing a leftmost derivation on a stack. Take control states $q_s,q,q_f$, input alphabet $\{a,b\}$, stack alphabet $\{S,T,U,a,b,\perp \}$, initial control state $q_s$, initial stack symbol $\perp$, and sole final control state $q_f$. The symbol $\perp$ is a fresh stack bottom marker. As in part (a), the top of the stack is written on the left.

Initialize withIn control state $q$, replace a top nonterminal symbol by one of its production rule right-hand sides:The replacements are written in the order in which they are to be processed. For example, replacing $S$ by $UST$ leaves $U$ on top; an implementation using individual push operations pushes $T$, then $S$, then $U$.

Match and pop top terminal symbols byFinally includeAll unlisted transitions have no choices; $q_f$ has no outgoing transitions. This is acceptance by final state, leaving the bottom marker on the stack. Taking the last transition too early cannot cause false acceptance, because an unread input suffix remains and $q_f$ cannot consume it.

For correctness, after initialization the stack contains the unprocessed part of a sentential form. Expanding a top nonterminal symbol simulates one step of a leftmost derivation, and popping a matching terminal symbol transfers it to the already-read input prefix. Thus if the input prefix consumed so far is $u$ and the stack above $\perp$ is $\alpha$, then $S{\Rightarrow }_G^{\ast }u\alpha$. Acceptance gives $S{\Rightarrow }_G^{\ast }w$ for the entire input $w$.

Conversely, any leftmost derivation of $w$ specifies choices of these transitions: expand the next nonterminal symbol, and read each resulting leading terminal symbol when it reaches the top. After all symbols of $w$ are consumed, only $\perp$ remains, enabling the move to $q_f$. The nondeterministic pushdown automaton therefore recognizes exactly $L(G)$. The empty word is accepted by choosing $S\to \epsilon$ after initialization.

The word $abb$ has these two leftmost derivations:In the first grammar derivation, $U\to aT$ supplies an extra $b$; the remaining $S$ goes directly to the empty word. In the second grammar derivation, $U\to a$ is used, and the remaining $S$ uses $S\to ST$ before disappearing. Every step expands the leftmost nonterminal symbol, so these are genuinely different leftmost derivations, with different parse trees already distinguished by the production rule at the $U$ node.

A context-free grammar is an ambiguous grammar if some word in its generated formal language has two distinct parse trees. Equivalently, that word has two distinct leftmost derivations from the start nonterminal symbol. A leftmost derivation always expands the leftmost remaining nonterminal symbol.

Two arbitrary grammar derivations of the same word do not by themselves prove ambiguity: expanding independent nonterminal symbols in a different order can describe the same parse tree. Requiring distinct parse trees, or distinct leftmost derivations, avoids that issue.

Use state elimination for finite automata, with regular expression labels on a generalized finite automaton. Add a fresh initial automaton state $s$ with $s\stackrel{\epsilon }{\to }{q}_0$, and a fresh final automaton state $f$ with $q_2\stackrel{\epsilon }{\to }f$. Only $f$ is now accepting. Missing labels represent the empty language, and parallel alternatives are combined by union.

When eliminating an internal automaton state $k$, update every surviving label byThe added regular expression describes entering $k$, traversing its loop zero or more times by Kleene star, and leaving it. This accounts for exactly the graph paths newly bypassing $k$.

First eliminate $q_1$. Its only incoming and outgoing labels are both $1$, and it has no loop. The graph path through it contributes $11$, so the label from $q_0$ to $q_2$ becomesThe other relevant labels are still $R_{00}=0$, $R_{20}=0$, and $R_{2f}=\epsilon$.

Next eliminate $q_2$. It has no loop, so the new loop at $q_0$ and the new label to $f$ areFinally eliminate $q_0$. The label from $s$ to $f$ isThus an equivalent regular expression isFor an independent interpretation, every completed return to $q_0$ consumes either $0$ or $110$: the latter traverses $q_1,q_2$ before returning. The last visit to $q_2$ consumes either nothing or $11$. Consequently every run of ones has length exactly two, and successive such runs require at least one zero between them. In particular, consecutive copies of $11$ without a separating zero are not accepted.

For $x$, there is an accepting graph pathIts nonempty labels spell $1100110$, and its last automaton state is accepting. Therefore $x$ is accepted. The last epsilon transition matters: finishing the consumed input at $q_0$ does not prevent a subsequent move to $q_2$.

For $y$, track all possible automaton states, including their epsilon closure, after each input prefix:

The final set contains no accepting automaton state, and $q_1$ has no outgoing epsilon transition. Therefore $y$ is rejected.

Lucy's happiness is a single antecedent, while the conclusion applies to everyone:Since $x$ does not occur in the antecedent, this is equivalent to $\forall x[H(\ell )\to M(x)]$. The universal quantifier does not assert that everyone is happy; it is the merriness conclusion that is universal.

The same person $y$ must both love $x$ and be loved by $x$:Equivalently, use $\forall x\forall y[(L(y,x)\wedge L(x,y))\to H(x)]$. There is no restriction that $x$ and $y$ be distinct; this matters when the later ground resolution proof considers Lucy loving herself.

The property of loving at least one person is the antecedent:An equivalent first-order sentence, useful for Skolemization, is $\forall x\forall y[L(x,y)\to L(x,\ell )]$. The person loved in the antecedent need not be Lucy; the conclusion concerns Lucy specifically.

The existential quantifier supplies the person loved, with a choice that may depend on $x$:The outer universal quantifier ranges over everyone. The logical disjunction is inclusive; it permits a person both to be happy and to love somebody.

The halting problem is an unconditional example:Reduce SAT to it as follows. Given a Boolean formula $\phi$, construct a Turing machine $M_{\phi }$ that ignores its input, enumerates all Boolean valuations of $\phi$, and halts if it finds a satisfying one. If none satisfies $\phi$, it enters an infinite loop after the enumeration. ThenThe construction of the machine description takes polynomial time; the potentially exponential running time of the constructed machine is irrelevant to the time needed to compute the polynomial-time reduction. Since SAT is NP-complete, this proves NP-hardness of the halting problem.

Every problem in NP is decidable, by enumerating the finitely many polynomial-length certificates and running the verifier. The halting problem is undecidable, so it is outside NP and therefore cannot be NP-complete.

For polynomial-time many-one reductions, an unconditional example is the empty language:A procedure that rejects every input decides it in constant time, so it belongs to P and hence NP. It is not NP-hard: the nonempty formal language $\{0\}$ belongs to NP, but no many-one reduction $f$ can satisfyThe right-hand side is always false. Thus the hardness condition fails without assuming $\mathsf{P}\ne \mathsf{NP}$. Giving an ordinary nontrivial problem in P would not establish the requested separation unconditionally, because that would require excluding the possibility $\mathsf{P}=\mathsf{NP}$.

Add the ground atomTogether with the three rules above, this is the Datalog with negation knowledge base $\mathcal{K}$. There are no supplied divisibility facts and no other year facts. In particular, nothing in this knowledge base asserts $DivisibleBy(N,4)$ or $DivisibleBy(N,100)$.

The remaining classification rule isThe positive premise restricts the rule to years. Its negation as failure premise is evaluated by stable model semantics; it does not assert a separately stored negative fact. This gives a stratified Datalog program: divisibility and year facts are inputs, leap status is computed next, and common status last.

Use not for negation as failure, rather than classical logical negation. The disjunctive condition is expressed by two separate Datalog with negation rules:The positive $Year(x)$ premise restricts the rule to years and makes the variable explicitly safe. The divisibility relation is input data; the integer-looking constants do not make arbitrary arithmetic facts true automatically.

Absorb (4) using the equivalenceThus we can takeHere $A⊑\neg B$ is a primitive inclusion, handled by adding $\neg B$ whenever $A$ labels a node. For literal substitution-based TBox unfolding, introduce a fresh description logic concept $A_0$ and replace the primitive inclusion byThis preserves the original models after forgetting $A_0$: any model of the primitive inclusion extends by taking $A_0=A$, and any model of the new definition satisfies the primitive inclusion. The fresh name is important. Replacing $A$ by $\neg B$ alone would incorrectly assert that every non-$B$ element is an $A$ element.

An initial split into an acyclic definition and the remaining general concept inclusions isThe definition of $C$ is suitable for TBox unfolding: its right-hand side does not depend on $C$, and $C$ has only this defining left-hand side. The other displayed general concept inclusions do not initially have an atomic defined left-hand side. In particular, $A\sqcap B⊑\perp$ can be rewritten for TBox absorption, but is not already an atomic definition.