解释与赋值
设为一阶逻辑公式, 是中所有的谓词, 是中所有的常量。
的一个解释(Interpretation)是一个三元组:
分别对应于个体域的具体化、谓词的具体化和常量的具体化。
在不引起混淆的情况下,有时候就用表示.
设是一阶逻辑公式的解释。一个针对该解释的赋值(Assignment)是一个将所有变量映射成具体值的映射.
一阶逻辑公式一经赋值,就成为具有确定真值的命题。
用表示一阶逻辑公式 在解释和赋值下的真值。在不引起混淆的情况下, 有时也简写成.
例: 给定解释, 试确定:
在不同解释和赋值下的真值。
解释包括:
:个体域,表示"是素数";
:个体域,表示"是偶数";
:个体域,表示"是素数";
:个体域,表示"是偶数"。
赋值根据、、和的具体个体域确定。
,,的真值如下:
解释值 带量词的公式在具体赋值下的真值:
例: :
若一阶逻辑公式在某一解释下为真, 称是的一个模型(Model), 记作: .
若一阶逻辑公式在任意解释下均为真,则称为永真式, 记作: .
否则称为存伪式(Falsible)。
若一阶逻辑公式在任意解释下均为假,则称为永假式, 否则称为可满足式(Satisfiable)。
例: 是永真式
是永假式
是可满足式
例: 判断谓词公式是否为永真式。
解: 任意给定个体域, 假定在该解释下为真, 则对于任意, 均有为真, 因此也为真。
故为永真式。
例: 判断谓词公式是否为可满足式。
解:定义解释:个体域上为整数集,
表示是整数, 表示是有理数。
在解释下, 为真。
所以是可满足式。
设为一组一阶逻辑公式, 是中所有的谓词, 是中所有的常量。
的一个解释是一个三元组:
分别对应于个体域的具体化、谓词的具体化和常量的具体化。
针对的赋值是将所有变量映射成具体值的一个映射.
若一组一阶逻辑公式在某一解释下为真(对于任意, ), 称是的一个模型, 记作: .
若一组一阶逻辑公式在任意解释下均为真,则称为一组永真式, 记作: .
否则称为一组存伪式。
若一组一阶公式在任意解释下均为假,则称为一组永假式, 否则称为一组可满足式。