问题标签 [first-order-logic]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
artificial-intelligence - 使用一阶逻辑构建解析证明
对于即将到来的考试,我有以下复习题,希望得到一些帮助。我必须使用分辨率来回答“玛丽只用青苹果做馅饼”这个问题。我目前的知识库和语言是以下句子:
最近更新:
我会尽量说得更具体一些。我想证明的是“玛丽只用青苹果做馅饼”。写这个逻辑我得到:
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))
这是正确的吗!?还是我弄错了?
logic - 如何自动证明两个一阶公式是等价的?
自动证明两个一阶公式 F 和 G 等价的最佳方法是什么?
与“完整”一阶公式相比,这些公式有一些限制:
- 无量词
- 无功能
- 隐含的普遍量化的
我可以将这些公式转换为子句范式,并且我有统一文字的例程。但是,我不确定如何继续以及是否可以确定此问题。
prolog - Prolog - 什么样的句子不能表达
我想知道你不能用 Prolog 表达什么样的句子?我一直在研究逻辑编程,并了解到与 Prolog 所基于的明确子句逻辑(Horn 子句)相比,一阶逻辑更具表现力。这对我来说是一个很难理解的话题。
因此,例如,可以表达以下句子:
如果有,还有其他不能表达的句子吗?如果不是,为什么?
prolog - 证明的一阶逻辑语句。操纵量词
好的,我有给定的关系:如果 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)),因为这让工作更容易???
z3 - Z3中的FOL定义理论
我想将一阶理论放入微软开发的 SMT 求解器 Z3 中。该理论包含两个对象obj1和obj2,一个函数move接受一个对象并返回一个动作,以及一个单一的谓词发生,它将一个动作作为参数。该理论包含公式发生(move(obj1)),我想确保这是发生谓词为真的唯一方式。我通过给出发生的定义来做到这一点:
这意味着从理论上可以推断出发生(move(obj1)) ,但发生(move(obj2))不能。为了证明这一点,我把它翻译成 Z3 如下:
问题是这给出了以下输出:
我不明白,因为发生的定义为谓词为真提供了所有必要和充分条件,所以我认为发生(move(obj2))在任何模型中都不能为真。我究竟做错了什么?
更新
感谢 de Moura,我已经能够找到解决问题的方法。我需要做的是为动作提供唯一的名称公理,在我的例子中就是move
函数。我需要声明,当它有两个不同的参数时,它move
永远不会返回相同的排序元素。Action
这可以通过多种方式完成,但我发现这是最简洁的版本:
java - 是否有任何基于“描述逻辑”或基于 FOL 的推理引擎 java 库可用?
我最近在一门 AI 课程中学习了 KRL(知识表示语言),发现描述逻辑是语义 Web 的正式知识表示语言家族,这很有趣。此外,在描述逻辑中,表示知识比在一阶谓词逻辑中更简单易懂。
有谁知道可用于处理描述逻辑或一阶逻辑的 Java 库?
string-matching - 如何通过字符串匹配将一阶逻辑语句翻译成 Protègè 中的限制?
我正在尝试构建一个本体来推断有关域分类和术语的一些信息,但我遇到了一些概念上的困难。
让我解释一下这个问题。在 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。
提前致谢。
z3 - 处理空模型的量化公式的正确方法是什么?
我在玩未解释的排序和函数,不能完全理解量化公式如何与空模型交互。这里(也在这里http://rise4fun.com/Z3Py/6ets)是一些让我有些困惑的简单例子:
[∀v : False]
是不饱和的,而“直观地”它适用于空模型。- 检查
[∃v : v = v]
会产生一个空模型,而该模型没有令人满意的分配。 - 一些看似等同于 的公式以
[∃v : v = v]
某种方式阻止 z3 生成空模型。[∃v, v1 : v = v1]
就是这样一个例子。例如,如果我们将这样的公式添加到求解器,然后尝试创建类似于 allsat 程序的东西(添加越来越多的约束以排除越来越多的模型),我们会在得到一个空模型之前遇到 unsat。
那么,您能否请我参考任何描述 z3 如何处理量词和空模型的文档/论文?另外,如果我选择只关注非空模型,那么询问 z3 的正确方法是什么?诸如此类的事情[∃v, v1 : v = v1]
似乎可以解决问题,但是有更好的方法吗?
prolog - 将爱因斯坦谜题表示为一阶逻辑中的一组封闭公式
我得到了这种形式的经典爱因斯坦/斑马谜题:
让我们假设在同一条路上有五个不同颜色的房子相邻。每个房子里住着一个不同国籍的人。每个男人都有他最喜欢的饮料,他最喜欢的香烟品牌,并养着一种特定的宠物。
任务是将这些陈述表达为一阶逻辑中的一组封闭公式,每个陈述一个,假设拼图中的五个人由英国人、瑞典人、丹麦人、挪威人、德国人和保持(X,Y) 表示人 X 养宠物 Y。这些稍后将转换为序言。
我的问题是我是否要以正确的方式转换语句。现在,我有类似的东西:
这是正确的,还是应该更像我尝试的另一种方式:
我也尝试过类似的事情:
我认为第一个是最正确的,但我不确定。我也不确定如何在一阶逻辑中表示中心或邻居之类的东西。这些是否接近正确?
编辑:我想出了一个我认为可能是正确的解决方案。我注意到它说的是 CLOSED 公式,所以我这样做了:
这是正确的方法吗?任何帮助,将不胜感激。
python - 在 Z3py 中优化量词和 for
所以我正在寻找一种方法来简化 Z3py 中的以下代码,因为每次我想检查这个断言(在我自己的计算机或http://rise4fun.com/z3py/上)它只是超时所以我认为可能是最快的方法。
如您所见,这确实是一个很大的公式,但我没有找到使其更小的方法...目的是确保任务的每个部分都井井有条,即使它们由不同的处理器处理(p1或 p2)
如果您能帮助我,请提前非常感谢(即使只是可以帮助我更改公式的提示也会很棒)
编辑:我只是单独测试了该约束并且它有效,它给出了奇怪的结果但仍然有效,但我仍然需要它与其他约束一起工作,所以如果你能帮助我优化它,欢迎你。