定理证明器背后的数学原理

最近由于有同学要用到,我也跟着学了一下 Lean,之前也看过一点 coq (不过讲真的语法丑拒,虽然 Lean 也丑),所以说到底这类定理证明辅助软件背后的数学原理是怎么样的呢?

midi 文件转蜂鸣器乐谱

midi 文件转蜂鸣器乐谱工具

交流电基础

在我的教育经历里面就没有交流电这回事,但是这个东西其实非常重要,真不知道我受的是什么教育……

电阻阻值为什么这么奇怪

电阻阻值为什么这么奇怪,以及配出你要的阻值的工具

Contention-Aware Lock Scheduling 和 (b)LDSF 算法

MySQL 8.0.3 引入了 LDSF 事务调度算法,这是一种竞争感知调度算法,本文结合原论文介绍了这个算法。

Mitchell Merritt 分布式死锁检测算法

本文介绍了 Mitchell Merritt 分布式死锁检测算法。

自动机理论 • 有限状态机

本章介绍最为常见的有限状态机以及其可以识别的语言类——正规语言。

自动机理论 • 基本概念

本文搜集了自动机理论中的一点基本概念,以备后续学习过程中参考。

重新开始学数学 • 数理逻辑(3)

欲练PLT神功,必先学好数学,而其中最重要的一个分支即为数理逻辑。现在我在看 LOGIC IN COMPUTER SCIENCE 来重新学习离散数学里学过一丁点的数理逻辑……本章记录数理逻辑中 model 和相关概念的定义

自动逻辑综合原理 • 组合逻辑与 LUT 的最简单的综合

看到有人单枪匹马写 Verilog 综合器我真的羡慕了,于是我稍微探索了下自动逻辑综合的原理。