Here is a very simple problem for children, and I wonder if we can use mathematical logic(like "propositional logic" or "first order predicate logic", or others) and an automatic solver? Which means: formalize the statement of the problem, enter the formalized statement into the automatic solver, get an answer
- There are 3 teachers, Mike, Jack and John.
- One teaches art, one teaches music, and one teaches writing.
- Mike is older than whom teach music.
- Jack is younger than whom teach art.
- John is older than whom teach art.
Question: What do the 3 teachers teach?
Yes, we can do this with formal logic.
The given information can be formalized as follows:
$$\forall x (x = mike \lor x = jack \lor x = john)$$
$$\exists x (Art(x) \land \forall y (Art(y) \rightarrow y=x))$$
$$\exists x (Music(x) \land \forall y (Music(y) \rightarrow y=x))$$
$$\exists x (Writing(x) \land \forall y (Writing(y) \rightarrow y=x))$$
$$\forall x (Music(x) \rightarrow Older(mike,x))$$
$$\forall x (Art(x) \rightarrow Younger(jack,x))$$
$$\forall x (Art(x) \rightarrow Older(john,x))$$
together with some further fundamental truths:
$$\forall x \neg Older(x,x)$$
$$\forall x \forall y \forall z ((Older(x,y) \land Older(y,z)) \rightarrow Older(x,z))$$
$$\forall x \forall y (Older(x,y) \leftrightarrow Younger(y,x))$$
Any decent automated prover will be able to infer the answer from this information.