Z3 的 QnA 任务。可能吗？

Question

我正在尝试解决问答任务。有几种方法可以解决这个问题，比如深度学习方法、查询知识图、语义搜索等。但我想是否也可以使用 Z3 定理证明器来完成该任务？例如，如果我们可以将知识表示为一组公理，每个公理由谓词（关系）、主语和宾语组成，并用 FOL 子句表示，那么我们可以遍历它们并找到查询的答案（可以也可以表示为公理）。例如，我可以在 FOL 子句中编码一个简单的知识“English is language”：

exists l.(language(l) & exists n.(name(n) & :op1(n,"English") & :name(l,n)))

我怎样才能把它翻译成Z3？以及如何提取查询“{unknown} is language”的答案以找到 {unknown} 变量或子句？请注意，{unknown} 可以是任何东西。它可以是原子子句或逻辑子句，具体取决于与查询的匹配。

Answer 1

我不认为 SMT 求解器非常适合这项任务。不是因为你不能使用 z3 来做到这一点，而是像 Prolog 这样的系统或你构建的自定义程序也可以正常工作。当您结合理论（数字、算术、数组、数据结构等）时，SMT 求解器会大放异彩；对于您的问题域，您只需要一个 Prolog（如简单数据库）和一个查询引擎。

对建议的语句进行编码实际上取决于您想到的谓词类型。请注意，SMTLib 是一种“类型化”语言；所以像language(l) 这样的谓词是多余的：只有当调用类型检查时，你才会有类型语言的值；也就是说，你不能通过谓词language 任何不是语言的东西。 （这类似于使用 Haskell/O'Caml 等类型语言进行编程，而不是使用 Lisp/Scheme/Python 等动态类型语言进行编程。）

有关如何使用 SMT 求解器处理一阶逻辑建模问题的示例，请参阅 Solving predicate calculus problems with Z3 SMT。