问题标签 [decidable]

我有这两种语言

我相信这两个是不可判定的，但我不确定它们是图灵可识别的还是共同图灵可识别的。

我必须证明语言 L = {< M >: |L(M)| <= 2016} 不是半可判定的。现在我想这样做：

取一个随机字母 E。现在 E 中有无限个单词。我们只能得出 |L(M)| <= 2016 通过将 E* 中的每个单词作为输入传递给 M。但是由于单词的数量是无限的，这意味着我们必须将输入传递给 M 无数次。但这意味着执行这些检查的图灵机最终会陷入无限循环，因此永远不会返回接受或拒绝它的输入。因此语言 L 不是半可判定的。

但我认为这可能不够正式？主要是因为我只是假设检查这种语言的图灵机会让 M 在 E* 中的每个单词上运行。这个假设是否有效，还是我应该更正式？

Say I have the Universal Turing Machine encoding of a specific Turing machine T. Also say I have the encoding of a specific input s. Is the question of whether T halts on s decidable? Can simulating running T on s be used to reach an answer?

考虑语言 $E_{tm}={ \langle M \rangle: M\text{是一个不接受任何东西的图灵机}$

我什至不知道如何开始。我的想法是从一些 NP - Complete 问题中减少多时间。E_tm

我不明白的是，知道 E_tm 是不可判定的，但 NP-Hard 类是可判定的。

因此，我的理解是，递归可判定语言是我们可以构建图灵机的语言，这样给定来自该语言的输入 w，图灵机将始终要么接受并停止，要么拒绝并停止。我感到困惑的是可以发展到无穷大的语言。例如，假设我们有一种语言 L = {0^p | p 是素数}。所以我们可以编写一个算法来判断一个数在线性空间中是否是素数。所以我的理解是，既然这个算法告诉我们数字是素数还是不是素数，那么 L 必须是递归可判定的，对吗？但是由于 p 不受任何固定数的约束，它可以到无穷大对吗？那么假设我的算法在技术上可以永远运行，而不接受或拒绝输入，这是否正确？

一阶逻辑的有效命题 (EPR) 片段通常被定义为形式为 的一组前置量化公式∃X.∀Y.Φ(X,Y)，其中X和Y是（可能为空的）变量序列。量化的顺序，即∃*∀*EPR 的可判定性是否重要？如果量化顺序被切换，我们会失去可判定性吗？

特别是，我对在可判定逻辑中捕获 set-monadic 绑定操作的语义感兴趣。给定一组S1类型的元素T1（即，S1具有类型T1 Set）和一个f类型的函数T1 -> T2 Set，set-monad 的绑定操作通过对 的每个元素应用并合并结果集来构造一个新S2的类型集。可以在以下 SMT-LIB 代码/公式中捕获此行为：T2 SetfS1

观察到第二个断言语句有量化的形式∀*∃*，它不符合标准的 EPR 定义。然而，在 Z3 上使用此类公式时，我从未遇到过超时问题，我想知道我上面的公式是否确实在某个可判定的片段中（同时承认实践中的可解性并不意味着理论上的可判定性）。欢迎任何意见。

我一直在四处寻找为什么 OWL Full 是不可判定的，但我还没有找到一个易于理解的例子来让我理解它。

我找到了解释这是由于“蕴涵封闭”的陈述，这也与 OWL Full 可以同时具有属性和个人的类这一事实相关。

但我不明白这些陈述之间的关系。

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

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

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

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

1) 接受语言 L = {ε} 的图灵机 M 是否不接受任何条目？

一方面，我认为它可能是错误的，因为空词可能是一个条目，但另一方面，我认为这可能是一个无法确定的问题。

2）是否每台可判定语言的图灵机在任何输入时都会停止？

同样的想法，直觉上我会说是的，由于可判定的定义，但我不知道，有什么困扰我。

3）回文的语言是否可以确定，无论 aphabet 是什么？

对于这一点，我几乎毫不怀疑它是错误的，因为有了赖斯定理，我们可以证明，这个问题是不可判定的。

如何证明/反驳语言 {⟨A⟩∣A 是 NFA 并且 L(A)={0,1}∗} 是/不可判定的？

起初我假设因为它涉及 NFA，所以它是可判定的，但由于没有输入字符串来模拟，这会改变事情吗？如果是这样，怎么做？我想不出能决定这一点的图灵机。由于 {0, 1}* 在理论上是无限的，这是否意味着图灵机可能永远不会停止，因此语言是不可判定的？如果是这样，我该如何证明这一点？