一阶逻辑中的几个反直觉结论
最近的Research牵涉到一些时态逻辑的东西,但推式子的时候反而发现一些很简单的一阶逻辑结论之前都没注意到,感觉自己白学了。 首先是这个 $$(\exists x. P(x)) \to Q \iff \forall x.P(x) \to Q$$ 很奇怪,为什么“任意”放进括号里就变成“存在”了呢?其实这也很好…
2,463 2023-12-03 去围观![How Cairo Virtual Machine delegates contract function invocations internally http://dofy.top/wp-content/uploads/2023/12/cairo.png](http://dofy.top/wp-content/uploads/2023/12/cairo.png)
Cairo Compiler Learning Notes
Excerpts from How Cairo Works Introduction to Cairo Registers ap: allocation pointer fp: frame pointer pc: program counter Basic instructions [fp - 1] = [ap - 2] + [fp + 4] [ap - 1] = [fp + 10] * [ap]; ap++ [ap - 1] = [fp + 10] + 12345; ap++ #…
3,703 2022-06-02 去围观Rosette Learning Notes
Excerpts from The Rosette Guide. Rosette Essentials Symbolic Values (define-symbolic b boolean?) Specification (define (check-mid impl lo hi) ; Assuming that (assume (bvsle (int32 0) lo)) ; 0 ≤ lo and (assume (bvsle lo hi)) …
3,369 2022-06-02 去围观![《明清时代江南市镇研究》读书报告 http://dofy.top/wp-content/uploads/2023/12/Ming_Qing.jpeg](http://dofy.top/wp-content/uploads/2023/12/Ming_Qing.jpeg)
Notes of "The Logic of Computer Programming"
Link: The Logic of Computer Programming Four aspect: correctness termination transformation development Program A: Partial Correctness totally correct: if we execute Program A on any input satisfying the input assertion, the program will ha…
4,871 2021-11-13 去围观