In general, providing an axiomatization for an arbitrary logic is a task that may require some ingenuity. In the case of logics defined by a finite logical matrix (three-valued logics being a particularly simple example), the generation of suitable finite axiomatizations can be completely automatized, essentially by expressing the matrix tables via inference rules. In this chapter we illustrate how two formalisms, the 3-labelled calculi of Baaz, Ferm\"uller and Zach and the multiple-conclusion (or Set-Set) Hilbert-style calculi of Shoesmith and Smiley, may be uniformly employed to axiomatize logics defined by a three-valued logical matrix. The generating procedure common to both formalisms can be described as follows: first (i) convert the matrix semantics into rule form (we refer to this step as the generating subprocedure) and then (ii) simplify the set of rules thus obtained, essentially relying on the defining properties of any Tarskian consequence relation (we refer to this step as the streamlining subprocedure). We illustrate through some examples that, if a minimal expressiveness assumption is met (namely, if the matrix defining the logic is monadic), then it is straightforward to define effective translations guaranteeing the equivalence between the 3-labelled and the Set-Set approach.


翻译:一般而言,为任意逻辑提供公理化系统需要一定程度的创造性。对于由有限逻辑矩阵定义的逻辑(其中三值逻辑是一个特别简单的例子),可完全自动化地生成合适的有限公理化系统,其本质是通过推理规则表达矩阵真值表。本章将阐述如何统一运用两种形式化框架——Baaz、Fermüller和Zach的三标记演算,以及Shoesmith与Smiley的多结论(或称集-集)希尔伯特式演算——来公理化由三值逻辑矩阵定义的逻辑系统。这两种框架共有的生成程序可描述如下:首先(i)将矩阵语义转换为规则形式(此步骤称为生成子程序),然后(ii)主要依据任意塔尔斯基后承关系的定义性质简化所获得的规则集(此步骤称为精简子程序)。通过若干实例将说明,在满足最小可表达性假设(即定义逻辑的矩阵是单一的)的前提下,可轻松定义有效的转换,从而保证三标记方法与集-集方法之间的等价性。

0
下载
关闭预览

相关内容

牛津大学最新《计算代数拓扑》笔记书,107页pdf
专知会员服务
44+阅读 · 2022年2月17日
【ACL2020】多模态信息抽取,365页ppt
专知会员服务
151+阅读 · 2020年7月6日
自动结构变分推理,Automatic structured variational inference
专知会员服务
41+阅读 · 2020年2月10日
【SIGGRAPH2019】TensorFlow 2.0深度学习计算机图形学应用
专知会员服务
41+阅读 · 2019年10月9日
学习自然语言处理路线图
专知会员服务
140+阅读 · 2019年9月24日
RL解决'BipedalWalkerHardcore-v2' (SOTA)
CreateAMind
31+阅读 · 2019年7月17日
meta learning 17年:MAML SNAIL
CreateAMind
11+阅读 · 2019年1月2日
利用动态深度学习预测金融时间序列基于Python
量化投资与机器学习
18+阅读 · 2018年10月30日
disentangled-representation-papers
CreateAMind
26+阅读 · 2018年9月12日
概率图模型体系:HMM、MEMM、CRF
机器学习研究会
30+阅读 · 2018年2月10日
Layer Normalization原理及其TensorFlow实现
深度学习每日摘要
32+阅读 · 2017年6月17日
基于LDA的主题模型实践(三)
机器学习深度学习实战原创交流
23+阅读 · 2015年10月12日
国家自然科学基金
2+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
2+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
6+阅读 · 2014年12月31日
VIP会员
最新内容
超越网格:作战环境对炮兵的影响
专知会员服务
2+阅读 · 5月31日
BES:让语言模型通过双向进化搜索自我改进
专知会员服务
5+阅读 · 5月30日
以色列-美国-伊朗战争中的无人机:关键要点
专知会员服务
4+阅读 · 5月30日
《Palantir任务保障性软件安全标准(MA-S2)》
专知会员服务
17+阅读 · 5月30日
基于声学的无人机检测技术综述
专知会员服务
8+阅读 · 5月30日
《当代混合战争分析框架:俄乌战争经验教训》
相关资讯
RL解决'BipedalWalkerHardcore-v2' (SOTA)
CreateAMind
31+阅读 · 2019年7月17日
meta learning 17年:MAML SNAIL
CreateAMind
11+阅读 · 2019年1月2日
利用动态深度学习预测金融时间序列基于Python
量化投资与机器学习
18+阅读 · 2018年10月30日
disentangled-representation-papers
CreateAMind
26+阅读 · 2018年9月12日
概率图模型体系:HMM、MEMM、CRF
机器学习研究会
30+阅读 · 2018年2月10日
Layer Normalization原理及其TensorFlow实现
深度学习每日摘要
32+阅读 · 2017年6月17日
基于LDA的主题模型实践(三)
机器学习深度学习实战原创交流
23+阅读 · 2015年10月12日
相关基金
国家自然科学基金
2+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
2+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
6+阅读 · 2014年12月31日
Top
微信扫码咨询专知VIP会员