基于构造性思想的直觉主义逻辑证明语义

布劳威尔的直觉主义把数学理解为心智的构造性活动,只接受心智可构造的数学对象和数学证明。在直觉主义看来,判定一个命题为真必须要给出这个命题的构造性证明,对逻辑联结词及量词的理解也是基于构造性立场的。本文构建了直觉主义逻辑的证明语义,这是一种内涵语义,其特点是:遵循构造性思想、尽量贴近直观、避免使用集合概念,语义解释从具体命题、具体对象(个体)、具体性质和关系等出发,使具体命题成为“公式解释”和“直观有效”概念的基础。进而在这种语义下证明了直觉主义命题逻辑和谓词逻辑的可靠性。

证明论语义及其意义颗粒度

证明论语义是通过“证明”来解释表达式意义的逻辑语义学,与传统模型论语义在哲学和技术方法上存在诸多不同。它作为一种推理主义意义理论,又与布兰顿等的推理主义存在显著区别。证明论语义以典范证明而非“真”为中心建立有效性等语义概念,从而获得比模型论语义更为细密的意义颗粒度。本文通过阐释证明论语义的哲学背景和意义解释机制,指出其具有过于局限的“字符串式”的意义颗粒度,并证明对其放松会导致它迅速倒向模型论语义的颗粒度,从而说明证明论语义在意义颗粒度方面相对于模型论语义的优势是有限的。

现代汉语语义证明法的类型、特点和功能

现代汉语的语法证明包括语形证明法、语义证明法、语值证明法和语境证明法,语法证明的目的是证明某语言单位的语法性质和语法特点。语义证明法主要指从词汇意义的角度进行语法证明的方法,但语义证明法一般要和语法意义相结合才能进行语法证明。语义证明法可以分为直接证明和间接证明,直接证明指描写微观义素的义素化语义证明,即语义特征分析法;间接证明要变换语言单位的形式以便凸现原语言单位的语义特点来进行语法证明。间接证明包括利用外延分化形成的分解性语义证明,利用内涵类推形成的蕴涵性语义证明和利用成分关联形成的指向性语义证明。间接证明的理论依据是变换的语言单位和原有的语言单位具有内在的语义关联,而变换后凸现的语义特点成为原有语言单位的语义映射。就语义证明的效果而言,尽管不同话语的语义可能体现出一定的特殊性,但语义特点和句法形式相结合后能归纳出一定的类型化特征。

同步语言多线程代码生成的语义保持证明方法

同步语言具有确定性并行和精确时间语义等特性,因此被广泛用于设计和验证安全关键软件.随着安全关键领域应用多核处理器逐渐成为趋势,同步语言的多线程代码生成及其语义保持证明研究成为研究热点.目前,已有同步语言代码生成方法还较少考虑多线程代码生成的语义保持证明.因此,本文提出一种同步语言SIGNAL多线程代码生成的语义保持证明方法:首先形式化定义编译过程中源、目标、中间语言的结构化操作语义;其次形式化定义多线程代码生成过程;最后基于互模拟等价思想证明编译前后的语义一致性.

证明理论语义学及其意义阐述

逻辑及其合理性的确定是当代逻辑哲学研究的一个重要内容。证明理论语义学作为一种通过系统使用证明规则来确定逻辑常项意义的语义学方案。它的特征在于:语义不仅是外在的,同时也涉及到人的内在认知状态。一方面,对语言意义进行的形式化逻辑分析是客观的,能被看成是对世界直观理解的还原;另一方面,使用证明来呈现自然语言的意义和对世界最基本构件的理解,这体现了意义获得的认知过程。

逻辑常项的使用规则的生成与证成

在证明论语义学中,一个逻辑常项的I-规则通常作为该常项的意义定义是自我证成的,而其E-规则就是通过其与I-规则的协调性来证成的。这种思想遭受到tonk-问题挑战,而解决这个问题实质上就是解决逻辑常项的使用规则的协调性问题。E-规则的普遍形式所包含的GE-协调性没有对I-规则如何“协调地导致”相应的GE-规则做出清楚的描述,也无法用于解答普通E-规则的证成问题。基于GE-规则的生成机制的GM-协调性能够弥补这两点不足,但是它仍然无法排除具有弱E-规则的不协调的常项。由GE-和Ge-规则的生成机制所共同保证的Ge-协调性则可以克服以上这三点不足,从而能够为逻辑常项的使用规则的协调性问题以及证成问题提供更好的解答。

作为过程的论证和作为结果的论证

推理在我们的生活和工作中不可或缺。日常推理最大的特点在于它的非单调性。当今良好发展的经典单调逻辑仍无法有效处理非单调性日常类推,而抽象论辩理论则是对各种非单调推理进行形式化研究最有力的理论之一。用来证明各种论辩语义的争议树很好地结合了抽象的论辩框架与具体的推理过程,是研究自然语言论辩推理的有力工具。目前大多数的争议树证明都从论证作为过程的角度出发,对实时的论辩推理具有十分现实的指导意义,但仍存在一些问题。而从论证作为结果的新角度出发,我们给出了优先语义和基语义下的争议树证明理论。

模态解释的模态主义进路考察

模态主义主张模态是初基的,不可被还原。它的产生和发展与模态现实主义有一定的关联。近年来,模态主义得到进一步发展,不仅向逻辑常项理论和逻辑多元论延伸,并且提出了基于模态主义的模态知识论。模态主义虽然具有一定的技术与哲学优势,但是它难以彻底地摆脱一些理论困境。

根岑逻辑演绎思想的主要特征和哲学影响探析

论文在梳理根岑如何从逻辑公理化思想出发发展出自然演绎和矢列演算思想的基础上,总结出根岑逻辑演绎思想的主要特征。根岑对联接词引入和消去规则各自角色的理解及其采取的树形证明方式引导他发现并证明了切割消去定理。最后指出根岑的逻辑演绎思想对证明论语义学和意义理论有重要应用和哲学影响。