摘要：If the value structure of art were understood and explicated correctly, the traditional question “What is art” would become obsolete. The constitutive characteristics of art are not its ontic status among natural and artificial objects, but its direct participation in the artist’s realization of his/her intrinsic values on the one hand, and in the audience’s affirmative or negative responses with regard to his/her own realization of intrinsic values on the other hand. Here the two cases of realization of intrinsic values at the two ends are logically separated. Accordingly, there are contingencies for instrumental values intervened in the process of communication from one end to the other, so we need to be aware of the danger of equating instrumental market value of artwork with its artistic values.

摘要：图灵指出：“我希望数字计算机能够最终激起人们对符号逻辑的极大兴趣……人与这些机器的交流的语言构成了一种符号逻辑。”图灵所暗示的就是：程序设计语言不过是一种逻辑语言，而程序（或称算法）不过是用该语言表示的一列推理规则。蒯因也曾写道：“证明理论中的基本概念与机器计算理论中的基本概念相一致……（使得）关于数学证明的纯理论与关于机器计算的技术理论在底部合二而一。”但是，逻辑和计算究竟是如何关联的？本文主要从逻辑学演进的角度探讨这一问题，并简要介绍我们的相关工作。

摘要：自我欺骗现象与经典信念逻辑之间的偏差导致自我欺骗悖论,因此,建立合理的自我欺骗理论的必要条件是提出自我欺骗的认知机制的逻辑结构。该文试图采用逻辑分析和心理实验相结合的方法解决自我欺骗悖论,即在逻辑学层面说明矛盾信念间的逻辑关系,进而在心理学层面说明自我欺骗发生的机制。为了实现这一目标,首先用逻辑学的术语严格表述自我欺骗悖论;然后,在文献的基础上给出自我欺骗的逻辑结构;最后,根据上述逻辑结构设计并实施两可图认知实验,实验结果分析表明,自我欺骗的心理机制满足上述逻辑结构。

摘要：立场检测研究旨在提取文本相对于对特定话题所持的立场倾向。本文采用自然语言处理领域的基于提示学习的方法,针对论辩性文本,根据提示学习两大主要工程方法(模板工程和表达器工程)提出了新的设计方法:掩码位置导向的手工模板MPOT和语义相似度加权表达器SSWV。据此,本文提出了一个基于提示的论辩文本立场检测模型P-RoBERTaMPOT+SSWV,并和自动模板方法P-tuning进行比较。该模型在中山大学网络文本论辩语料库上和NLPCC中文微博立场检测数据集都达到了较好的准确率。本文实验显示在小样本学习条件下,P-RoBERTaMPOT+SSWV模型超过了使用预训练模型+微调方法的效果。本文研究表明,提示学习的模型设计方法有助于文本论辩立场检测任务,并在小样本的条件下也依然能取得十分可观的性能。

摘要：CTL模型检测技术已被广泛应用于形式验证领域。交互时态逻辑(ATL)是对CTL的一个扩展,用于表达多主体博弈结构上的性质。ATL使用合作算子来表达多个主体能够通过合作保证系统的设计目标。在实际应用中,我们需要知道主体的行动与系统的输出状态之间具有因果关系。在本文中,我们通过引入新的模态算子扩展ATL,使得这种因果关系得到表达。我们使用两种方式的扩展。其中之一是从主体的能力出发,直观上,如果一些主体可以通过合作的行动来保证系统进入某个状态,同时,这些主体也可以通过合作的行动保证系统不进入这个状态,则这些主体的行动与该系统状态间具有更强的因果关系。我们使用的另一种方式是从系统状态出发。我们考虑要想使系统进入某状态,哪些主体的行动的必不可少的,哪些主体的行动是充分的但非必要的条件。在本文中,我们扩展后的逻辑CATL和SATL表达力强于ATL,但计算复杂性与ATL相同。

摘要：直观地说,简洁性是指一个逻辑系统紧凑表示问题的能力。近年来关于简洁性的研究逐渐得到人们的关注。本文将讨论两类逻辑程序,即基数约束程序(Cardinality Constraint Programs,CCP)与前提嵌套程序(Nested Logic Programs,NLP)之间的简洁性。我们设计了一个从CCP到NLP多项式长度的等价翻译,这极大改进了Ferraris和Lifschitz提出的指数长度翻译方法,由此证明NLP至少与CCP一样简洁。

摘要：我们在膨胀不动点逻辑IFP的基础上,加入一种带有(多重)对数上界的新二阶量词,并且证明了,在有序结构上我们的新逻辑■logωIFP刻画受限非确定性复杂类βP。为了研究该逻辑的表达力,我们也设计了一种新的Ehrenfeucht-Fraïssé博弈,并说明在最一般的情况下,也就是在全体有穷模型之上,该逻辑对βP的刻画并不成立。

摘要：近年来关于不完全知识的规划成为活跃的研究领域,许多逻辑系统引入感知动作、条件规划描述这一问题。作为代表性的成果之一,Son和Baral提出了动作语言Ak及其不完全信息下的推理语义。本研究进一步为Ak设计了谨慎语义和弱谨慎语义,使得主体可以在严格安全环境下生成并执行可靠的规划。计算复杂性分析表明谨慎语义降低了Ak的推理复杂性;为上述语义提出用于验证条件规划推理机制的Hoare型证明系统,该系统是可靠和完全的,既可应用于规划生成,又可应用于规划验证;且该系统有离线规划的性质,即在离线状态下主体可以将已有的短的证明组成新的长的证明。

摘要：说服性传播是一种重要的现代传播活动。针对隐藏论证意图的独白式语篇,该领域的研究路径可划分为数据驱动型论证采掘和理论驱动型论证采掘,主要体现为基于语用论辩学和广义论证理论框架的论证性语篇提取。这两种操作程序具有清晰的理论边界:理论驱动型方法适用于在静态语境下重构强冲突型文本,其论证采掘不考虑目标及文体因素的影响,是一种依赖于分歧解决模型的“自上而下”式论证分析;数据驱动型方法既适用于在动态语境下直述强冲突型文本,也适用于识别弱冲突型文本,其论证采掘强调目标及文体因素的影响,是一种不具有模型依赖性的“自下而上”式论证描述。

摘要：1994年Gabbay等论证了时态逻辑的公理化系统和证明论方法不适于时态数据库推理建模,因此目前主要使用非公理化的时态逻辑做推理。然而非公理化的时态逻辑缺乏公理化性质约束,形式晦涩,无直观性与运算性,因而一般不用于知识推理。另一方面,1983年Allen提出了13种时态关系运算,并使用区间逻辑对时态关系进行表达,但这些运算只能表示时间本身的运算关系,未能体现时间与属性之间的映射关系,不能表达时态数据库属性间的推理与运算。此外,时态数据库中仍存在着许多开问题,例如在做属性推理与运算时出现的Now语义的不确定性问题。基于此,我们提出一种基于时态数据库属性推理的类型逻辑系统,其主要思路为将属性映射为类型,将类型映射为时间向量子集,以时间向量集为逻辑语义模型,在推理中从句法逻辑系统剥离对时间的表示,减少逻辑算子,与时间相关的运算单纯由语义模型支持,从而降低复杂性,提高运算能力。并且由于该类型逻辑系统是基于构造性语义的,能直观解释Now的不确定性问题。文中给出了相对该系统的时态数据库属性推理的应用示例,从技术可操作性上介绍了根据该类型逻辑设计的时态推理中间件原型及工作流程,最后从元理论范畴证明了系统可靠性与完全性的逻辑性质及切割消除与判定性的证明论性质。