多项式环中的非确定性语义：逻辑计算机科学电子笔记

可在www.sciencedirect.com在线获取理论计算机科学电子笔记305（2014）19-34www.elsevier.com/locate/entcs多项式格式中的非确定性语义Walter Carnielli沃尔特·卡涅利1，2 Mariana Matulovic玛丽安娜·马图洛维奇1，3中心逻辑，认识论和科学史（CLE）和哲学系坎皮纳斯州立大学-UNICAMP巴西坎皮纳斯摘要[6]中提出的自动定理证明方法，称为多项式环演算，是一种基于处理有限域上的多项式的代数证明机制。 虽然在一般领域很有用，在一阶逻辑，某些非真值函数逻辑，甚至模态逻辑（见[1]）中，该方法特别适用于确定性和非确定性多值逻辑，如这里所示。本文的目的是展示如何将该方法扩展到任何有限值非确定性语义，并通过开发能够将确定性和非确定性有限值逻辑系统中的可证明性转换为多项式环上的运算的软件来探索该方法的计算特性。关键词：多项式证明系统，确定性和非确定性多值逻辑，非确定性语义，可满足性，复杂性。1引言基于代数闭域上的形式多项式的代数证明系统形式多项式作为经典和非经典逻辑中的逻辑推导的有力工具，特别是对于命题（确定性和非确定性）多值逻辑、次协调逻辑和模态逻辑。在过去几年中，出版了一系列关于中华人民共和国及其适用性我们将主要想法总结如下。第一个粗略的想法出现在2001年的[5]中，随后在[6]中得到次协调系统mbC和mCi的多项式版本（形式不一致逻辑或LFI的特殊情况，参见。[9]在[7]中开发，1感谢Fapesp、CNPq和CPAI2电子邮件：walter. cle.unicamp.br3电子邮件地址：marianamatulovic@cle.unicamp.brhttp://dx.doi.org/10.1016/j.entcs.2014.06.0031571-0661/© 2014 Elsevier B. V.保留所有权利。20W. Carnielli，M.Matulovic/Electronic Notes in Theoretical Computer Science 305（2014）19其中提出了使用所谓的隐藏变量（由于次协调语义的非真值函数特性）。一阶逻辑的一元片段（FOL）的多项式版本已经在[8]中给出，其中还显示了任何有限函数如何通过有限域上的多项式来表示（参见[10]）。定理3.1，第6页）。 多项式方法也可以被看作是一种启发式的设备，在某些情况下能够发现新的简单逻辑系统或逻辑系统的新性质，如[10]和[11]所示。最近，文献[1]中的多项式证明方法已推广到模态逻辑。总之，多项式环的方法适用于各种逻辑系统，包括经典逻辑、模态逻辑、有限多值逻辑、一阶逻辑，更令人惊讶的是，正如我们在这里所展示的，甚至适用于一些用非确定性矩阵进行逻辑表示的逻辑。这种新的证明方法值得研究的原因有几个：(i) 搜索效率：多项式环的方法可以有助于解决与计算复杂性相关的问题，因为它可以揭示满意度的新观点;(ii) 广泛性：如这里所强调的，多项式环的方法可应用于各种逻辑系统，并且在这方面（在普遍性上）可与表格相比较;(iii) 与代数的关系：多项式环的方法恢复了布尔和莱布尼茨的传统中的通过代数的逻辑方法，这似乎已经被遗忘了;(iv) 启发式：多项式方法可以被看作是一种启发式方法，能够发现新的逻辑系统或逻辑系统的新性质关于如何将该方法作为启发式设备应用的示例，请参见[10]和[11]。在本文中，我们探讨的普遍性和计算特性的方法，将其应用到确定性和非确定性有限多值逻辑系统。我们还展示了一个软件PoLCa，它可以将任何有限值矩阵（确定性或非确定性）转换为具有伽罗瓦场系数的多项式。2多项式环演算-PRC基于多项式环的证明方法（PRC）是一种代数证明机制，其工作原理是将给定语言L的逻辑公式转换为有限域中具有系数的多项式，然后通过完成多项式运算来执行演绎。场的元素代表真值，多项式可以被认为是公式可以采用的可能的真值。这使得公式上的真值条件可以通过某些操作（PRC规则）来减少多项式来确定。PRC可以被看作是一种代数语义，其中多项式的结构反映了逻辑公式的真值条件的结构;它也可以被看作是一种证明方法（就像表演算可以被看作是一种理论证明或一种W. Carnielli，M.Matulovic/Electronic Notes in Theoretical Computer Science 305（2014）1921−L|≈|≈模型理论装置）。我们定义了一个（p，m）-多项式环演算（（p，m）-PRC）对于一个给定的比例逻辑系统L，基于伽罗瓦域，GF（p，m）对于p素数和m是一个非零的自然数，通过以下条款：(i) 所有的（p，m）-PRC项都是变量，所有的公式都是多项式[X];(ii) 在（p，m）-PRC中的操作受一系列规则的约束。 它们是：(a) 索引规则。• p.X|其中（p.x）表示（x + x +. +x），这样的加法被执行p次。• x i.x j x k（mod q（x）），其中q（x）是定义GF（p m）的方便的本原多项式，并且k = i + j（mod p m1）。(b) 环规则，一致替换和莱布尼茨规则（平等）4。这样，给定逻辑L的（p，m）-多项式环演算（如果没有混淆的危险，简单地写为PRC）基本上包括将L的公式转换为有限域中具有系数的多项式，并通过对这些多项式的运算（由上面定义的规则集 我们说，多项式规则证明了某个句子α， 如果通过应用规则（多项式α ∈F，系数在伽罗瓦域GF（pm）中），它的简化形式的平移永远不会输出区别真值集D总之，为特定逻辑L定义PRC包括：• 选择一个合适的有限域GF（pm）来表示真值，指定一个可区分的真值子集（在文献中也称为指定真值）。• 定义了一个由L的公式到GF（pm）中系数多项式的平移函数，即：FormL→GF（pm）[X].• 在某些情况下，必须添加一些对翻译的约束，例如模态逻辑以多项式格式表示的情况（参见[1]）。获得（确定性或非确定性）有限值逻辑的多项式表示的过程始于为将要翻译的语言中的每个连接词构建真值表。从现在开始，为了表征对应于公式的多项式，有两种算法选项可以根据其进行：通过拉格朗日插值或直接通过求解有限域上的线性系统。[4]这个符号表示“用多项式规则进行归约”;然而，为了便于阅读，我们在没有误解的危险时，在任何地方都使用等号。22W. Carnielli，M.Matulovic/Electronic Notes in Theoretical Computer Science 305（2014）19L2.1获得可由有限矩阵表征的多项式环系统的算法获得对应于确定性或非确定性有限值逻辑的多项式的算法始于为每个连接词构建真值表，这些连接词构成了将要被翻译的逻辑系统的语言。因此，我们有：算法1第一步：给定一个固定逻辑L，我们选择一个有限域GF（p m）（方便的是p是素数，m是一个非零的自然数），使得这个域可以表示L的真值。步骤2：选择一个集合D，D<$GF（p m），作为被区分（或指定）的真值。步骤3：定义一个函数，该函数将具有GF（pm）中的系数的多项式的公式与集合X中的变量进行转换，即：对于L→GF（pm）[X]在[8]中证明了任何有限函数都可以用适当的有限域上的多项式表示。即：定理2.1（GF（pn）中有限函数的表示）：设A是任意具有基数的有限集|一|= k，f：Am→A是A上的任意m个自变量的函数，GF（pn）是k ≤ p的伽罗瓦域.则f可以表示为GF（p n）[x1，.， x m]。为了通过求解线性系统来确定多项式，我们回想一下，有限值逻辑的定义取决于真值的有限个数n，n≥2（例如，如果n= 2，我们将处理一个二值系统，如果n=3，我们将处理一个三值系统，等等）。通过以矩阵的形式表达这些真值，所有可能的逻辑连接词都可以被定义。在本文中，我们将把自己限制在代表有限值系统中绝大多数逻辑联结词的一元和二元真值表上（当然，k元联结词的情况也可以类似地处理对于一个二值逻辑，所有可能的真值表都由下列多项式表示，其系数在域Z2中：p（x）=ax+bq（x，y）=n+bx+cy+d类似地，在三值逻辑中，所有一元和二元连接词分别由以下多项式表示，其系数在域Z3中：p（x）=ax2+bx+cq（x，y）=ax2y2+ajx2y+ajx2y0+bxy2+bjxy+bjxy0+cx0y2+cjjx0y+cjjx0y0W. Carnielli，M.Matulovic/Electronic Notes in Theoretical Computer Science 305（2014）1923∪˜nn在n值系统中，所有一元和二元联结词将分别由系数在域GF（pm）中的多项式定义（对于最小pm，p是素数，m是非零自然数，使得n≤pm）：p（x）= a n−1x n−1+ a n−2x n−2+. +a0x0，q（x，y）=an−1，n−1xn−1yn−1+. . . +ai，jxiyj+. . . +a0，0x0y0通过对q（x，y）赋值，例如在二元连接数的情况下，我们得到一个具有n2个方程和n2个未知数的线性系统，正如上面提到的定理所示，它有一个唯一的解。同样地，如[8]所示，多项式可以通过拉格朗日插值来确定，拉格朗日插值是一种众所周知的数值分析的一般方法，它使人们能够在多项式中给定许多点的情况下导出多项式，但这里仅限于有限的情况。两种方法（基于上述定理2.1和下面的定理2.2）都保证了第5节中描述的PoLCa软件包的校正在具有非确定性矩阵的系统的情况下，过程是类似的，但略有区别：非确定性矩阵可以被视为熟悉的有限矩阵，区别在于条目可能具有一组真值，而不是单个真值。在有一组真值的条目中，引入一个新的多项式来表示这种非确定性条目。新的多项式将被定义为伽罗瓦域GF（pm）[X XJ]中的系数，其中XJ表示一组新的变量，称为隐变量。定理2.1的直接推广适用于非确定性矩阵。定理2.2（伽罗瓦域上有限确定和非确定函数的表示）：设M = V，D，O是一个有限非确定矩阵，根据定义3.1。则M可以表示为一个多项式，其系数在一个适当的伽罗瓦域中。V是的。 如果ea-c-h函数V→ 2 − {\displaystyleV → 2 −{\displaystyle V}返回0个酉集（即，单例），这只是一个确定性函数，其推理与定理2.1相同。否则，对于V中的一个输入，函数f返回在2V−{f}中的一个非空集合C上的一组函数。但这类函数具有基数性|C||，并且可以表示为合适的域GF（p）上的多项式。|, and can beexpressed as polynomials over a suitable field GF (p ).在这种情况下，所有输入为Vm，输出为VxGF（Pn）[XJ]的函数类也可以用多项式表示，这是通过应用定理 2.1.Q隐变量（或更一般的隐项）是额外的代数变量，与命题变量相关的变量不同，应该在同一个字段中取值。通过这种方式，语义的非确定性特征通过将真值分配给隐变量来捕获。对应于特定公式的多项式中存在隐变量，表明24W. Carnielli，M.Matulovic/Electronic Notes in Theoretical Computer Science 305（2014）19该公式的真值在函数上不依赖于其命题变量的真值。重要的是要注意，需要的隐变量的最大数量n在一个有限的非确定性矩阵中表示非确定性元素：2在最坏的情况下（所有条目都是不确定的），V− {n}由Vn限定。也就是说，要引入的隐变量的最大数量是真值V的n次幂的数量，其中n是矩阵的arity。由于这些参数是固定的，因此没有组合爆炸的危险作为一个动机，我们将首先定义一个PRC的经典命题计算器（CPL），然后将其扩展到非确定性系统。在这两种情况下，公式都被转换为域Z2（CPC中的Z2[X]和非确定性矩阵中的Z2[X<$XJ在这种情况下，x+x形式的元素归约为0，x.x形式的元素归约为x。定义2.3（CPL的PRC）设For CPL是CPL的合式公式集，设X ={xp1，xp2，. }是代数变量的集合CPL的PRC由平移函数确定：对于CPL→Z2[X]，定义为：• （pi）对于每个原子变量pi，• （<$α）= 1+（α）• （α<$β）<$=（α）<$·（β）<$• （α<$β）<$=（α）<$·（β）<$+（α）<$+（β）<$• （α→β）=（α）·（β）+（α）+1CPL中的推导的说明性示例如下：实施例2.4 |CPL（p（p<$$>p）=p+（<$p）+p+（<$p）==x（x+ 1）+x+x+1 ==x.x+x+x+x+1=x+x+x+x+1= 0 +0+ 1= 1个3基于多项式的非确定性语义在[2]和其他文献中，A. Avron通过对通常矩阵的推广提出了非确定性真值的概念，其中给定复杂公式的真值在一组选项中非确定性地选择这种非确定性方法，当应用于多值矩阵时，扩展了真值函数的概念，至少当所讨论的选择的非确定性特征是有限有界的时候。逻辑中的分析性问题指的是这样一种性质，即为了阻止-W. Carnielli，M.Matulovic/Electronic Notes in Theoretical Computer Science 305（2014）1925˜˜在挖掘φ是否由Δ导出时，总是只检查有关Δφ {φ}的子公式的信息。几种语义方法，如可能的翻译语义学（参见。[4]，也在[9]中）和非确定性矩阵，允许将真值函数性的概念与分析性的概念分开：一些语义可以是分析性的，而不一定是真值函数性的。非确定性矩阵构成了多值矩阵的轻微推广，但适用于更广泛的逻辑，这些逻辑不能通过普通的有限矩阵来表征。尽管哲学和逻辑中的分析性概念并不一致，但它们确实是有联系的：在1974年的《参照的根源》一书中，W。诉O.奎因为分析性的概念辩护了一个更广泛的解释，我们可以称之为“学习过程”。奎因甚至建议三元非功能矩阵（从我们的角度来看，完全不确定，参见。[16]，pp.76-77），好奇地期待非确定性矩阵5。定义3.1命题语言L的非确定性矩阵（简称Nmatrix）是一个元组M=V，D，O，其中：• V是真值的非空集合;• D是V的一个非空真子集，即D ∈ V。• 对于L的每一个n元连接数，O包含一个相应的n元函数从Vn变为2V − {\displaystyle 2 V− {\displaystyle 2 V −{\displaystyle 2 V −}}。我们说，M是有限的，如果V也是定义3.2设W是L的公式集。N 矩阵M中的（合法）赋值是函数v：W→ V，对于L的每个n元连接数n，满足以下条件，且n =1，...，n∈W：v（（1，.， n））∈ n（v（n1），.， v（n））。正如预期的那样，一个普通的（确定性的）矩阵被识别为一个Nmatrix，其在O中的函数总是返回单例。这样，非确定性矩阵就构成了确定性矩阵的真正推广。下面的两个例子说明了这样的语义是如何推广经典情况的。例3.3考虑语言L=，，→，<$，其运算符（，，→）被经典地解释，而否定允许矛盾律，但不一定支持排中律。这些条件定义了以下N矩阵M2=（V，D，O），其中V={t，f}，D={t}和O是5我们感谢Marcello D 'Agostino教授26W. Carnielli，M.Matulovic/Electronic Notes in Theoretical Computer Science 305（2014）19由下式给出不¬˜{f}F{t，f}不不∨˜{t}∧˜{t}˜→{t}不F{t} {f} {f}F 不 {t} {f} {t}F F{f} {f} {t}经典的否定在这里可以在M2中定义为：=→。在真理表方面，我们有：因此，完整的命题经典逻辑PRC可以在这个逻辑中定义例3.4考虑语言L=，，→，<$，其运算符（，，→）被经典地解释，而否定允许矛盾律，但不一定支持排中律。这些条件定义了以下N矩阵M2=（V，D，O），其中V={t，f}，D={t}，O由下式给出：不¬˜{f}F{t，f}不不∨˜{t}∧˜{t}˜→{t}不F{t} {f} {f}F 不 {t} {f} {t}F F{f} {f} {t}经典否定在M2中又可以定义为：否定=否定→否定，因此PRC现在可以在这个逻辑中定义在真理表方面，我们有：不¬˜{f}∼˜{f}F {t，f}{t}4形式不一致逻辑mbC如[2]所示，mbC系统的N矩阵由三元组M=其中：• V={f，t，I}={0，1，2};不¬˜{f}∼˜{f}F {t，f}{t}W. Carnielli，M.Matulovic/Electronic Notes in Theoretical Computer Science 305（2014）1927021∨˜0{0}{1，2}{1，2}2{1，2}{1，2}{1，2}1{1，{1，{1，021∧˜0{0}{0}{0}2{0}{1，2}{1，2}1{0}{1，{1，021→˜0{1，2}{1，2}{1，2}2{0}{1，2}{1，2}1{0}{1，{1，021¬˜{1，2}{1，2}{0}021∨˜0{0}{1}{1}2{1}{1}{1}1{1{1{1021∧˜0{0}{0}{0}2{0}{1}{1}1{0}{1{1• D={t，I}={ 1， 2};• O是由以下定义的操作：021˜◦{0，1，2}{0}{0，1，2}获得相应多项式的过程，在这种情况下在域Z3中，可以通过定义具有真值集合的条目1（表示“存在”）和0（表示“不存在”）的二值辅助表来简化。因此，在有多个真值的地方，条目是1，否则是0。从这些辅助表中，我们得到辅助多项式，这些多项式将被提交给必要的变化，以表示非确定性表。这种情况下的辅助表是：021→˜0{1}{1}{1}2{0} {1}{1}1{0} {1}{1}021¬˜ {1}{1}{0}021˜◦ {1}{0}{1}28W. Carnielli，M.Matulovic/Electronic Notes in Theoretical Computer Science 305（2014）19⎪⎨a+2aJ+2b+bJ+ 2=1021∨˜0{0}{1，2}{1，2}2{1，2}{1，2}{1，2}1{1，{1，{1，021∨˜0{0} {1}{1}2{1}{1}{1}1{1 {1}{14.1mbC中析取算子的多项式表示作为一个例子，我们在这里详细计算mbC的析取算子，表示在非确定性矩阵中。如上所述，mbC系统的N矩阵是三值的，因此将表示一元和二元连接词的一般多项式由下式给出(i) p（x）=ax2+bx+c.(ii)p（x，y）=ax2y2+ajx2y+ajx2y0+bxy2+bjxy+bjjxy0+cx0y2+cjx0y+cjjx0y0.如上所述，关于N矩阵的mbC的析取算子由下式给出：通过分析辅助表，我们可以看到，（0， 0）= 0;p（0，2）=p（0，1）=p（2，0）=p（2，2）=p（2，1）=p（1，0）=p（1，2）=p（1，1）= 1。现 在 ， 通 过 将 这 些 值 代 入 一 般 多 项 式 p （ x ， y ）=ax2y2+AJX2y+ajx2y0+bxy2+BJxy+BJJxy0+cx0y2+CJx0y+CJJx0y0，我们得到未知数a，aj，AJJ，b，bj，BJJ，c，CJ，CJJ中的九个方程的线性系统。该系统快速给出cJJ= 0，cJ= 0，c= 1，bJJ= 0和aJJ= 1，并简化为以下四个方程的线性系统(1)a+aJ+ 2b + 2bJ +2 = 1a+ 2aJ +b+ 2bJ +2 = 1⎪a+aJ+b+bJ+ 2=1求解系统，用于析取的辅助多项式为：p（x，y）= 2x2y2 +x2+y2现在有必要回忆一下，辅助矩阵是通过将析取算子的N矩阵中的值{1， 2}替换为{1}而获得的现在辅助多项式已经确定，我们需要拯救N矩阵的特征，这将通过使用一些额外的（隐藏）变量来完成。5一般三值场景中的隐藏变量这里的想法是，真值的非确定性集合（即，f{0，1，2}的非空子集）可以用新的、额外的变量的p多项式来表示，W. Carnielli，M.Matulovic/Electronic Notes in Theoretical Computer Science 305（2014）1929.Σ22.Σ.- 是的 Σ.- 是的 Σ..好吧ΣxJ2+12（xJ2+ 1）（考虑到p∈（x，y）=2x2y2+x2+y2xj2+ 1;p→（x，y）=x2y2+ 2x2 +1XJ2+ 1;.Σ多项式xJ2+ 1，使用新的（隐藏的）变量xJ。我们称之为隐藏变量作为一个例子，注意多项式x2被约束到集合{0，1}，因为对于一个yx∈{0，1，2}，我们有一个x2∈{0，1}，或者在其他情况下：• 如果x= 0，则02 = 0。• 如果x= 1，那么12= 1。• 如果x= 2，则22 = 4<$1（mod 3）。对于同一组真值，显然存在其他受约束的多项式（实际上，也可能存在从{0，1，2}到{0，1}的满射函数），但对于我们的目的，使用其中任何一个都是足够的。以同样的方式，多项式x2+ 1被约束到集合{1，2}中（对于多项式2也是如此。x + 1 .）并且多项式2x被约束到集合{0，2}。这样，N矩阵中的真值集合{1， 2}可以表示为：因此，我们必须将上面获得的辅助多项式乘以新的XJ2+ 1，结果与用多项式表示下表相同，其条目本身是多项式021∨˜0{0}xJ2+1xJ2+12xJ2+1xJ2+1xJ2+11xJ2+1xJ2+1xJ2+1读者可能会注意到，我们选择在辅助表中用y1表示集合{1，2}是一个随机的（但不是随机的）。venie nt）。如果我们用2表示{1，2}，我们因此，mbC中的析取算子的所得多项式最终由下式给出p∈（x，y）= 2x2y2 +x2+y2 xJ2+1现在，对其余算子进行同样的推理，我们得到：p（x，y）=（.X. y）。XJ2+1;Σp<$（x，y）=x2+x+1xJ2 + 1;p（x，y）= x2+ 2x +1（xJ）.将多项式域算术）。30W. Carnielli，M.Matulovic/Electronic Notes in Theoretical Computer Science 305（2014）19在环Z2[X<$XJ]内，其中X={xp：p∈ForL}且XJ=xJp：p∈对于L需要强调的是，LFI的多项式版本（参见[9]中的此类逻辑），由域Z2上的多项式表示，也可以定义为二元非真值函数语义，如[7]中所做的那样由此产生的多项式（在Z2上）与这里所示的多项式（在Z3上）不同。在某种意义上，N矩阵恢复了在二进制语义中丢失的真值功能的一部分，而多项式表示则巧妙地表达了这种细微差别。更多详情，请参见[7]。请注意，mulasi n的翻译是polynom。次幂函数这样，多项式可以被视为句法元素，其语义部分是I：Z2[X<$XJ]→Z2中的解释。定理5.1对于每一个命题赋值v，存在一个运算（定义于[1]）和环同态I：Z2[X] →Z2，使得：v（α）= I（α），即：v（α）= 1 i <$I（α<$）= 1 ∈Z2.因此：v（α）= 0 i <$I（α<$）= 0 ∈Z2.是的。 设v：F→{0，1}是一个值. 定义，I（xp）= 1 iv（p）= 1;I（xp）= 0 iv（p）= 0.在不太正式的术语中，我们有：I（xp）=v（p）。只需要证明v（α）=I（α≠），α∈For。因此，通过归纳公式的复杂性，我们有：• 对于否定：I（<$α）= 1惠I（α）+1 = 1惠Z2 I（α）= 0惠HIv（α）= 0惠v（<$α）= 1.I（<$α）v= 0惠I（α）v+1 = 0惠Z2I（α）v= 1惠HIv（α）= 1惠v（<$α）= 0.• 对于合取：I（α<$β）<$=I（α）<$.I（β）<$= 1惠Z2I（α）<$= 1和I（β）<$= 1惠HIv（α）= 1和v（β）= 1I（α<$β）<$=I（α）<$.I（β）<$ = 0优惠Z2 I（α） = 0或I（β） = 0HIv（α）= 0 或v（β）= 0惠v（αβ）= 0。• 对于（，→），证明是类似的。Q因此，如果公式α ∈ L的多项式平移α∈Z2[X]，则公式α∈ L是满足的 在一个特定的真值集合D∈F内是封闭的.W. Carnielli，M.Matulovic/Electronic Notes in Theoretical Computer Science 305（2014）1931∪→⎨定理5.2对于每个赋值v，定义一个解释I：Z2 [X XJ] Z2为环同态，使得v = I0（）≠ 0，即，v（α）= I（α）.因此，对于mbC中的所有句子α，(2)v（α）=π1，当且仅当I（απ）= 1.α0，当且仅当I（α0）= 0.证据 在[15]中找到Q基于定理5.1和5.2，我们得出结论，上述多项式为[2]第3节中给出的正确和完整的结构提供了多项式表示从这一点来看，很明显，我们的方法在多项式方面为mbC（在这种情况下，三值和非确定性）产生了正确和完整的语义。然而，对于相同的演算mbC，也存在确定性的二值语义。一般来说，当有一个多值非确定性语义（我们可以称之为在[9]中，作者为系统mbC提出了一个半真值函数语义;该语义也可以用多项式表示，这为比较提供了一个共同的基础设是由={，，→，<$，}形成的签名，使得P={pn：n∈ω}是原子公式的集合，ω是一元算子.我们定义，像往常一样，为作为一组公式自由产生的P超过为。设2=def{0，1}为两个真值的集合，其中1表示一个mbC-赋值是任何函数v：对于v→2，服从以下条款：(v1)v（α）= 1，则v（α）= 1，v（β）= 1。(v2)v（α≠β）= 1 ssev（α）= 1或v（β）=1。(v3)v（α→β）= 1 ssev（α）= 0或v（β）= 1。(v4)v（<$α）= 0意味着v（α）= 1。(v5)v（<$α）= 1意味着v（α）= 0或v（<$α）= 0。在这种半真值函数语义学中，mbC系统的多项式环演算由以下步骤定义。设X={x p1，x p2，. }和XJ={x α1，x α2，. }代数变量的不交集，分别用命题变量p1和mbC公式表示，用αi在这种情况下，XJ中的变量mbC关于这个二值语义的多项式环演算由平移函数定义：n：对于mbC→Z2[X<$XJ]使得：(i) （pi）n=xi，其中xi∈X，p是原子数.(ii) （α<$β）<$=α<$β<$。32W. Carnielli，M.Matulovic/Electronic Notes in Theoretical Computer Science 305（2014）19(iii) （α<$β）<$=α<$β<$+α<$+β<$。(iv)（α→β）α=αβα+α αβ+1。(v) （<$α）n=αnxα+1，ondexα是XJ中的隐变量。(vi) （α）x=（αx（xα+1） +1）xα，如果xα是隐变量X '.因此，我们有相同的系统（mbC），其特征在于两个不同的语义，其多项式特征具有不同的性质。使用非确定性语义的有限结构的好处是保留了具有普通有限值语义的逻辑的优点（特别是：可判定性和紧致性），同时它适用于更大的逻辑家族。关于N矩阵的另一个重要的观点是，多值矩阵概念的推广允许我们为一个不能用有限（真值泛函）矩阵表征的逻辑提供一个有限结构，就像mbC的情况一样。这自动地为mbC提供了一个决策过程，例如，这仅仅是通过更一般的可能翻译语义的概念给出的（参见[9]）。虽然N矩阵的概念只是可能翻译语义概念的一个特例，但N矩阵构成了计算语义的更方便的工具，其多项式表达式也具有这一特性。当然，上述方法一般适用于N矩阵;特别是所有可以由非确定性矩阵表征的LFI，尽管具有非有限值语义，但可以类似地处理作为对该方法的最后评论，在我们的多项式语义和关系语义之间有一些自然的联系，正如J. M.Dunn在[14]中，并在其他几篇论文中进行了研究，特别是[3]。应该清楚的是，我们在本文中对有限结构的限制不是必要的。通过任意域上的多项式对逻辑进行抽象刻画，反之亦然，对定义在形式幂级数环上的一般结构进行刻画，解释为逻辑，是本研究的下一步6PoLCA软件PoLCa软件6（开源和公开可用）翻译几个逻辑（如多值，次协调等）的句子，其语义是确定性的（真值函数）或非确定性的（受控的非真值函数），转换成有限域上的多项式，自动化上面的例子中所示的内容。在这样的系统中的证明，然后，减少到处理多项式在一个自然和直观的方式。Brie-briey，给定真值表的集合，由确定性矩阵或6Glauber De Bona编程，Mariana Matulovic和Walter Carnielli设计。W. Carnielli，M.Matulovic/Electronic Notes in Theoretical Computer Science 305（2014）1933非确定性矩阵（Nmatrices）定义任意量的逻辑运算符，PoLCa包（PolynomialRing Calculus Software）计算其整数变量表示逻辑运算符的自变量的多项式，使得多项式将模拟对应（确定性或非确定性）真值表的所有输入-输出值程序的正确性由定理2.1和2.2保证。程序输入由一个文本文件给出，该文件指定了感兴趣的运算符的矩阵。第一行（头）文件必须按顺序指定真值的数量，矩阵被指定的逻辑运算符的数量以及每个运算符的这些值应该用空格分隔的自然数来指定。例如，如果我们对两个运算符感兴趣，分别是三元和一元，有五个真值，输入文件的第一行应该包含：5 2 3 1（五个真值，两个运算符，运算符的arity，分别为三个和一个。在具有n个真值的逻辑中，这些值将由自然数0，1，2...表示n-1，但作为最小伽罗瓦域GF（pm）的元素，使得n≤pm。例如，考虑一元运算符o（x）的真值表X0 1 2o（x）1 0 2在程序中，它将由以下行表示：1 0 2要表示值的集合（非确定性）表，只需将集合的元素放在用逗号分隔的大括号中。例如，如果对于其参数的某些值，运算符可以取值1或2，则应将它们放置在它们在N矩阵中出现程序的输出是纯文本的。对于在输入中指定了（确定性或非确定性）真值表的每个运算符，分别返回一个多项式。变量是按字母顺序排列的字母，反映了输入真值表指定中隐含的参数顺序，如上所述。输出字符串简单地列出了系数，包括零，以相反的顺序，在多项式提出。欲了解更多详情，请访问：http://marianamatulovic.wix.com/polyringcalculus确认该研究由FAPESP（巴西LogCons 2010/51038-0主题项目）和巴西国家科学技术发展委员会（CNPq）的个人研究资助。巴西的CPAI-UnB提供了额外的赞助34W. Carnielli，M.Matulovic/Electronic Notes in Theoretical Computer Science 305（2014）19引用[1] Agudelo，J. C.，Carnielli，W.一、模态逻辑的多项式环演算：模态的新语义和证明方法，符号逻辑评论。4（2011），150[2] Avron，A.，具有一致性运算符的逻辑的非确定性语义，近似推理杂志。45（2007），271[3] 好吧，K.， 和Dunn，J.M.，“广 义 伽 罗 瓦 逻 辑 ： 非 经 典 逻 辑 演 算 的 关 系 语 义 学 ” ， CSLI 讲 义 -CSLI出版物，2008年。[4] Carnielli，W.一、次协调逻辑的可能翻译语义。在：Frontiers in Paraconsistent Logic：Proceedings of the IWorld Congress on Paraconsistent，Ghent，1998，pp.15972编辑：D. Batens等人，国王学院出版社，2000年。[5] Carnielli，W. 一、第二届国际原理学术讨论会，卢卡谢维奇逻辑学系统的多项式程序（2001），6[6] Carnielli，W.一、多值逻辑的多项式环演算，第35届多值逻辑国际研讨会论文集Calgary，Canada（2005），20[7] Carnielli，W.一、Polynomial Ring Calculus for Logical Inference，CLE e-Prints. 5（2005），1-17. 网址：ftp：//ftp.cle.unicamp.br/pub/e-prints/vol.5，n.3，2005.pdf.[8] Carnielli，W.一、Polynomizing：Logic Inference in Polynomial Format and the Legacy of Boole，Model-Based Reasoning in Science，Technology，and Medicine，Magnani，L.和Li，P.，编辑：斯普林格出版社。64（2007），349[9] Carnielli，W.一、Coniglio，M. E、和Marcos，J.，形式不一致的逻辑，哲学逻辑手册，Gabbay，D.，和Guenthner，F.，Eds14（2007），15[10] Carnielli，W. 一、 F正规多项式和形式的法律，逻辑的多维度，B'eziau，J。是的，Costa-Leite，A.，Eds.54（2009），2002-2012。[11] Carnielli，W.一、形式多项式，逻辑学和逻辑证明，逻辑研究，Karpenko，A.美国，艾德哲学研究所-俄罗斯科学院出版社16（2010），280[12] Carnielli，W.一、处理多项式的证明：逻辑与元逻辑教学工具，会议录第三届国际逻辑教学工具大会，西班牙萨拉曼卡（2011），1[13] D'Agostino，M.，分析推理和逻辑运算符的信息意义，Logique et Analyse，2013年出版。[14] Dunn，J.M.，一级蕴涵和耦合树的直观语义，哲学研究29（1976），149[15] Matulovic，M.，“Proofs in the 论文坎皮纳斯州立大学（UNICAMP），巴西，2013年。[16] Quine，W.诉O.，