数理逻辑之 入门及参考资料推荐

简介: 打算发表一系列关于数理逻辑基础的小文章,希望对一部分读者有用。   数理逻辑又称符号逻辑、理论逻辑。它既是数学的一个分支,也是逻辑学的一个分支。是用数学方法研究逻辑或形式逻辑的学科。其研究对象是对证明和计算这两个直观概念进行符号化以后的形式系统。

打算发表一系列关于数理逻辑基础的小文章,希望对一部分读者有用。

 

数理逻辑又称符号逻辑、理论逻辑。它既是数学的一个分支,也是逻辑学的一个分支。是用数学方法研究逻辑或形式逻辑的学科。其研究对象是对证明和计算这两个直观概念进行符号化以后的形式系统。数理逻辑是数学基础的一个不可缺少的组成部分。虽然名称中有逻辑两字,但并不属于单纯逻辑学范畴。(百度百科)

也许看了上述定义你依然不知道学习计算机技术和数理逻辑之间有什么关系。简单的说,软件形式化方法已被广泛关注(你可以搜一下这方面的论文,十分多)。规范语言、定理证明器、模型检测器正被企业常规地应用。而数理逻辑是所有这些技术的基础。现在数理逻辑是计算机科学与技术专业的一门重要的基础课程。

 

数理逻辑基本的概念涉及:

1。命题逻辑

(包括命题、自然演算、相继式;

合取规则、双重否定规则、蕴含消去规则、MT规则、蕴含引入规则、析取引入和消去规则、copy规则、否定规则、否定引入规则、

MT导出规则、双重否定导出规则、PBC导出规则、排中律导出规则;

合式公式及其语法树和字符串、合式公式的高度、重言式;

范式的语意等值、可满足性、有效性;

合取范式、析取子句、Horn子句;

逼迫规则)

2。谓词逻辑,是为了解决命题逻辑的局限性

(包括谓词表达语句、谓词演算公式、函数符号;

谓词公式三个集合、语言的项、谓词公式语法树、自由变量和约束变量、代换;量词的等价;

谓词逻辑的语意、语意推导、语意相等;

谓词逻辑公式的不可判定性;

谓词逻辑的表达能力、一阶谓词逻辑、存在二阶逻辑、全称二阶逻辑)

3。如果有时间,稍微说一下形式验证。

(包括模型检测;

时态逻辑、线性时态逻辑、计算树逻辑;

迁移系统、有向图表示、路径;

线性时态逻辑间的等价、连接词集)

如果你对这些概念很熟悉或者完全不感兴趣,请掠过;否则敬请期待随后的文章。

 

推荐的参考资料有:

1。 面向计算机科学的数理逻辑(第二版) 陆钟万   科学出版社 2002 1

 

2。Logic in Computer Science: Modelling and Reasoning about System,Second Edition,  Michael Huth and Mark Ryan,  Originally Published by Cambridge University Press in 2004.

 

3。Logic for Mathematicians(Revised Edition), A. G. Hamilton,  Originally Published by Cambridge University Press in 1978(1988).

 

 

 

目录
相关文章
|
传感器 数据采集 物联网
Zigbee 控制节点数据收发流程|学习笔记
快速学习Zigbee 控制节点数据收发流程
Zigbee 控制节点数据收发流程|学习笔记
|
数据可视化 定位技术 Python
基于ArcMap的精美地图可视化绘制--以各省GDP数据为例
大家好,我是志斌~ 今天手把手教大家如何用ArcMap 10.3画分级地图。
2336 0
基于ArcMap的精美地图可视化绘制--以各省GDP数据为例
|
数据可视化 计算机视觉
ICCV2021 | TOOD:任务对齐的单阶段目标检测
单阶段目标检测通常通过优化目标分类和定位两个子任务来实现,使用具有两个平行分支的头部,这可能会导致两个任务之间的预测出现一定程度的空间错位。本文提出了一种任务对齐的一阶段目标检测(TOOD),它以基于学习的方式显式地对齐这两个任务。
ICCV2021 | TOOD:任务对齐的单阶段目标检测
|
关系型数据库 分布式数据库 PolarDB
[PolarDB实操课] 02.使用云起实验室资源快速体验PolarDB分布式版
本次课程由阿里云PolarDB开源架构师黄心雨分享,重点介绍如何使用云起实验室资源快速体验PolarDB分布式版。主要内容包括: 1. **PolarDB-X的四种安装方法**:Docker、PXD工具、Kubernetes和源码编译。 2. **容器技术简介**:解释容器在云原生环境中的作用,解决代码跨环境迁移问题。 3. **云起实验室实操**:通过云起实验室提供的零门槛平台,快速部署PolarDB-X,体验其主要功能。 4. **课程小结**:总结PolarDB-X的安装方式及实际操作步骤,并展望后续课程内容。
170 0
|
8月前
|
人工智能 JavaScript 前端开发
【CodeBuddy】三分钟开发一个实用小功能之:3D旋转相册
通过CodeBuddy,用自然语言描述需求即可快速实现炫酷3D相册。本文展示了从零开始构建一个可旋转的6面3D相册的过程:AI自动生成HTML骨架、CSS样式及JS交互逻辑,甚至优化性能与修复问题。无需代码基础,仅需明确需求,AI便能将想法变为现实。最终效果支持鼠标拖拽旋转、触摸操作及图片预览放大,完整代码附于文末。这一体验凸显了AI编程工具在降低技术门槛、提升开发效率方面的巨大潜力,让开发者专注于创意本身。
249 2
【CodeBuddy】三分钟开发一个实用小功能之:3D旋转相册
|
前端开发 UED SEO
HTML基础-链接与图片插入:网页的连接与视觉元素
【6月更文挑战第2天】本文介绍了HTML中`<a>`和`<img>`标签的使用,包括链接的基本结构、目标类型以及图片的插入、尺寸调整和对齐方式。常见问题涉及链接和图片路径、缺失`alt`属性及尺寸不匹配,解决方案包括正确引用资源、使用绝对URL和重视`alt`属性。通过示例代码,展示了创建链接和图片的方法,强调了提升网页用户体验的重要性。
576 3
|
移动开发 前端开发 JavaScript
鸿蒙-webview的使用和JS交互(附源码)
日常我们在开发项目时,为了项目快速的开发和迭代,难免会用到H5页面。使用鸿蒙进行项目开发时,也一样免不了要加载H5页面,在移动开发中打开H5页面需要使用WebView组件。同时,为了和H5页面进行数据交换,有时候还需要借助JSBridge来实现客户端与H5之间的通讯。 那么鸿蒙之中用到的技术是什么呢?WebView 在此之前,先看一个报错 ​ App Launch: The Huawei Lite Simulator supports only Lite projects.
946 0
鸿蒙-webview的使用和JS交互(附源码)
开发者说:Sentinel 流控功能在 SpringMVC/SpringBoot 上的实践
从用户的视角来感受一个开源项目的成长,是我们推出「开发者说」专栏的初衷,即在开发者进行开源项目选型时,提供更为立体的项目信息。专栏所有内容均来自作者原创/投稿,本文是「开发者说」的第6篇,作者 Jason Joo,@友乐活(北京),Sentinel Committer.
24849 89
|
弹性计算
阿里云服务器带宽升级收费价格?带宽升级方法
阿里云服务器公网带宽升级怎么收费?阿里云1M带宽价格是23元1个月,2M带宽价格是46元一个月,按流量收费带宽价格是0.8元每GB
1102 0
阿里云服务器带宽升级收费价格?带宽升级方法