基于模型的量词实例化和分层排序片段 [英] Model-based Quantifier Instantiation and the Stratified Sorts Fragment

问题描述

Z3 的文档说明了基于模型的量词实例化 (MBQI):

the documentation of Z3 says for the Model-based Quantifier Instantiation (MBQI):

分层排序片段

statified sorts 片段是另一个可判定的片段排序的一阶逻辑公式.它对应于以下公式，当以 prenex 范式编写时，有一个函数级别来自排序到自然，并为每个功能

The statified sorts fragment is another decidable fragment of many sorted first-order logic formulas. It corresponds to formulas which, when written in prenex normal form, there is a function level from sorts to naturals, and for every function

(declare-fun f (S_1 ... S_n) R)

(declare-fun f (S_1 ... S_n) R)

等级(R)＜级别(S_i).

level(R) < level(S_i).

Z3 是否支持任何 prenex 范式的公式，或者仅支持所有存在量词都已通过 skolemization 删除的通用公式?

Does Z3 support any formula that is in prenex normal form, or only universal ones where all existential quantifiers have been removed by skolemization?

这会使片段更具限制性，是不是(因为 skolem 函数可能会破坏分层)?

This would make the fragment more restrictive, wouldn't it (as the skolem functions might break the stratification)?

(至少在关于 MBQI [量化 SMT 公式的完整实例化，Yeting Ge 和 Leonardo de Moura，CAV 2009] 的论文中，在我看来只涵盖了通用公式.)

( At least in the paper on MBQI [Complete instantiation for quantified SMT formulas, Yeting Ge and Leonardo de Moura, CAV 2009] it seems to me that only universal formulas were covered. )

推荐答案

你说得对.条件 level(R) 必须在所有存在量词被 skolemization 删除后满足.Skolemization 可能会引入新的未解释函数符号，它们也需要满足上述条件.

You are correct. The condition level(R) < level(S_i) must be satisfied after all existential quantifiers have been removed by skolemization. Skolemization may introduce new uninterpreted function symbols, and they also need to satisfy the condition above.

这篇关于基于模型的量词实例化和分层排序片段的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！