投影时序逻辑的公理系统与形式验证

为了采用定理证明的方法对并发及交互式系统进行验证,提出了一阶投影时序逻辑的公理系统.利用投影时序逻辑既可描述待验证系统性质和规范,又可描述其实现模型的特点,在同一投影时序逻辑框架可以方便地对待验证系统进行建模和性质描述,并使用公理系统完成系统性质的证明.最后通过一个实例来展示投影时序逻辑及公理系统在系统验证中的应用.

有穷时间投影时序逻辑的完备公理系统

为采用定理证明的方法对并发及交互式系统进行验证,研究了有穷论域下有穷时间一阶投影时序逻辑(projection temporal logic,简称PTL)的一个完备公理系统.在介绍PTL的语法、语义并给出公理系统后,提出了PTL公式的正则形(normal form,简称NF)和正则图(normal form graph,简称NFG).基于NF给出了NFG的构造算法,并利用NFG可描述公式模型的性质证明PTL公式的可满足性判定定理和公理系统的完备性.最后,结合实例展示了PTL及其公理系统在系统验证中的应用.结果表明,基于PTL的定理证明方法可方便用于并发系统的建模与验证.

论辩证逻辑的形式系统Z与ZT的超协调性

本文先着重从超越世界的语义学角度,讨论辩证逻辑形式系统Z的超协调性。进而在系统Z的基础上建立一个句法上扩展的超协调系统ZT。在系统ZT内进一步阐明辩证否定的逻辑性质。

逻辑的形式化与形式的系统化

逻辑学从亚里士多德开始就已经朝着这个方向发展了。这个方向我们今天把它称为逻辑的“形式化”。形式化是一种较为经济的抽象方法。它的特点是用字母或其它一些技术手段,例如表意的符号,去代表那些有相同特性的被研究的具体对象,从而把我们由原来的对具体对象的研究转换、上升为对字母或符号所代表对象的组合规律的研究。在逻辑中引进符号,对逻辑内容进行形式化处理,这是从亚里士多德《前分析篇》开始的。正如数学中发生的情形那样,逻辑成为形式逻辑,成为一门学科,符号的引入是关键的一步。

从易经逻辑到数理辩证逻辑

早在6000多年前,中国先人就创造了以爻卦为命题形式,以八卦和六十四卦为体系的辩证逻辑形式演绎系统。此后,又给出了爻辞和卦辞的语义解释系统。后来,又给出了《易经》的语义和语用解释系统。它自古至今,长盛不衰,成为中国的传统逻辑、文化发展的活水源头。以互补结构整体思想的形式结构和推理有效式规律为研究对象的数理辩证逻辑,是以易经逻辑为其辩证逻辑基础的,它又是易经逻辑的一致性扩大系统。它为实现易经逻辑的现代化发展提供了现代逻辑形式化方法。易经逻辑形式公理系统DPA++就是其现代化形式公理系统。

多值逻辑的公理化

给出了一种新的多值逻辑系统，公理化所得到的ＧＭＬ３形式系统与二值逻辑有本质的区别，二值逻辑是它的一个退化．

公理化方法是科学理论系统化的重要方法

任何一门科学当其积累了一定数量的概念、范畴、原理和定律之后,运用一定的逻辑手段把已经获得的各种庞大的理论知识——概念、定律和原理进行合理的重建,构成一个严密的科学理论系统,就成为无可避免的事情了。这是一门科学发展成熟的标志。公理化的方法是科学理论系统化的有效方法,是现代自然科学理论普遍采用的演绎系统的形式。我们研究和掌握公理化的方法,对于形成严谨的科学理论系统,推动科学的发展,迎接世界新的技术革命,具有重要的现实意义。

MSVL语言的公理系统的程序验证

MSVL语言是一种用于模拟、建模和验证程序的区间时序逻辑程序设计语言.为了证明区间时序逻辑程序的正确性,提出了MSVL语言的一个公理系统:包括正则形转换的状态公理和状态推演规则,以及将程序从一个状态转换到另一个状态的区间公理和区间推演规则.最后给出验证实例说明基于该公理系统的程序验证方法.

现代逻辑的思想方法与科学的眼界──从爱因斯坦的一封信谈起

现代逻辑的思想方法与科学的眼界──从爱因斯坦的一封信谈起邓生庆一作为本文开篇的话，我们不妨以本世纪最伟大的科学家爱因斯坦的一封短信谈起。４１年前，爱因斯坦在给Ｉ·Ｅ·斯威策的一封复信中谈到西方科学的基础和中国古代的重大发明，他写道：“西方科学的发展是...

命题逻辑语法完全性问题

本文对学界普遍认可的命题逻辑语法完全性问题重新进行分析 ,认为 :命题逻辑的语法完全性在逻辑上是一个关于形式系统和语义模型之间关系的二元谓词 ,是与具体的命题逻辑形式系统联系在一起的 ;指出 :公理数有限、有代入规则的命题逻辑公理系统具有语法完全性 ;证明 :由公理模式和分离规则构成的命题逻辑公理系统不具有语法完全性。

试探逻辑代数的特点和运用

逻辑代数的建立,展示了形式逻辑的改造,宣告了数理逻辑的诞生。然而,它在形式逻辑和数理逻辑中并未得到系统的运用。问题在于它的特点尚未得到充分的发挥。逻辑代数有何特点?如何运用?有必要进一步探讨。

论人工智能科学诞生的逻辑背景

论人工智能科学诞生的逻辑背景王建芳人工智能科学的诞生同其他许多自然科学相似，既需要一定的思想基础，又必须借助一定的物质手段。在对人工智能科学诞生行程的历史回顾中，我们会清楚地看到，人们对于它的构想与实践，与逻辑科学的演化与发展密切相关。一些逻辑学家为...

关于系统Z的一些意见

本刊1992年第6期刊发了张金成同志的《辩证逻辑形式化的研究》一文后,陆续收到了一些稿件,对张文展开了讨论。我们本着“百花齐放,百家争鸣”的宗旨,已在本刊第4期及本期发表了部分来稿。至此,对该文讨论暂告一段落。

数理逻辑的发展

数理逻辑又称符号逻辑,是用数学方法研究思维形式的逻辑结构及其规律的学科。所谓数学方法,是指用一套表意符号(即形式语言系统)表达思维的形式结构和规律,从而把对思维的研究转化为对符号的研究。以便摆脱自然语言的歧义性,构成能像算术或代数那样的严格精确的演算系统。

公理化方法的哲学分析

一九七八年在西德召开了第十六届世界哲学会议。大会以现代自然科学哲学问题为主题,分八个方面进行讨论,其中一个议题是关于科学数学化的成就和范围问题。经过讨论,会议认为,科学数学化包括科学的算术化、形式化和公理化。这个讨论反映了现代科学数学化这一特点已经引起国外哲学工作者的关注和研究。本文拟就公理化方法的作用和意义作些探讨。

原始命题的逻辑学研究──兼论多因-果的逻辑推理

本文对公理系统中的原始命题进行了初步的探讨。原始命题之间的蕴涵是一种纯形式蕴涵，它与一般实质蕴涵的区别是，纯形式蕴涵具有非传递性，一般实质蕴涵则满足蕴涵传递律。公理系统中有限个原始命题推导出结论命题的过程，可以理解为多因一果的推理。这种推理需要对究竟依靠多少个原因命题作为前提，进行主观的选择。本文将多因-果同一因一果两种推理方法作了比较，并简单解释了以往认为欧氏第五公设不能被证明的原因。

思维具体奥秘无穷——读《辩证逻辑—认识史的总结》有感

几年前,为了学习一些科学研究的方法,曾读过封毓昌先生的《辩证逻辑—认识史的总结》(下简称《总结》)一书。当时的感觉是,该书视角独到,脉络清晰,论述严谨,与大多数相同题材的书迥然有别,不失为一本难得的辩证逻辑专著。最近,重读此书,却为其关于思维具体之论述思想的深邃和隐喻的精妙所震撼,方悟出此书乃是关于思维具体的一部力作。 许多关于辩证逻辑的书都致力于把辩证法应用于逻辑,并强调舍此不能正确解决逻辑问题。但这样一来,就难免处处强调同形式逻辑的区别、对立,从而使形式逻辑成为自己不可缺少的参照系;一旦离开这个参照系。

现代演绎逻辑史考略

本文侧重考察自然语言逻辑史上所遇到的一些主要难题,怎样在与之苦斗的过程中寻求改良与改革的途径,又怎样在改良与改革中发现现代逻辑,从而论述现代逻辑是传统逻辑的自然历史发展。

公理化方法与辩证思维上升法

在辩证思维诸方法中,由抽象上升到具体的方法可以说是其核心,这主要是因为抽象上升到具体的方法概括了人类思维活动的全过程。人的认识活动始于对客观世界的外在特征的反映,即借助感官获得对象的整体表象,在此基础上,通过大脑的分析加工,进行思维抽象,然后再运用综合等手段,上升到思维的具体。