Jaakko Hintikka’s (?) conception of propositional #logic in terms of a game between the “verifier,” who owns the disjunctions, and the “falsifier”, who owns the conjunctions.
on 02026-01-06#Kripke semantics may be the #logic I need for #Jaakko or other incarnations of “principled #APL”. #array-languages
on 02026-01-06#Kripke’s “Semantical Considerations on Modal #Logic”, archived from the Saul Kripke Center website.
on 02026-01-06Kevin Buzzard’s #LEAN blog for the "Xena Project" to formalize mathematics in L∃∀N #logic, starting to take up #AI
on 02025-11-05#Harmonic is hiring part-time #LEAN 4 experts. #AI #logic
on 02025-11-05#Harmonic still says, “We are forging the world’s most advanced mathematical reasoning engine.” #logic #AI
on 02025-11-05Tudor Achim’s #AI startup "Harmonic" provides #logic proofs
on 02025-11-05“"Kripke" is the governance infrastructure for AGI. Fast. Provable. Auditable.” #AI startup: “Kripke empowers humanity, to specify, monitor, and guarantee what intelligent systems must (and must not) do. From winning through AI to ensuring compliance with regulatory frameworks, Kripke guarantees it with infrastructure designed to codify, enforce, and audit AI behavior to ensure aligned outcomes across any domain.” #logic #startups
on 02025-11-05Hammack's #ebook "Book of Proof" has been approved by the American Institute of Mathematics' Open Textbook Initiative. #logic #math
on 02023-06-17literate-programming #ebook developing the proof assistant "Proust" in Racket, apparently written for teaching Waterloo's Logic and Computation course, with an overview of propositional and predicate #logic, as well as #Coq and #Agda. #cc by-nc-sa
on 02021-02-09A #PDF chapter on finite-domain constraint #logic programming in #Prolog, including #optimization problems, with examples like cryptarithms and Hamiltonian cycle optimization. #toread
on 02016-10-11A bunch of stuff I don’t understand about #logic and #computability in the context of competing AI agents that are able to examine each other’s code and compute things about it. Refers to a bunch of SIAI stuff like “Kripke frames” and “modal combat” that I know nothing about, as well as stuff like Löb’s Theorem that I know a little bit about.
on 02016-09-23Adding call/cc to Haskell converts its #type-system from being a model of classical #logic to being a model of #intuitionistic-logic
on 02016-06-22"The Markable Mark": an #ebook on Laws of Form #logic
on 02016-06-05A draft #PDF #ebook on Laws of Form, covering a bunch of advanced topics in #logic.
on 02016-06-05The Martelli and Montanari unification algorithm, which seems to be the one of the various unification #algorithms that everyone uses for #logic. This original #paper #pdf is 25 pages and clearer than most of the attempts at exegesis that I’ve seen.
on 02016-05-093773 of the 19383 two-input ternary #logic gates are universal; the proportion of universal N-ary two-input gates goes to 1/e as N→∞.
on 02015-08-13A 2014 discussion about #reactive programming with #Facebook’s React and how it relates to #incremental computation and #FRP and #temporal #logic. Neel Krishnaswami (#neelk) links his paper on “higher-order reactive programming without spacetime leaks”.
on 02015-08-10Wadler explains the #Curry-Howard isomorphism, with a #logic #tutorial into the bargain #formalmethods
on 02015-08-05