𝟲
/
𝟛𝟘·
I'm generalizing the way I validate proof steps so inference rules match if any formulae with an equivalent (Sapphire specific) normal form would have matched.
𝟳
/
𝟘𝟚·
This page is a rough (perhaps embarrassingly so) version of a solution to the first puzzle in Raymond M. Smullyan's Satan, Cantor and Infinity
╭
𝟘𝟞·
I now have a somewhat general "pigeonhole solver" which, given a set of equations of the form x_i¬=x_j and for each x_i, one equation of the form x_i∈{c_j c_(j+1)
┊
c_(j+2) ... c_(j+k)}. This can directly be solved with a search, but I've been trying to avoid that in my pretense toward symbolic manipulation. In the end, I'm not
𝔻
┊
sure my approach is all that different than a search - if I can write my approach up in a sensible form, I'll post a doc someplace and hope to learn more.
𝕖
┊
𝕔
┊
𝟚𝟛·
I've added support for the Cartesian Product, represented by ‘×’ in Unicode (U+D7). What I call “tuple constrained quantification” (∀⟨x y⟩∈Z×Z) is accepted in
┊
⟪Sapphire⟫ as well as set exponentiation by an integer (Z^4 ▷ Z×Z×Z×Z) ({1⋯3}^3 ▷ {1⋯3}×{1⋯3}×{1⋯3}). Finite expressions can be evaluated in calculator fashion (⟨1 2
┊
3⟩∈{1⋯3}^3 ▷ ✔) (∀⟨a b⟩∈{1⋯3}^2 a>3 ⇒ a+b>4 ▷ ✔) and can also be symbolically manipulated by ⟪Ag⟫, aka “The Silver Solver”. I've updated my Sudoku rules to use these
╰
new features