ChatGPT understands First Order Logic

If you've taken a logic course, there's a good chance that you've learned about Wumpus World - a game from the 1970s that inspired AI experiments in logic.

As a refresher, Wumpus World is a game played on a grid where a gold reward and hazards such as pits and wumpuses (a monster-like creature) await you. You can't see the gold or hazards, but you can sense them through glitter, breezes and stenches respectively. When you sense any of them, it's an indication that an associated item is in a horizontally or vertically adjacent square. Below is an example of a Wumpus World board.

Sounds like a fun game, but how is a motivated game player to keep track of all those glitters, breezes and stenches and know how to move? An effective way is by using First Order Logic (FOL). The set of games rules is maintained as clauses. For example, "all cells next to the cell of Wumpus will sense a stench" can be expressed as:

Stench(a,b)??c,d:(Adjacent([a,b],[c,d]) ∧ Wumpus(c,d))         

and "all cells next to the cell of a pit will sense a breeze" as:

Breeze(a,b) ? ?c,d:(Adjacent([a,b],[c,d]) ∧ Pit(c,d))        

Using the Stench and Wumpus rule, how can we derive that a Wumpus does not exist at [1,3] if a Stench was not sensed at [1,2]? We can convert the rule, observations and conclusion into Conjunctive Normal Form clauses resulting in:

(Stench[1,2] ? (Wumpus[1,3] ∨ Wumpus[2,2])) #bi-directional implication
?Stench[1,2] #observation - no stench sensed at [1,2]
?Wumpus[1,3] #conclusion - no wumpus at [1,3]        

Then conjunct them resulting in:

(Stench[1,2] ? (Wumpus[1,3] ∨ Wumpus[2,2])) ∧ ?Stench[1,2] ∧ Wumpus[1,3]        

Using proof by negation and resolution, it can be derived at Wumpus[1,3] (the negation of no Wumpus at 1,3) is derived.

The above process is taught and learned by students every year, so I'm not demonstrating anything revolutionary. But...what if an artificially intelligent agent could perform this task without any specific training in the problem itself? This is what I did with ChatGPT. Below is a transcript of a ChatGPT interaction that I had to show how this works.

And ChatGPT understands FOL quantifiers:

Beyond the obviously fun aspect of playing Wumpus World, ChatGPT's ability to deduce and infer using First Order Logic opens up interesting possibilities of rule-based problem solving using ChatGPT as the agent. Creating an LLM with pre-built FOL predicates and clauses would allow users to reason over problems effectively and in a scalable way.

If you've used ChatGPT in this way, please reach out so we can discuss.