nn可在www.sciencedirect.com在线获取理论计算机科学电子笔记312（2015）143-160www.elsevier.com/locate/entcs从常识推理中提取证据项的实用纳塔利娅·诺瓦克纽约市立大学布朗克斯社区学院数学与计算机科学系Bronx NY 10453，USANatalia. bcc.cuny.edu摘要知识、信念和证据是出现在广泛领域的基本概念。 来在过去的十年里，具有正当性的认知推理已经扩大了认知逻辑的应用范围，因为智能体不仅能够推理知识的认知状态，代理人的信念，但也跟踪他们的正义和排序那些与给定的事实有关并且对于认知结论来说足够了。本文将S_4到LP的实现算法推广到S_4J到S_4nLP的实现算法. 它将无切割衍生物-在S4 J中的推理转化为相应的正义化逻辑S4 n LP中的推导，其中知识的见证人，正义化项，对于所有正义化的共同知识的实例都被恢复。该算法在MetaPRL框架中实现，并在几个著名的认知难题上进行了测试，如MuddyChildren，Surprise Examination Parket等。保留字：证明逻辑，逻辑难题，证据术语，元介绍认知推理的研究，关于知识和信念的推理，是计算机科学和人工智能的核心领域之一。传统的形式认识论系统是建立在模态逻辑的基础上的，并且在过去的几十年里一直是激烈的研究活动的子系统[10;15]。有几个计算机辅助系统的模态和认知推理（不完整的列表，见[17]）。这一领域的一个基础性成果丰富了模态认知逻辑，使其具有内在化的正义化概念，并成为认知逻辑语言的一部分。这一发展大大拓宽了表位逻辑的应用范围。我们现在不仅有能力推理主体的知识和信念的认知状态，而且有能力跟踪它们的证明，并对那些与给定事实相关并足以得出认知结论的证明进行排序。证据的概念已经成为严格研究的主题http://dx.doi.org/10.1016/j.entcs.2015.04.0091571-0661/© 2015作者。出版社：Elsevier B.V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。144N. Novak/Electronic Notes in Theoretical Computer Science 312（2015）143nArtemov它恢复的证据条款，每次出现的认识模态在一个给定的-orem。我们开始与MetaPRL计算机辅助推理系统的框架内的实施改进的阿特莫夫1S4J翻译S4nLP证明1.1S4n LP逻辑概述S4nLP[4]是一个基于证据的知识的多智能体逻辑，具有n个智能体K1，K2，K3，.，Kn，充当S4模态[10]，以及t：A形式的证据断言，其中t是证据项，A是公式，如LP[3]中所示。 证据项t由常数a、b、c、.. . . 以及变量x，y，z，. . . 借助二进制操作符“·”（应用程序）、“+”（联合）和一元（视察）。S4nLP的公式由以下语法定义：⊥ |S|A→B|A组B组|A组B组|欧阿|K i A|t：A，其中t是证据，S是句子变量。证据操作具有最高优先级，所有其他连接词都具有标准的优先顺序。S4nLP的希尔伯特式公理和规则包含经典的命题逻辑公理和前件推理规则，知识原则B1岛Ki（A→B）→（KiA→KiB）B2i.Ki A→AB3岛KiA→KiKiA（正内省） 知识概括（KnowledgeGeneralization）对于每个单独的知识算子Ki。证据原则E1. s：（A→B）→（t：A→（s·t）：B）（应用）E2. t：A→！t：（t：A）（检验）E3. s：A→（s+t）：A，t：A→（s+t）：A（并集）E4. t：A→A（反射率）R3. A，其中A是S4nLP公理，c是证明常数（公理）。联系证据和知识的原则C1. t：A → K i A（证据的可证明性）。所有公理都是S4nLP语言中的模式。规则适用于所有部门。 该系统是封闭的证据项下的替代证据变量和命题变量的公式。 演绎定理Γ，A<$B<$其中，Γ是S4nLP公式的有限集.N. Novak/Electronic Notes in Theoretical Computer Science 312（2015）143145nnnnnnnnn以下两个引理将用于本文后面介绍的实现算法的证明：引理1.1（提升引理）[3; 4]如果A1，...，A n，y1：B1，...，y m：B m<$F，则对于某个证据项t = t（x1，...，x n，y1，.，y m），x1：A1，.，xn：An，y1：B1，.，y m：B mt（x1，.，x n，y1，.，y m）：F.引理1.2 [5]对于任何证明变量xi和任何公式Bi，存在证明项s = s（x1，...，x n），使得LPx1：B1. Bn →s（x1，...，x n）：（x1：B1. Bn）。1.2关于S4J系统S4J[4; 5]是具有n +1个 模态K1，...， K n，J.JA读作对应于J的虚拟第n+ 1个不是逻辑上无所不知的S4-只有在提供可检验的证据时才接受事实的代理人。 此代理受到所有其他代理的信任，并且能够内化和检查系统中实际证明的任何事实S4J证据可证性原则的遗忘版本是JA→Ki A，对于所有i = 1，...， n.下面我们介绍S4J的Gentzen式公式[18]，称为S4JG。A是表示为Γ Δ的S4J公式的一对有限集合公理Gentzen式S4J的序列是S，Γ Δ，S和，Γ Δ，其中S是命题变量S4J严格弱于系统S4C[1]，其中公共知识C被定义为n n使用传统的fixpoint常识[10]。然而，S4J似乎是足够的，所有实际应用。与此同时，S4J公理学允许标准方法的证明理论，并允许绘制平行的逻辑明确的证据LP.146N. Novak/Electronic Notes in Theoretical Computer Science 312（2015）143nnnS4J的Gentzen风格规则：Γ Δ，A（）<$A，<$A，<$AA，B，Γ Δ（）Γ Δ，AΓ Δ，B（）AB，Γ ΔΓ Δ，ABA，Γ ΔB， Γ Δ（）Γ Δ，A，B一（刘伟）B，ΓΓ Δ，A B，ΓA（→）A， Γ Δ，B（→）A→B，Γ ΔΓ Δ，A→B以及n+ 1对模态规则：A，QA，Γ Δ（Q）JΓ，Q ΔA（Q）QA，Γ ΔJ Γ，Q Δ，，QA其中Q∈ {K1，.，Kn，J}和Q{A1，...，A m}={QA1，...， QA m}。1.3实现程序的主要定义和事实这项工作的目标是用显式的证明（即证明多项式）来代替可证明的知识J。换句话说，我们并不知道某件事是“正当的”，而是希望得到它实际的正当化。实现这一点的算法称为实现过程。定义1.3从S4J实现模态公式F在S4中，nLP意味着取代-证明多项式J在F中的所有出现。定义1.4一个实现r被称为正规的，如果J的所有负出现都被证明变量实现。实现定理第一个版本的实现定理S4和LP，产生希尔伯特式的推导，建立在[2]。另一个版本的实现定理，产生一个根岑式的推导，在[3]中提出。在这两个版本中，所产生的证据项在给定的定理的无割证明的长度上可以是指数的[5]中的一个改进算法将产生的证据项本文将文献[5]中的实现算法推广到S4J和S4nLP，并加以实现，并在若干聚合认知问题上测试其性能。这些测试显示了实现项的鲁棒性，其中复杂性稳定地保持在理论预测的多项式（二次）范围内。N. Novak/Electronic Notes in Theoretical Computer Science 312（2015）143147nn⇒n1.4实现算法实现程序的工作通过归纳的S4J的深度树它贯穿于S4J中公式F的根岑式证明推导和模拟构造一个实现和实现公式的希尔伯特式证明。我们还跟踪在这个希尔伯特式证明中使用的公理规则R3的证据的所有实例，即，不断的具体化。我们从公式和公式中模态J的积极和消极出现的定义开始，如改编自[2]：• J在JF中的外部出现是正的;• J在F中的一个对应出现和G→F，G<$F，G<$F，JF，和Γ<$ Δ，F具有相同的极性;• J在F和<$F中的相应出现，F→G和F，Γ<$ Δ具有相反的极性。在无割流推导中，规则尊重极性。由（J）引入的J的出现是正的：JA（J）. Jr，马可，JA所有出现在一个给定的派生树中的J-modality被划分成家庭的相关出现。副式G中的J的每次出现（即，从Γ和Δ）只与规则结论中J在G中的对应出现有关。类似地，规则的有效公式中的J的每次出现，即，在由规则变换的前提中的公式中，只与规则的主公式中J的相应出现有关，即在变换的结果中。例如，在（J）-规则中，前提中的公式A和JA是有效公式，结论中的公式JA是主公式。这一关系又被反显性和传递性所扩展。因此，所有相关的事件都自然地分成相关事件。由于根岑自由切割系统中的规则尊重极性，因此每个族都由极性相同的J如果一个族由正J组成，我们称它为正族;如果它由负J组成，我们称它为负族来自同一族的J模态对应于证明中J的相同出现，因此我们通过解释此J的相同证明多项式来实现它们。此外，由于正规性条件，来自一个负族的所有J根岑系统中公式的证明（推导），特别是S4JG节点是三元组：当前的节点、规则的名称和主公式，以及作为叶子的公理。它在J的评论：没有必要在每个节点中携带序列-它们可以是148N. Novak/Electronic Notes in Theoretical Computer Science 312（2015）143nnn从规则名称、原则公式和根处的完整序列重构虽然为了实现算法，需要每个节点中的全序列一个正的J实现算法：(by递归的派生树结构）在我们的系统S4JG中，只有三种方式引入新的J模态：• 一个公理;• 在一个公式中，一个在（BQ）规则中被“削弱”的符号• 在（JPQ）规则的主公式中的外部J让我们枚举派生树中的所有（j）规则，并将临时变量ui与第i个规则的主体J相在算法结束时，所有临时变量都将被证明多项式替换阶段1每个J的否定族和非本质族都由一个新的证明变量来实现。来自这样一个族的所有J将通过对应于该族的证明变量来实现。阶段2选择一个J的基本正族。 枚举所有出现的（CNOQ）规则，这些规则将这个族中的J作为原则引入<<：i1i2。. .和lt; ik.所有这样的J最初由临时项ui 1 + ui 2 +.实现。其中加法与左边相关联，并且是新的临时变量。我们还初始化一个作用于这些临时变量的替代σ，使其成为空替代。在实现过程结束时，该替换将为每个临时变量分配一定的证明多项式因此，本质正的J下一篇：S4J将在推导过程中出现的公式G转化为一个S4nLP公式Gr如下：在G中的每一次出现的J被可能包含临时变量的证明多项式tσ所代替，其中t是实现该J的族的项，并且σ是作用于临时变量的替换的当前状态。在实现过程中，即在处理（REQ）规则期间，附加该替换。第三阶段对于初始推导中的每一个矩阵，我们将构造• 一个对应于该α的S4n LP• 不包含临时变量的证明多项式t，以及• t的希尔伯特式推导：C递归地对BNF的导出树的结构进行了研究。库兹涅茨和勃列日涅夫的想法是使用多项式t。他们习惯在处理初始S4J的（REQ衍生，是一个重要的组成部分，来消除指数爆炸。N. Novak/Electronic Notes in Theoretical Computer Science 312（2015）143149nn12M1n1M基础：设C是一个公式。 任何一个公式，其中，{A1，. A n}，并且Δ ={B1，...，B m}，转换为公式（... （ArAr）1 2.. . ）A r→（. （B rB r）.. . ）Bagarbr.一个数组的前件和后件都是多重集，所以公式在这两种情况下都是无关紧要的，但正常的希尔伯特式运算不具有这种自由。因此，我们需要在Ar和B r上强制某种顺序，这样我们就我我使用允许高效排序的任何排序。 这种顺序应该是统一的，所有的序列。这对于Cook和Reckhow的思想[ 9 ]来说很重要，词典编纂的顺序是自然的。一个空的后件构成空的析取，并被翻译为空的析取。空的先行词构成空的连词，被翻译成T。因此F→T→Fr。S4JG的两个公理的翻译：（A）A1， . ，Ai−1，S，Ai， . ，AnB1， . ，Bj−1，S，Bj， . ，Bm被翻译为A r... Ar A r→ B r Br 布雷博，1i− 1inr 1rj− 1jm特别地，SS被翻译为S（B）A1，...，A nB1，...，BM被翻译为我的天啊A r→B r Br;→S;特别是，被翻译为→。（假设Ak和B l、A r和B r已经按K L字母是字母表的第一个符号，向左）。这种类型的每个翻译蕴涵C在S4nLP中显然是可导出的。在将提升引理应用于这个导子之后，我们得到了一个基础证明多项式s和s的一个导子：C。诱导步骤：命题规则有一个前提：是的Γj ΔJ设C和CJ分别是Γ<$ Δ和ΓJ <$ ΔJ根据归纳假设，存在一个项tC和tC：C的一个导子lC.通过命题推理，有一个C→CJ的推导。利用提升引理，我们得到一个基项tR和tR的导数lR：（C→CJ）。lC与lR连接并将结果附加以下序列... （推导1 R）n.t R：（C→ CJ）...（推导1C）m.tC：Cm+1。tR：（C→CJ）→（tC：C→tR·tC：CJ）（公理E1）150N. Novak/Electronic Notes in Theoretical Computer Science 312（2015）143⇒R rrR rr1R rri−1我Jn1M1j−1Jn我m+2。 t C：C→t R·t C：CJ（MP来自n和m+1）m+3。 tR·tC：CJ（MP from m andm+2），得到了tC′ = tR·tC和tR·tC：Cj的导子LC ′.一个有两个前提的命题规则的情况也以类似的方式处理让我们考虑对于Γ={B1，.，Bn}，并且Δ ={D1，...，D m}：A，JA，B1，...，B.N.D.1，.，D m（Q）.JA，B1，...，BnD1，. DM不失一般性，让C= B r. BrA CIBBAbaby. B→D，其中D = D r. r和x是与否定相关联的证明变量JA中的外J-模态族。那么结论的翻译是CJ= B r. BrAbaby. B→ D。由于S4nLPx：Ar→Ar（反存在性原理E4），很容易导出C→CJ。然后，利用提升引理，我们得到了一个基项t（Q_j）和t（Q_j）的一个导子l（Q_j）：（C→C_J）。其余的与一个前提的提议相同常规规则。唯一被区别对待的规则是（Q），它包括两种情况：（Ki）和（J）。让我们考虑第一个：对于Γ = {B1，...，B n}，Δ ={D1，. D m}，n ={E1，...，E o}，并且，A r}JΓ，K i Δ λ A（λK）。JΓ，Ki Δ，Ki A不失一般性，让C=x： Γr<$Ki Δr→Ar并且x =（x1，...，xn），其中xi是与J Γ中的外J -模态的负族相关联的不同证明变量。那么结论的翻译是CJ= x：Γ r<$K i Δ r<$$> r→ <$r<$K i A r.通过归纳假设，我们有一个项tC和一个导数lC，tC：（x：Γr<$Ki：Dr→Ar）j−1N. Novak/Electronic Notes in Theoretical Computer Science 312（2015）143151∧→⇒RRrn+5。.2019 - 04- 22 01：01：0201：02（Ki Ki Dr）→Ki（x：Γr<$KiΔr）（简单S4nLP推理）n+6。.2019 - 04- 22 01：01：0201：02（Ki Ki Dr）→Ki Ar（n+4和n+5的三段论LLJLJLn+10。.2019 -05 - 2201：01：02（Ki Dr）→Ki Ar（n+6和n+9的三段论n+11。.xj：Br（Ki Dr）→KiArn+12。 t n+11：（.xj：Br（Ki Dr）→KiAr）1M11MMJLJL...（推导1C）n.tC：（x：Γr<$KiΔr→Ar）n+1。tC：（x：Γr<$Ki Δr→Ar）→Ki（x：Γr<$Ki Δr→Ar）（公理C1）n+2。Ki（x：Γr<$Ki Δr→Ar）（MP from n and n+1）n+3。Ki（x：Γr<$Ki Δr→Ar）→（Ki（x：Γr<$Ki Δr）→Ki Ar）（公理B1i）n+4。Ki（x：rKiΔr）KiAr（MP from n+2 andn+3）JLn+7。xj：Br→Ki xj：Br(an easyS4nLP fact）J Jn+8。Ki Dr→Ki Ki Dr（公理B3i）n+9。.x j：B r（K i D r）→.Ki xj：Br（Ki Ki Dr）（从n+7和n+8开始的命题推理）JL（从n+10开始的命题推理）JL（从n+11提升引理）。我们得到了基项 tn+11和 tn+11 的一个导子：（C→CJ）.现在，让我们考虑一下（BJJ）规则：对于Δ ={D1，...，D m}，n ={E1，...，E o}，并且，A r}JD1，.，JD mA（ J）.J D1，.， J D m，A1，.， AR第1页，... Eo，JAJDi's中的所有J都设k是这个（KJ）规则的个数，并让它的族由u s1 +.. + uk+.乌湖通过归纳假设，我们有一个项tC和一个导数lC，t C：（x1：D r. Mr.Yu：Dr→A）。通过引理2，我们构造一项s = s（x1，...，x m）的导数l1，x1：D r. Mr.Yu：Dr→s：（x1：D我... m：D）。152N. Novak/Electronic Notes in Theoretical Computer Science 312（2015）1431LRn1L请注意，s不包含任何临时变量。现在很容易附加派生lC和l1（我们...（推导1C）n.tC：（x：Dr→Ar）...（推导l1）M.x：Dr→s：（x：Dr）m+1。t C：（x：Dr→A r）→（s：（x：Dr）→t C·s：A r）（ 公 理E1）m+2. s：（x：Dr）→t C·s：Ar（ MPfromnandm+1）m+3. x：Dr→tC·s：Ar（m和m+2的三段论... （多次使用公理E3K. x：Dr→（u s σ +. + t C·s+. u s σ）：A r.此外，该推导式易于附加，得到公式的推导式l2CJ（模置换）看起来像x：DrA → E（u sσ +. + t C·s +. u sσ）：A r(herex：Dr和A代表连词，E代表析取）。然后，我们使用提升引理来再现基项tC′和导子lC′oft C′：（x：Dr<$A → E <$（usσ +. + t C·s +. u sσ）：A）。1L当提升l2[5]时，不需要提升其初始部分lC，因为我们对第二部分使用的唯一公式是tC：（x：Dr→Ar）;这个公式很容易通过向lC添加以下两个公式来提升：tC：（x：Dr→Ar）→！tC：tC：（x：Dr→Ar），以及！tC：tC：（x：Dr→Ar），后者是所需的提升形式。这个过程产生一个接地项，因为tC接地。此外，这种修改使整个过程多项式的大小原始S4J-推导。在原算法[2]中，每处理一个（SQREQ）规则，初始推导中的大多数公式被提升的一个中的三个公式取代，这导致指数增长在规则的数量（SQUID）中。 然后，我们通过一个新的替换来附加σ：σ+{uk<$tC·s}，并在整个推导过程中应用此替换（S4nLP为已知在替换下关闭）。 在那之后，没有出现uk在推导中保持不变。 因此，我们排除了一个临时变量。最后一步：在过程的最后，已转换因此，Fr只是一个S4nLP公式。此外，对于某些基项t，我们有t：（T→Fr）的希尔伯特式导子lt。 为了获得Fr，我们做以下工作：...（推导lt）n.t：（T→ Fr）n+1。 t：（T→Fr）→（T→ Fr）（公理E4）n+2。 （T→ Fr）（MP from n and n+1）N. Novak/Electronic Notes in Theoretical Computer Science 312（2015）143153不nn+3。n+4。Fr（ MPfromn+2andn+3）.1.5执行情况说明该过程在OCaml中实现。盒族的评估，在纸上被认为是微不足道的，是最大的障碍。每个盒子都被分配了一个唯一的家庭标识符。证明有分支，族通过传递扩展而增长，因此需要维护相关（属于同一族）的盒标识符的集合（族）的不相交集合。实际发生的是，每个盒子都被Pr（Provisional，F）替换，其中Provisional是这个唯一的标识符。该算法递归地遍历证明树，分配这些标识符，并收集有关哪些标识符属于哪个族的信息。在表示应用规则的每个步骤中，我们必须跟踪（规则的）行上方的每个公式是如何转换的，然后相应地转换行下方的公式对于所有证明从规则假设到规则结论的转变的经典推理，我们说存在一个（新的）证明常数来证明这个蕴涵，并使用反显性公理t：A→A推导出这样的蕴涵。在某些时候，我们意识到所产生的证明太长了，无论是步骤的数量还是所产生公式的长度。我们部分地解决了这两个问题。首先，根据Melvin Fitting的建议，我们引入了两个一步规则：演绎和提升。在每次应用提升引理或演绎定理之后，我们保留完整的推理链以用于验证目的，但为了显示目的而折叠它们因此，可以看到以下情况：K.A 1，...， Am，...， AnCIBBk+1。A m+1，...，A nA m→. →A1→B（通过扣除）和K.x1：A1，.，x n：A n Bk + 1。 x1：A1，.，x n：A n n=c（x1，...，x n）：B（通过提升）。其次，我们为证明中出现的每个长度大于5的证明项分配了新的（快捷）常数。我们将这些作业列在证明，并提供一个超链接，从每次出现这样一个常数，其定义。我们还插入了虚拟步骤来标记单个Gentzen证明步骤和某些阶段的Gentzen规则实现之间的界限这些虚拟步骤被标记为根岑规则或实现阶段名称，而不是希尔伯特规则或公理。这些虚拟规则也以正常字体大小呈现，所有中间步骤都以较小的字体呈现。该实现与多智能体自动证明器相连接逻辑与正当知识S4J在MetaPRL逻辑框架中[6;7]。的154N. Novak/Electronic Notes in Theoretical Computer Science 312（2015）143n−S4J证明器的输出是一个根森式的无割证明，这正是多项式实现程序所需要的。2实验实现过程在几个简单的例子上运行，以及在几个经典的谜题上运行：聪明女孩谜题和聪明男人谜题[16]，我们将不在本文中介绍我们在这里提出的泥泞的儿童难题和惊喜检查悖论。2.1图部分实验还附有这三种图形。第一个图显示了希尔伯特式证明中步骤数的增长，作为原始根森式证明中步骤数的函数。根据[5]，我们应该在这个图上观察到O（n2）-依赖第二个图显示了希尔伯特式证明中所有公式的总长度的增长，作为原始根森式证明中所有公式的总长度的函数。根据[5]，我们应该在这个图上观察到O（n6最后一个图显示了希尔伯特式证明中外部项的大小随原根森式证明中步骤数的变化根据[5]，我们应该在这个图上观察到O（n2）-依赖人们可以看到图表上的凸起。这些颠簸是（1999年）规则实现我们观察到，所有其他规则都是线性的步骤。因此，有可能通过分别计算“昂贵”和“廉价”规则来提高O（n62.2泥泞儿童拼图的实现孩子们在一起玩耍[10]。他们的母亲告诉他们，如果他们弄脏了，会有严重的后果。现在碰巧在他们玩耍的时候，一些孩子，比如说他们中的k，额头上沾上了泥每个人都能看到别人身上的泥他们的父亲来了，他说：“你们中至少有一个人的额头上有泥，”这样表达了 每个人在说话之前都知道一个事实（如果k >1）。父亲又问了一遍：“你们知道自己额头上有没有泥巴吗？”假设孩子们都是有感知力的，聪明的，诚实的，他们同时回答，会发生什么？有一个“证据”，即第一个K1次他问这个问题，他们都会回答“不”，但第k次，额头上满是泥的孩子们都会回答对于这个难题，一个简单的认知逻辑形式化可以导致不一致的假设集[7;11;12]。例如，设c1，...，c n是为N个孩子保留的命题变量，其中c i表示第i个孩子是muddy的。J形支架N. Novak/Electronic Notes in Theoretical Computer Science 312（2015）143155nn因为然后，公式集J（c1 c2... 对于所有i，对所有n≥2都不一致。j，J<$（kwi Ci）对于所有i，为了观察实现过程的复杂性，我们可以在下面的图表中找到五个孩子的这种矛盾形式化的复杂性在[14]中，一个类似于S4J使用了，所有模式均按时间，提出了一个基于模型的解决方案的泥泞的孩子。这个解决方案有一个模型，因此它避免了引入矛盾。作为参考，在[16]的附录中给出。在这里，我们提出了三个可能的形式化的泥泞的儿童puz-zle三个孩子，使用麦卡锡在最后一次形式化之后，给出了每个复杂性度量的图，为了便于比较，我们将它们我们使用以下符号：• K-模态现在有两个指标：时间和施事，即时间和施事.Kt， A代表t，代理人A知道A。• E t A：：= K t，a1A. A代表“每个人在时间t都• kwt，aA：：= Kt，a A<$Kt，a<$A，即A保持不变。”我们只用麦卡锡的思想，不用他的体系。我们停留在S4J中，没有引入与时间相关的新公理或规则，Kt，a只是K（t−1）n+a的语法糖，其中n是主体的数量在不失一般性的情况下，让我们假设第一个和第三个孩子是脏的，第二个是干净的，即，c1，<$c2，c3.(A) 较长版本表示法：孩子1代表第一个孩子，等等。假设：（含义：wmn代表(1)c1c2c3(2) kw3， 2c1;在时刻3，孩子2知道孩子1是否泥泞(3) kw3， 2c3;在时刻3，孩子2知道孩子3是否泥泞(4) kw3， 2（kw2， 1c1）;在时刻3，孩子2知道孩子1在时刻2是否知道他wmn(5) K3， 2（在时刻3，第二个孩子知道，156N. Novak/Electronic Notes in Theoretical Computer Science 312（2015）143n(6)（kw2， 1c3）（kw2， 1c2）在时刻2，孩子1知道孩子2和孩子3是否wmn，并且(7)K2， 1（在时刻2，孩子1知道，(8)（kw1，2c2）（kw1， 3c3）在第一时刻，没有人知道他们是否wmn，(9)（E1（c1c2c3））在第一时刻，每个人都知道其中至少有一个是泥泞的，(10)(11)和和（kw1， 1c2）（kw1， 1c3）在第一时刻，孩子1知道孩子2和孩子3是否wmn，（kw1， 2c1）（kw1， 2c3）在第一时刻，孩子2知道如果孩子1和孩子3 wmn，(12)（kw1， 3c1）（kw1， 3c2） 在第一时刻，孩子3知道孩子1和孩子2是否wmn(13) K3，2（（c1 <$c2 <$c3）→ <$kw2，1 c1）在时刻3，孩子2知道如果所有的都是肮脏的，孩子1在第2时刻不知道他是否泥泞或没有结论：kw3，2c2在第3时刻，孩子2知道他是否泥泞最后一个假设不能放松，因为在一个孩子说他不知道他是否泥泞的情况下，他不能真正从S4J中推导出来。所以当系统进行案例分析时，我们必须帮助它了解这些含义。(B) 一个简短的版本：如果我们使第二、第三和第四个前提更强，那么我们就得到一个更短的版本：假设：(1)c1c2c3(2)K3，2c1(3)K3，2c3(4)K3， 2（K2， 1c1）(5)K3， 2（（c1<$c2<$c3）→ <$kw2， 1c1）结论：kw3， 2c2。(C) 一个简短的版本与J：我们希望看到一些模态实现为证明项，因此我们用J替换了所有表示每个人都知道的事实（由于公开声明或谜题的一般条件）的模态。我们还强化了这个结论，指出在第三个时刻，每个人都知道每个人都知道自己，所以我们必须添加行（6），（7），将第一个和第三个孩子的知识从第二步带到第三步，我们添加行（9），以反映这样一个事实，即如果第二个孩子知道了自己，他会宣布这一点。我们没有在较长的版本中执行这种转换，因为证明者被复杂性所淹没。假设：(1)c1c2c3（2）J（kw3， 2c1）（3）J（kw3，2c3）（4）J（K2， 1c1）（5）J（K2，3c3）N. Novak/Electronic Notes in Theoretical Computer Science 312（2015）143157(6)J（K2， 1c1→K3， 1c1）(7)J（K2， 3c3→K3， 3c3）(8)J（（c1c2c3）→ <$（kw2， 1c1））(9)J（K3， 2c2→J（K3， 2c2））结论：J（K3， 2<$c2<$K3， 1c1<$K3， 3c3）。以下是所有三种情况的图表：2.3突击检查的形式化有一个著名的认知性的惊喜考试（SEP）：一位教授告诉他班上的学生，下周将有一个惊喜的课堂考试。 有5个工作日，每天上课。 教授能不能给 考试？我们认为教授和学生都是诚实和聪明的。根据通常的逆向归纳法，学生们认为考试根本不可能进行。事实上，考试不能在最后一天进行，因为这不会是一个惊喜。因此，考试不能在前一天进行，等等。当教授在第二天进行考试时，矛盾就发生了，这对学生来说是一个完全的惊喜！在[8]中有12页关于这个主题的参考文献，我们的目标不是成为这个领域的专家。这里有一个简单明了的SEP条件的形式化：假设一个非常信任的学生，尽管他或她很聪明，但在最后一天，如果测试还没有发生，他会非常困惑。他/她“知道”教授从不撒谎或犯错，同时似乎没有其他选择，考试必须在最后一天进行。对于“你认为今天会考试吗？”这个问题，任何肯定的答案，肯定的或否定的？会导致矛盾。因此，自然的答案是“我不知道”，这意味着（就像一个否定的答案）学生考虑的可能性，将没有测试。这个隐含的附加结果解决了这个悖论。在下面的形式化中，我们采取保守的方法，简单地证明整套假设是矛盾的，或者考试不能在一周的最后一天进行。我们使用不同的代理指数来表示不同的时间158N. Novak/Electronic Notes in Theoretical Computer Science 312（2015）143n和不同的学生，如果需要的话。同一学生的不同时刻之间的知识关系必须为个别公式明确说明，如S4J 没有内置的时间支持。di代表对于一个学生的情况，KiA意味着学生将在第i天之前知道A。在这种设置下，K1具有某种特殊的意义，因为它描述了我们对这个谜题的预先了解。2.3.1两天工作周1.一、J（（d1<$$>d2）<$（<$d1<$d2））2. K1（K2d1<$K2<$d1）3.K1<$K2d24. K1d1⊥第一个假设是考试将在两天中的任何一天进行。第二个假设是，在第一天之后，将知道考试是否已经进行。第三个假设实际上是我们对“惊喜”的形式化--在第二天之前，我们不知道第二天是否会考试。最后一个假设也是“惊喜”，这次是第一天。MetaPRL在几秒钟内找到了这个定理的证明2.3.2每周两天，许多学生通过重复相关公式并替换模态指数，可以简单地公式化2个学生的相同问题：1 .一、J（（d1d2）d2））5. K3（K4d1K4<$d1）二、K1（K2d1<$K2<$d1）6. K3<$K4d23 .第三章。 K1-K2d27. K3d1四、 K1d1⊥将这个定理推广到40个学生，对证明搜索时间有一些影响，但影响不大，仍然保持在一秒以下;它似乎是线性的或低次多项式。这是预料之中的，因为定理的结论与学生的数量无关，而且前4个假设无论如何都是足够2.3.3三天工作周第一个假设是，考试将在任何一天进行。第二、第三和第四个假设说我们知道前几天的结果的N. Novak/Electronic Notes in Theoretical Computer Science 312（2015）143159nnn第五至第八种假设是1 .一、 J（（d1d2d3）（<$d1d2d3）（<$d1d2d3））K1<$K2d2二、J（K2d1<$K2<$d1）6. K1<$K3d33 .第三章。J（K3d1<$K3<$d1）7. K2<$K3d3四、J（K3d2<$K3<$d2）8. K1d1第3天注意，这个定理只说明了在一周的最后一天考试的不可能性，并不涉及逆向归纳。所以这是一个简化的版本，基本上是建立悖论的第一步如果我们展开所有的析取，MetaPRL完成证明没有问题。但它无法在一小时内以全自动模式找到证据。从这个意义上说，这个定理比4个孩子的Muddy Children难题更难，可以在150-250秒内解决。全自动模式失败的原因是因为所有的J框假设必须在推理中使用两次，证明器的工作原理是首先耗尽所有最多使用一次模态的证明矩阵，然后通过允许每个模态有两个前缀解释来扩展搜索空间Muddy Children难题也需要这种搜索空间扩展，但我们在那里得到了更幸运的，尽管不清楚确切的原因。4个孩子的Muddy Children难题可以通过手动复制将在推理中使用两次的假设并避免所有模态的自动扩展来加速一个数量级。我们试图将同样的技术应用到我们手头的问题上，但它为证明者提供了太大的搜索空间，而且搜索根本没有在合理的时间内完成SEP的这种直接形式化导致了预期的矛盾关于SEP的更多信息，请参见[13]。3结论在[5]和[4]的基础上，在MetaPRL逻辑框架中实现了S4nLP的多项式实现算法，并与S4Jprover连接[7]。这个过程在几个有趣的例子上运行实现算法性能更好比预期的要多，瓶颈总是在S4J上prover的一面。 另另一方面，即使是小的S4JGentzen式证明也会导致超出人类理解的长的S4nLP虽然我们删除了证明中某些琐碎的部分，但结果太长，难以阅读。因此，指导性的部分是所得到的证明的长度，作为传入证明的函数的外部项的长度，以及实现的公式本身。该算法已经知道了十多年，但这项工作是第一次将其应用于比几个步骤更长的证明我们用了著名的Muddy160N. Novak/Electronic Notes in Theoretical Computer Science 312（2015）143儿童拼图和惊喜考试Parantry为我们的实验。4今后工作考虑到所遇到的并发症，似乎有助于修改或扩展S4nLP实现器的当前实现，以接受交互式/手动构造的证明。这将允许在SEP上评估三天或更长引用[1]E.安东纳科斯比较公正和常识。《符号逻辑通报》，2006年12月。2005年，美国手语协会夏季会议。[2]谢尔盖·阿特莫夫操作模态逻辑。技术报告MSI 95-29，康奈尔大学，1995年。[3]谢尔盖·阿特莫夫显式可证明性和构造性语义。符号逻辑通报，6（1）：1[4]谢尔盖·阿特莫夫基于证据的共同知识。技术报告TR-2004018，纽约市立大学博士计算机科学技术报告，2004年11[5]勃列日涅夫和库兹涅茨。让知识明确：这有多难。Theoretical Computer Science，357（1）：23[6]叶戈尔·布留霍夫自动证明搜索在逻辑的公正的共同知识。Holger Schlinglo，编辑，Proceedings ofMethods for Modalities Workshop 2005。洪堡大学，2005年。[7]叶戈尔·布留霍夫将决策过程集成到高阶交互式证明器中。博士论文，研究生院和大学中心，纽约市立大学，2006年。[8]蒂莫西·Y周梁淑意外检查或意外绞刑悖论。美国数学月刊，105：
我的内容管理
展开
