Det formella systemet MIU beskrivet av författaren Hofstadter i boken Gödel, Escher, Bach arbetar på strängar som kan innehålla symbolerna m, i och u, t.ex mii, mu, iiuuii och uuuu. Det finns fyra härledningsregler för hur strängar kan omvandlas:
 

1. Om sista symbolen är i kan u tillfogas strängen, t.ex uii blir uiiu.
2. Om hela strängen är mX där X är en godtycklig sträng så kan mX omvandlas till mXX, t.ex miiu blir miiuiiu.
3. Om en sträng innehåller tre i på rad (iii) kan dessa ersättas av u (iii kan finnas på en godtycklig plats i strängen), t.ex miiii kan meddenna regel förvandlas till mui eller miu.
4. Om en sträng innehåller två u på rad (uu) kan dessa plockas bort (de kan finnas på godtycklig plats i strängen), t.ex miuu blir mi och iiuui blir iii.

steg 1. Vi utgår från mi.
steg 2. mi blir mii enl. regel 2.
steg 3. mii blir miiii enl. regel 2.
steg 4. miiii blir mui enl. regel 3. (miu hade också kunnat erhållas)
steg 5. mui blir muiu enl. regel 1.
steg 6. muiu blir muiuuiu enl. regel 2.
steg 7. muiuuiu blir muiiu enl. regel 4.

Vi har lyckats visa att muiiu är ett teorem (kan härledas med hjälp av reglerna) om man utgår från strängen mi (axiom).

Uppgift 1

Man vill nu låta ett sökprogram ta reda på om muiui är ett teorem om man utgår från axiomet mi. Er uppgift är att deklarera predikatet successor så att detta och liknande problem kan lösas i MIU-systemet. Dessutom skall predikatet final_state deklareras för just detta problem.

Uppgift 2

Kan ovanstående sökproblem lösas med depth-first search algoritmen? Motivera ditt svar.

Uppgift 3

Modifiera programmet depth-first search så att sökningen ej sker bortom ett specificerat djup. Djupet skall anges som ett argument till predikatet. Visa hur anropet av predikatet skall se ut för att sökproblemet beskrivet i uppgift 1 skall kunna lösas.

Uppgift 4

Modifiera programmet breadth-first search så att besökta tillstånd ej besöks igen.