语义推理器的健全性是什么意思？答案

【问题标题】：What does soundness of a semantic reasoner mean?语义推理器的健全性是什么意思？
【发布时间】：2012-12-12 06:04:00
【问题描述】：

许多关于语义推理器的文章，将健全性称为推理器或推理算法的特征。然而，根据维基百科 (http://en.wikipedia.org/wiki/Soundness) 的健全性定义，我了解健全性是我的模型的一个属性，并且独立于我应用于它的推理算法。例如型号：

All organisms with wings can fly. 
Penguins have wings.

导致以下有效（可证明？）但不合理的结果：

Penguins can fly.

因此，当我将此模型提供给一个基于 Tableaux 的算法或 KAON2 推理器时，它们都被认为是可靠的，它们仍然会给我这个不可靠的结果。那么你能向我描述一下究竟什么是健全性吗？如果它是模型或建模语言或推理方法的特征，还是仅仅是推理结果？

【问题讨论】：

这不是声音，因为它是写出来的。如果你大声读出来，它会是健全的。
所有有翅膀的生物都会飞吗？对我来说这听起来不像..
是的，“健全性”用于描述推理算法。模型是从句子到真值的映射。 “所有有翅膀的生物都会飞。企鹅有翅膀。”对我来说看起来不像模特。
@nawfal 是的，这也是我的观点。这里的模型不健全。所以健全性应该是模型的特征，而不是建模语言或推理算法。那么为什么说 Tableaux 算法或 KAON2 推理器是健全的呢？

【解决方案1】：

它基本上意味着正确。声音意味着推理器将只返回正确的结果，即在知识库中明确显示或从其内容中包含的结果。不健全意味着推理器返回的结果在您的知识库中既不明确，也不包含任何公理，即不正确的结果。

完成意味着它返回所有答案。您可以在不完整的情况下保持健全，即返回所有正确答案的子集。这在某些用例中可能是可取的。

你也可以是完整的，但不健全；你返回所有正确的答案，以及一些不正确的答案。

在你的例子中，结果对你来说只是不合理的，因为你有知识库没有的信息，即企鹅不能飞。从推理者的角度来看，这是一个合理的结果。它不能证实它所提供的事实的真实性，它只是用它们来暗示新的事实。

【讨论】：

谢谢。我认为这基本上回答了我的问题。推理器的健全性意味着它不会返回不正确的结果，即知识库中没有明确显示或可以从其公理中推导出的结果。所以稳健性可以是模型、推理结果和推理者的特征。这取决于您从哪个角度看待它。如果我错了，请纠正我。

【解决方案2】：

论证有效，但前提之一不正确。所以这个论点是不成立的。

我不认为推理者可以决定你的前提是否正确——如果可以，那将是相当革命性的 :)

【讨论】：

这是什么意思：“......大多数基础推理方法已被证明是健全和完整的。tableaux 和 hypertableaux 演算是健全和完整的......”。仅作为从此处获取的示例http://www.semantic-web-journal.net/sites/default/files/swj120_2.pdf
@zardosht - 我想这意味着算法本身只包含合理的推理。那就是它们“可证明是正确的”。