表推演方法

表推演方法（tableau method），理学-计算机科学技术-人工智能-机器学习-知识表示-一阶推理，通过分析公式的结构来寻找矛盾从而证明公式不可满足性的推理方法。表推演方法根据输入公式构造一棵节点标有公式的树，如果树的每个分支上都有互相矛盾的公式，则表明输入公式是不可满足的。主要内容以一阶逻辑中的表推演方法为例，进行推理时有非子句表推演方法和子句表推演两种方法。非子句表推演方法的输入是一阶逻辑公式，将输入公式标在树的根节点上。把一阶逻辑公式根据其顶层逻辑联结符的语义分为、、和四种类型（见表）。针对这四种类型有相应的规则来扩展树。当树的某分支上包含一个类型公式时，则为该分支叶节点生成儿子及后代节点，形成长度为n的链，子公式至分别标在新生成的n个节点上。当某分支包含一个类型公式时，则为该分支叶节点生成n个儿子节点，子公式至分别标在新生成的n个儿子节点上。当某分支包含一个类型公式时，则为该分支叶节点生成唯一儿子节点，标注的公式为，其中是树中从未出现的变量。当某分支包含一个类型公式时，则生成唯一儿子节点，标注的公式为，式中为树中从未出现的Skolem函数，是树中出现的全部自由变量。