问题标签 [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.
first-order-logic - 一阶逻辑解析算法。提出否定请求
我尝试用否定的请求询问知识库。所以在解决之前,补码(这里是positif)被添加到算法使用的子句集中。
有了这些事实:
和论文公理:
子句变成 CNF
我可以要求
配偶(莎拉,安德鲁)或配偶(苏菲,爱德华)
这个请求 ¬Spouse(Sarah,Edward) : Sarah 不是 Edward 的配偶,不工作。
当然,我可以问配偶(莎拉,爱德华)是否是莎拉与爱德华的配偶,没有答案,认为这是错误的。
这种请求有什么问题,因为我不知道我的实现是否存在错误,或者是否不可能这样做(假设是......)。
谢谢你的帮助 !
logic-programming - 答案集编程中的混合量化
我希望能够在 ASP/cligo 中制定以下 FOL 语句:
两者的域X
由Y
给出dom/1
。的域A
由 给出domA/1
。的域V
是1..n
。
对我来说,问题是混合量化。现在,当然,我可以扩展∀ V
并得到如下内容:
但是,当我n
直到运行时才知道(我将它作为参数传递给 cligo)时,这并不能很好地工作。
有没有办法用 cligo 方便又干净地做到这一点?还是应该改用 Python/Lua 脚本功能?如果是这样,怎么做?
z3 - SMT 到底是针对什么量词完成的?
我一直在研究各种 SMT 求解器,主要是 Z3、CVC4 和 VeriT。他们对使用量词解决 SMT 问题的能力都有模糊的描述。他们的文档主要基于示例 (Z3),或由学术论文组成,描述了可能实际实施或未实施的可能变化。
我知道一阶逻辑有可判定的片段,例如:
- 有界量词
- 一阶一阶逻辑
我想知道的是,哪些(如果有的话)FOL 类是保证完成的各种 SMT 求解器?我如何知道我正在查看的问题是否存在于它们完成的片段中?
proof - 哪些一阶定理证明者可以保证在单子输入上停止?
一阶一阶逻辑,其中所有谓词都只有一个参数,是一阶逻辑的已知可判定片段。测试一个公式在这个逻辑中是否可满足是可判定的,并且存在基于分辨率的方法来判定这一点。
我处于需要测试一些一阶一阶逻辑语句的可满足性的情况。我意识到我将达到复杂性的理论极限,但我希望我能在常见情况下获得合理的性能。
目前,存在大量的定理证明器,它们为解决一阶逻辑问题提供了快速的方法。这些包括Vampire、SPASS、E,以及Z3和CVC4的量词扩展。但是,由于不确定性,它们不能保证停止。
我的问题
在现有的定理证明者中,当给定一元公式作为输入时,是否有任何人可以保证停止?或者有没有办法使用它们(在某种程度上)有效地测试一元公式的可满足性?
logic - Skolem函数的逻辑统一
我到处寻找我能找到的关于这个主题的任何信息,但我找不到任何东西。甚至我的教科书也完全跳过了它。
关于统一 Skolem 功能甚至一般功能的规则是什么?
任何人都可以有所了解吗?
prolog - 通过通用规则在 Prolog 中创建含义,其中 A 暗示 B,B 暗示 A
无火无烟,无烟无火。
用 Prolog 程序识别上述语句的结论和条件。在答案中,结论必须是,如果有火,就有烟,如果有烟,就一定有火。
我该怎么做呢?
请解释答案。
logic - 用英语代表 FOL
我有以下 FOL 公式:∀e(S(e)) → ∃d(P(d))
还有词汇:
variables: e:'exam', d:'day'
functions: S:'successful', P:'party'
我最初将该公式翻译成:
For every successful exam, there will be a day of party
虽然显然正确的翻译是这样的:
You party at least one day after all exams were successful.
为什么正确的说我们只有在所有考试都成功后才聚会?
是否∀e(S(e))
意味着:“对于所有考试,他们都会成功”?意思是: “∃d(P(d))
至少有一天我们聚会”?
暗示不是转化为“if a then b”吗?
我想我可以以某种方式看到正确翻译的逻辑,但其中的含义让我不确定……
first-order-logic - 将句子翻译成 FOL 表达式,对常量和量词感到困惑
将下列语句翻译成 FOL 句子
1)亚历克斯喜欢约翰
Likes(alex, john) - 我知道这是正确的
2)每个人要么是男人要么是女人
AxAy(男人(x)v女人(y))
编辑:这更好吗??: Az(Person(z) -> man(x) v woman(y)) 或编辑:这更好吗??: Ax(Person(x) -> man(x) v woman( X))
3)没有人既是男人又是女人
例如((男人(x)^ ¬女人(x))v(¬男人(x)^女人(x)))
4)Alex喜欢一个喜欢女人的男人
AxEy(喜欢(男人(x),女人(y))->喜欢(亚历克斯,男人(x)))
谢谢
编辑:对于第 3 号,我在网上找到了这个“p 和 q 的排他性析取断言 p 为真或 q 为真,但不是两者兼而有之。那么,表达排他性析取的自然但冗长的方式是(p | q) & ~(p & q)。”
如果这适用,那么我假设正确答案是 Ax( (man(x) v woman(x)) ^ ¬(man(x) & woman(x)) )
但是现在我对2和3有何不同感到困惑......
prolog - Prolog 查询可满足但返回 false
我在下面有一个我编写的 prolog 程序的简单示例,其中包含一个可满足的查询,该查询始终返回 false 进行搜索。
当我问两个常量是否是兄弟时,这很好,但是如果我尝试找到一个常量 prolog 的兄弟,则返回 false。
我究竟做错了什么?