QnA task for Z3. Is it possible?

Question

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 can present knowledge as a set of axioms, each axiom consists of the predicates (relations), subjects and objects and is expressed in FOL clauses, then we can traverse through them and find an answer to the query (which can be expressed as axiom as well). For example, I 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 can I translate it into Z3? 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.

Answer 1

I don't think an SMT solver is very suitable for this task. Not because you can't do it using z3, but a system like Prolog or a custom-program you build will work just as fine as well. SMT solvers shine when you have combination of theories (numbers, arithmetic, arrays, data-structures, etc.); for your problem domain, all you need is a Prolog like simple-database and a query engine.

Encoding your suggested statement really depends on what sort of predicates you have in mind. Note that SMTLib is a "typed" language; so a predicate like language(l) is redundant: You'd have a value of the type language only when that call type-checks; i.e., you can't pass the predicate language anything that's not a language anyways. (This is similar to programming in a typed-language like Haskell/O'Caml etc., vs. in a dynamically typed language like Lisp/Scheme/Python etc.)

See Solving predicate calculus problems with Z3 SMT for an example of how to use an SMT solver to deal with first-order-logic modeling problems.