0

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.

user2222943
  • 15
  • 3

1 Answers1

0

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.

alias
  • 28,120
  • 2
  • 23
  • 40
  • Thanks for your answer. The idea is to be able to use some symbolic inference engine for logical reasoning rather than trying to find an answer with the statistical methods. So I thought that some automated theorem prover might work for this. I was also looking into Lean prover. I could use GPT-f (trained on Lean) for inference automation. But I think Z3 may work for that as well. I just need to figure out how to translate this FOL clause into Z3 to find an answer as the result of inference which would involve query axiom and the knowledge axioms... – user2222943 Nov 27 '21 at 08:58