合金中矛盾事实的一致性检验

Question

我不明白合金中的事实是如何工作的。在这个小示例中，有两个相互矛盾的事实，但是谓词testWithoutParameters找到了一个实例(不是预期的)，而谓词testWithParameters不是(预期的)。这两个断言都没有在应该这样做的时候找到反例。我的解释中的错误在哪里？代理代码和执行的输出。

sig A{
    aset: set B
}

sig B{
    bset: set B
}

fact Rule_1{
    all a: A |
    #a.aset < 3
}

fact Rule_2{
    all a: A |
    #a.aset > 3
}

pred testWithoutParameters[]{
    all a:A |
    #a.aset = 3
}

pred testWithParameters[a:A, b:B]{
    #a.aset = 3
}

assert test_aset{
    all a:A |
    {
        #a.aset = 3
    }
}

assert testWithoutSense{
    all a: A |
    #a.aset > 3 and #a.aset < 3
}

run testWithParameters for 10
run testWithoutParameters for 10
check test_aset for 10
check testWithoutSense for 10

正在执行"Run testWithParameters for 10“Solver=sat4j Bitwidth=0 MaxSeq=0 SkolemDepth=1 Symmetry=20 2910 vars。240个主要变量。6294条。14ms。找不到实例。谓词可能不一致。3ms。

正在执行"Run testWithoutParameters for 10“Solver=sat4j Bitwidth=0 MaxSeq=0 SkolemDepth=1 Symmetry=20 2602 vars。220个主要变量。5499个条款。14ms。。找到了。谓词是一致的。21ms。

执行"Check test_aset for 10“Solver=sat4j Bitwidth=0 MaxSeq=0 SkolemDepth=1 Symmetry=20 2834 vars。230个主要变量。6162条款。14ms。找不到反例。断言可能是有效的。3ms。

执行"Check testWithoutSense for 10“Solver=sat4j Bitwidth=0 MaxSeq=0 SkolemDepth=1 Symmetry=20 2844 vars。230个主要变量。6191条。13ms。找不到反例。断言可能是有效的。7ms。

执行了4个命令。结果是：#1:找不到实例。testWithParameters可能不一致。#2：.testWithoutParameters是一致的。#3:没有找到反例。test_aset可能是有效的。#4:没有找到反例。testWithoutSense可能是有效的。

Answer 1

看看testWithoutParameters的解决方案:集合A总是空的。对于空集，普遍的量化公式总是正确的，所以矛盾并不重要。

另一方面，testWithParameters包含一个隐含的事实，即在A中至少有一个元素:参数a。但是不可能有符合矛盾事实的a，所以这个谓词没有解决方案。

编辑:由于相同的潜在原因，没有找到testWithoutSense的反例。由于矛盾的事实Rule_1和Rule_2，您的模型总是被约束为在A中不包含任何元素。如果A为空，则断言testWithoutSense几乎为真。