问题标签 [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.

0 投票
0 回答
96 浏览

first-order-logic - 一阶逻辑解析算法。提出否定请求

我尝试用否定的请求询问知识库。所以在解决之前,补码(这里是positif)被添加到算法使用的子句集中。

有了这些事实:

和论文公理:

子句变成 CNF

我可以要求

配偶(莎拉,安德鲁)或配偶(苏菲,爱德华)

这个请求 ¬Spouse(Sarah,Edward) : Sarah 不是 Edward 的配偶,不工作。

当然,我可以问配偶(莎拉,爱德华)是否是莎拉与爱德华的配偶,没有答案,认为这是错误的。

这种请求有什么问题,因为我不知道我的实现是否存在错误,或者是否不可能这样做(假设是......)。

谢谢你的帮助 !

0 投票
1 回答
142 浏览

logic-programming - 答案集编程中的混合量化

我希望能够在 ASP/cligo 中制定以下 FOL 语句:

两者的域XY给出dom/1。的域A由 给出domA/1。的域V1..n

对我来说,问题是混合量化。现在,当然,我可以扩展∀ V并得到如下内容:

但是,当我n直到运行时才知道(我将它作为参数传递给 cligo)时,这并不能很好地工作。

有没有办法用 cligo 方便又干净地做到这一点?还是应该改用 Python/Lua 脚本功能?如果是这样,怎么做?

0 投票
2 回答
445 浏览

z3 - SMT 到底是针对什么量词完成的?

我一直在研究各种 SMT 求解器,主要是 Z3、CVC4 和 VeriT。他们对使用量词解决 SMT 问题的能力都有模糊的描述。他们的文档主要基于示例 (Z3),或由学术论文组成,描述了可能实际实施或未实施的可能变化。

我知道一阶逻辑有可判定的片段,例如:

  • 有界量词
  • 一阶一阶逻辑

我想知道的是,哪些(如果有的话)FOL 类是保证完成的各种 SMT 求解器?我如何知道我正在查看的问题是否存在于它们完成的片段中?

0 投票
0 回答
108 浏览

proof - 哪些一阶定理证明者可以保证在单子输入上停止?

一阶一阶逻辑,其中所有谓词都只有一个参数,是一阶逻辑的已知可判定片段。测试一个公式在这个逻辑中是否可满足是可判定的,并且存在基于分辨率的方法来判定这一点。

我处于需要测试一些一阶一阶逻辑语句的可满足性的情况。我意识到我将达到复杂性的理论极限,但我希望我能在常见情况下获得合理的性能。

目前,存在大量的定理证明器,它们为解决一阶逻辑问题提供了快速的方法。这些包括VampireSPASSE,以及Z3CVC4的量词扩展。但是,由于不确定性,它们不能保证停止。

我的问题

在现有的定理证明者中,当给定一元公式作为输入时,是否有任何人可以保证停止?或者有没有办法使用它们(在某种程度上)有效地测试一元公式的可满足性?

0 投票
0 回答
296 浏览

logic - Skolem函数的逻辑统一

我到处寻找我能找到的关于这个主题的任何信息,但我找不到任何东西。甚至我的教科书也完全跳过了它。

关于统一 Skolem 功能甚至一般功能的规则是什么?

任何人都可以有所了解吗?

0 投票
1 回答
107 浏览

ontology - 使用描述逻辑的本体

我想知道我们如何为大学的员工使用描述逻辑语法(A-box,T-box)制作本体?我们可以在它们之间建立哪些类、对象、关系、父母、兄弟姐妹、约束和相互关系?

我制作了下面的类图,但不确定是否可以添加其他任何东西。

在此处输入图像描述

0 投票
2 回答
302 浏览

prolog - 通过通用规则在 Prolog 中创建含义,其中 A 暗示 B,B 暗示 A

无火无烟,无烟无火。

用 Prolog 程序识别上述语句的结论和条件。在答案中,结论必须是,如果有火,就有烟,如果有烟,就一定有火。

我该怎么做呢?

请解释答案。

0 投票
1 回答
50 浏览

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”吗?

我想我可以以某种方式看到正确翻译的逻辑,但其中的含义让我不确定……

0 投票
1 回答
671 浏览

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有何不同感到困惑......

0 投票
1 回答
94 浏览

prolog - Prolog 查询可满足但返回 false

我在下面有一个我编写的 prolog 程序的简单示例,其中包含一个可满足的查询,该查询始终返回 false 进行搜索。

当我问两个常量是否是兄弟时,这很好,但是如果我尝试找到一个常量 prolog 的兄弟,则返回 false。

我究竟做错了什么?