- Edward Latimore
- Paul Phillips
- Dana Scott
;; See | |
;; http://takeonrules.com/2021/08/22/ever-further-refinements-of-org-roam-usage/ | |
;; for details on this configuration. | |
;; | |
;; See https://takeonrules.com/2021/08/23/diving-into-the-implementation-of-subject-menus-for-org-roam/ | |
;; for a walk through of the implementation. | |
;; | |
;; A Property List of my `org-roam' capture templates. | |
(setq jnf/org-roam-capture-templates-plist | |
(list |
(ns firstshot.chessknightmove | |
(:refer-clojure :exclude [== >= <= > < =]) | |
(:use clojure.core.logic | |
clojure.core.logic.arithmetic)) | |
(defn knight-moves | |
"Returns the available moves for a knight (on a 8x8 grid) given its current position." | |
[x y] | |
(let [xmax 8 ymax 8] | |
(run* [q] |
Please see “Strongly-normalising agents” for a follow-up.
Throughout much of MIRI research work, there is an underlying assumption that a consistent system cannot prove its own consistency.
While it is usually acknowledged that the above assumption applies only to systems as strong as Peano Arithmetic (PA), it is done only in passing, with little consideration for the possibility of using other systems. Girard’s system F appears merely as a footnote, while Willard’s self-verifying systems merit just a brief mention. (YH2013, pp.6,9,18; F2013a, p.1; F2013b, p.1; FS2014, pp.3; FS2015, p.4b)