问题标签 [first-order-logic]

对于即将到来的考试，我有以下复习题，希望得到一些帮助。我必须使用分辨率来回答“玛丽只用青苹果做馅饼”这个问题。我目前的知识库和语言是以下句子：

最近更新：

我会尽量说得更具体一些。我想证明的是“玛丽只用青苹果做馅饼”。写这个逻辑我得到：

Mary 只用青苹果做馅饼： π,a Pie(π) A Make(M, π, a) => Green(a)

以及将其翻译成 CNF 形式的步骤（http://en.wikipedia.org/wiki/Conjunctive_normal_form）：

以 CNF 形式否定此陈述（我们将在决议中使用它来证明）：

饼图(π) A Make(M, π, a) A ⌐Green(a)

现在当对一阶逻辑使用分辨率时:(http://en.wikipedia.org/wiki/Resolution_(logic))

这是正确的吗！？还是我弄错了？

自动证明两个一阶公式 F 和 G 等价的最佳方法是什么？

与“完整”一阶公式相比，这些公式有一些限制：

1. 无量词
2. 无功能
3. 隐含的普遍量化的

我可以将这些公式转换为子句范式，并且我有统一文字的例程。但是，我不确定如何继续以及是否可以确定此问题。

我想知道你不能用 Prolog 表达什么样的句子？我一直在研究逻辑编程，并了解到与 Prolog 所基于的明确子句逻辑（Horn 子句）相比，一阶逻辑更具表现力。这对我来说是一个很难理解的话题。

因此，例如，可以表达以下句子：

如果有，还有其他不能表达的句子吗？如果不是，为什么？

好的，我有给定的关系：如果 F(x) 不正确，则没有任何情况满足 G(x) 和 H(y,x)。((∀x ¬F(x)) ⇒¬(∀y G(y) ˄ H(y,x)))

现在，我可以将其转换为： (∀y G(y) ˄ H(y,x))) ⇒ ((∀x F(x)) ????

如果不是，则左侧基本上必须暗示：如果 F(x) 不正确.... 没有提及 For All 或 Existential 量词。我可以把否定放在量词之外，即把它写成 (¬(∀x F(x))，因为这让工作更容易？？？

我想将一阶理论放入微软开发的 SMT 求解器 Z3 中。该理论包含两个对象obj1和obj2，一个函数move接受一个对象并返回一个动作，以及一个单一的谓词发生，它将一个动作作为参数。该理论包含公式发生(move(obj1))，我想确保这是发生谓词为真的唯一方式。我通过给出发生的定义来做到这一点：

这意味着从理论上可以推断出发生(move(obj1)) ，但发生(move(obj2))不能。为了证明这一点，我把它翻译成 Z3 如下：

问题是这给出了以下输出：

我不明白，因为发生的定义为谓词为真提供了所有必要和充分条件，所以我认为发生（move（obj2））在任何模型中都不能为真。我究竟做错了什么？

更新 感谢 de Moura，我已经能够找到解决问题的方法。我需要做的是为动作提供唯一的名称公理，在我的例子中就是move函数。我需要声明，当它有两个不同的参数时，它move永远不会返回相同的排序元素。Action这可以通过多种方式完成，但我发现这是最简洁的版本：

我最近在一门 AI 课程中学习了 KRL（知识表​​示语言），发现描述逻辑是语义 Web 的正式知识表示语言家族，这很有趣。此外，在描述逻辑中，表示知识比在一阶谓词逻辑中更简单易懂。

有谁知道可用于处理描述逻辑或一阶逻辑的 Java 库？

我正在尝试构建一个本体来推断有关域分类和术语的一些信息，但我遇到了一些概念上的困难。

让我解释一下这个问题。在 Protègè 4.1 中，我创建了 Thing 的 6 个子类：Concept、conceptTitle、ConceptSynonym（用于分类）和 Term、TermTitle、TermSynonym（用于术语）。我还创建了 hasConceptTitle、hasConceptSynonym、hasTermTitle 和 hasTermSynonym 对象关系（带有一些约束）来表示每个概念都有一个（并且只有一个）标题，并且可能有一些同义词，并且每个术语都有一个（并且只有一个）标题和一些同义词。Concept 和 Term 都有另一种关系 isA，为分类赋予 DAG/树结构，而术语具有格结构（换句话说，一个术语可能是多个术语的子类）。

问题来了：我想创建一个概念的子类，比如说“MappedConcept”），它应该是映射概念的集合，即标题等于术语标题的概念集，或者它有同义词等于术语的标题或具有等于术语的同义词的同义词。在一阶逻辑中，这个集合可以表示为：

我怎样才能得到这个？为“ConceptTitle”、“ConceptSynonym”、“TermTitle”和“TermSynonym”定义数据属性？以及如何描述字符串匹配？也许这 4 个类应该只是 Concept 和 Term 类的数据属性？我多次阅读 Matthew Horridge 的实用指南，但我无法将脑海中的实用想法转化为 Protègè 的 ongology。

提前致谢。

我在玩未解释的排序和函数，不能完全理解量化公式如何与空模型交互。这里（也在这里http://rise4fun.com/Z3Py/6ets）是一些让我有些困惑的简单例子：

1. [∀v : False]是不饱和的，而“直观地”它适用于空模型。
2. 检查[∃v : v = v]会产生一个空模型，而该模型没有令人满意的分配。
3. 一些看似等同于 的公式以[∃v : v = v]某种方式阻止 z3 生成空模型。[∃v, v1 : v = v1]就是这样一个例子。例如，如果我们将这样的公式添加到求解器，然后尝试创建类似于 allsat 程序的东西（添加越来越多的约束以排除越来越多的模型），我们会在得到一个空模型之前遇到 unsat。

那么，您能否请我参考任何描述 z3 如何处理量词和空模型的文档/论文？另外，如果我选择只关注非空模型，那么询问 z3 的正确方法是什么？诸如此类的事情[∃v, v1 : v = v1]似乎可以解决问题，但是有更好的方法吗？

我得到了这种形式的经典爱因斯坦/斑马谜题：

让我们假设在同一条路上有五个不同颜色的房子相邻。每个房子里住着一个不同国籍的人。每个男人都有他最喜欢的饮料，他最喜欢的香烟品牌，并养着一种特定的宠物。

任务是将这些陈述表达为一阶逻辑中的一组封闭公式，每个陈述一个，假设拼图中的五个人由英国人、瑞典人、丹麦人、挪威人、德国人和保持(X,Y) 表示人 X 养宠物 Y。这些稍后将转换为序言。

我的问题是我是否要以正确的方式转换语句。现在，我有类似的东西：

这是正确的，还是应该更像我尝试的另一种方式：

我也尝试过类似的事情：

我认为第一个是最正确的，但我不确定。我也不确定如何在一阶逻辑中表示中心或邻居之类的东西。这些是否接近正确？

编辑：我想出了一个我认为可能是正确的解决方案。我注意到它说的是 CLOSED 公式，所以我这样做了：

这是正确的方法吗？任何帮助，将不胜感激。

所以我正在寻找一种方法来简化 Z3py 中的以下代码，因为每次我想检查这个断言（在我自己的计算机或http://rise4fun.com/z3py/上）它只是超时所以我认为可能是最快的方法。

如您所见，这确实是一个很大的公式，但我没有找到使其更小的方法...目的是确保任务的每个部分都井井有条，即使它们由不同的处理器处理（p1或 p2)

如果您能帮助我，请提前非常感谢（即使只是可以帮助我更改公式的提示也会很棒）

编辑：我只是单独测试了该约束并且它有效，它给出了奇怪的结果但仍然有效，但我仍然需要它与其他约束一起工作，所以如果你能帮助我优化它，欢迎你。