QnA task for Z3. Is it possible?

[PolKul]

I'm trying to solve a question answering task. There are several approaches to this like Deep Learning methods, querying Knowledge Graphs, Semantic Search etc. But I thought if it would be possible to use Z3 theorem prover for that task as well? For example, if we present knowledge as a set of axioms, each axiom consists of the predicates (relations), subjects and objects and is expressed in FOL, then we can traverse through them and find an answer to the query (which can be expressed as axiom as well). For example, we can encode a simple knowledge "English is language" in FOL clause:
exists l.(language(l) & exists n.(name(n) & :op1(n,"English") & :name(l,n)))
How would you translate it into Z3? And how can we extract an answer to the query "{unknown} is language" to find an {unknown} variable?

[NikolajBjorner]

This is a very long story.

It is outside the scope of mainstream uses of z3, but I have seen one or two over time.
For example, the EPR fragment is sufficient for many scenarios.
Witness creation using z3 models is different from resolution answer literals, though,
so you might find some issue with mapping what is in a Prolog textbook into z3.

[PolKul]

Thanks @NikolajBjorner for your answer. I'm a programmer, but I'm new to Z3. Would you mind helping me with the basic example code? For example, I'm able to encode the above clause as follows:

from z3 import *

s = Solver()

l = Const('l', Object)
n = Const('n', Object)

language = Function('language', Object, BoolSort())
name = Function('name', Object, BoolSort())
op1 = Function('op1', Object, StringSort(), BoolSort())

s.add(ForAll(l, Implies(language(l), Exists(n, And(name(n), op1(n, StringVal("English")))))))

x = Const('x', Object)
print(s.check())
print(s.model())

But I'm not sure if this is the correct way of doing it? And how can I extract an answer to the query "{unknown} is language" to find an {unknown} variable or clause? Note that the {unknown} can be anything. It can be an atom or logical clause depending on the match with the query.