Z3が要素のないソートを提案できないのはなぜですか？

Question

Z3Pyを使用して、Z3が決定するプログラムを構築しようとしましたが、Humanの種類は空です。

from z3 import * 
from z3_helper import Z3Helper 

Human = DeclareSort("Human") 
is_mortal = Function("is_mortal", Human, BoolSort()) 
h = Const('h', Human) 

s = Solver() 
s.add([ 
    ForAll([h], And(is_mortal(h), Not(is_mortal(h)))) 
]) 

print s.check() 
s.model() 

しかし、その代わりHumanが空のモデルを返すので、それはunsatを返します。どうしてこれなの？

「すべての人が死ぬ」公理を削除すると、モデルとして空のセットが返されます。

const hの存在は、少なくとも1つのHumanの存在が必要であることを意味しますか？

Answer 1

SMT-LIBとZ3は、単純に型指定された一次論理では、すべてのソートが空ではないとみなしているという見解を示しています。セクション8.1以降のhttp://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-draft-3.pdfも参照してください。