This book can be seen either as a text on theorem proving that uses techniques from general algebra, or else as a text on general algebra illustrated and made concrete by practical exercises in theorem proving. The book considers several different logical systems, including first-order logic, Horn clause logic, equational logic, and first-order logic with equality. Similarly, several different proof paradigms are considered. However, we do emphasize equational logic, and for simplicity we use only the OBJ3 software system, though it is used in a rather flexible manner. We do not pursue the lofty goal of mechanizing proofs like those of which mathematicians are justly so proud; instead, we seek to take steps towards providing mechanical assistance for proofs that are useful for computer scientists in developing software and hardware. This more modest goal has the advantage of both being achievable and having practical benefits. The following topics are covered: many-sorted signature, algebra and homomorphism; term algebra and substitution; equation and satisfaction; conditional equations; equational deduction and its completeness; deduction for conditional equations; the theorem of constants; interpretation and equivalence of theories; term rewriting, termination, confluence and normal form; abstract rewrite systems; standard models, abstract data types, initiality, and induction; rewriting and deduction modulo equations; first-order logic, models, and proof planning; second-order algebra; order-sorted algebra and rewriting; modules; unification and completion; and hidden algebra. In parallel with these are a gradual introduction to OBJ3, applications to group theory, various abstract data types (such as number systems, lists, and stacks), propositional calculus, hardware verification, the {\lambda}-calculus, correctness of functional programs, and other topics.


翻译:这本书既可以被视为理论文字,可以证明使用通用代数的计算法,也可以视为一般代数的计算法,在理论证明中以实际练习方式演示和具体化。本书考虑了若干不同的逻辑系统,包括一阶逻辑、合恩条款逻辑、方程逻辑和等序逻辑。同样,也考虑了若干不同的证明范式。然而,为了简单起见,我们只使用OBJ3软件系统,尽管它以相当灵活的方式使用。我们不追求诸如数学家引以为豪的那种普通代数的校正证明的崇高目标;相反,我们寻求采取步骤,为计算机科学家在开发软件和硬件方面有用的证据提供机械协助。这个更小的目标具有既可以实现又具有实际效益的优势。以下主题被覆盖了:许多分解的签名、代数和正态;术语变数和替代;公式和满意度;等式推算及其完整性;对等式公式的推算;对等式公式的推算;对等式;对等式、正序、变数的判和变数。

0
下载
关闭预览

相关内容

ACM/IEEE第23届模型驱动工程语言和系统国际会议,是模型驱动软件和系统工程的首要会议系列,由ACM-SIGSOFT和IEEE-TCSE支持组织。自1998年以来,模型涵盖了建模的各个方面,从语言和方法到工具和应用程序。模特的参加者来自不同的背景,包括研究人员、学者、工程师和工业专业人士。MODELS 2019是一个论坛,参与者可以围绕建模和模型驱动的软件和系统交流前沿研究成果和创新实践经验。今年的版本将为建模社区提供进一步推进建模基础的机会,并在网络物理系统、嵌入式系统、社会技术系统、云计算、大数据、机器学习、安全、开源等新兴领域提出建模的创新应用以及可持续性。 官网链接:http://www.modelsconference.org/
【经典书】线性代数,Linear Algebra,525页pdf
专知会员服务
72+阅读 · 2021年1月29日
Linux导论,Introduction to Linux,96页ppt
专知会员服务
75+阅读 · 2020年7月26日
强化学习最新教程,17页pdf
专知会员服务
166+阅读 · 2019年10月11日
【新书】Python编程基础,669页pdf
专知会员服务
186+阅读 · 2019年10月10日
机器学习入门的经验与建议
专知会员服务
89+阅读 · 2019年10月10日
【哈佛大学商学院课程Fall 2019】机器学习可解释性
专知会员服务
96+阅读 · 2019年10月9日
MIT新书《强化学习与最优控制》
专知会员服务
269+阅读 · 2019年10月9日
计算机 | 入门级EI会议ICVRIS 2019诚邀稿件
Call4Papers
10+阅读 · 2019年6月24日
Unsupervised Learning via Meta-Learning
CreateAMind
41+阅读 · 2019年1月3日
Hierarchical Disentangled Representations
CreateAMind
4+阅读 · 2018年4月15日
已删除
将门创投
4+阅读 · 2018年1月19日
Arxiv
0+阅读 · 2021年3月12日
Vectorial Parameterizations of Pose
Arxiv
0+阅读 · 2021年3月12日
Arxiv
0+阅读 · 2021年3月11日
Arxiv
0+阅读 · 2021年3月11日
Arxiv
0+阅读 · 2021年3月10日
The Measure of Intelligence
Arxiv
6+阅读 · 2019年11月5日
Arxiv
3+阅读 · 2018年12月18日
VIP会员
相关VIP内容
【经典书】线性代数,Linear Algebra,525页pdf
专知会员服务
72+阅读 · 2021年1月29日
Linux导论,Introduction to Linux,96页ppt
专知会员服务
75+阅读 · 2020年7月26日
强化学习最新教程,17页pdf
专知会员服务
166+阅读 · 2019年10月11日
【新书】Python编程基础,669页pdf
专知会员服务
186+阅读 · 2019年10月10日
机器学习入门的经验与建议
专知会员服务
89+阅读 · 2019年10月10日
【哈佛大学商学院课程Fall 2019】机器学习可解释性
专知会员服务
96+阅读 · 2019年10月9日
MIT新书《强化学习与最优控制》
专知会员服务
269+阅读 · 2019年10月9日
相关资讯
计算机 | 入门级EI会议ICVRIS 2019诚邀稿件
Call4Papers
10+阅读 · 2019年6月24日
Unsupervised Learning via Meta-Learning
CreateAMind
41+阅读 · 2019年1月3日
Hierarchical Disentangled Representations
CreateAMind
4+阅读 · 2018年4月15日
已删除
将门创投
4+阅读 · 2018年1月19日
相关论文
Arxiv
0+阅读 · 2021年3月12日
Vectorial Parameterizations of Pose
Arxiv
0+阅读 · 2021年3月12日
Arxiv
0+阅读 · 2021年3月11日
Arxiv
0+阅读 · 2021年3月11日
Arxiv
0+阅读 · 2021年3月10日
The Measure of Intelligence
Arxiv
6+阅读 · 2019年11月5日
Arxiv
3+阅读 · 2018年12月18日
Top
微信扫码咨询专知VIP会员