The convention of a cover math is to use lower case letters as constants, upper case letters as operators, Greek letters as variables, any combination of which is an expression symbolized by an arabic number or Greek number for a variable expression, and can be rewritten under certain rules.
Suppose you have certain constants that you symbolize with lower case letters:
the room = r
the blue ball = b
the brown box = x
the red ball = y
the green pyramid = p
the table = t
and you have certain operators you symbolize with upper case letters:
is inside of = I
is outside of = O
is on top of = T
is underneath = U
is next to = N
and = A
And you have certain axioms about the system that appear as rewriting rules, using greek letters alpha, beta etc for variables that can take the value of any constant.
Those under expressions say if you end up with two expressions that are identical with an and in between, you can rewrite it as just one. And the second says if you have two expressions, you can combine them with an AND to get a third.
Now we have to add to those descriptive axioms describing our situation...
And from these many statements can be proven. We can find that the blue ball is inside the room for example , even though not explicitly stated, by adding 1 and 2 together with A by the last rule, and then using the transitive axiom for "is inside of".
We could ask a proof machine whether "the red ball is next to the brown box" for example and it could see whether it was deducible from what it was given.