No.216
I'm really sorry about textboard.org but Bitdiddle said the stress tests were badly needed and kept encouraging me. I hope it's back up soon.
No.217
>>216It seems to have returned from death.
…
Why are you testing in production?
No.257
Currently implementing truth tables for propositional logic in Python. I am aiming to make it general enough so that I can represent every possible table (not just AND, XOR and the usual) with any number of truth-values.
Fun fact: if you have V truth values, then the number of possible truth tables for a binary connective (a truth table with two inputs, basically) is: V ^ (V ^ 2).
This number gets very big very quickly:
V - V ^ (V ^ 2)
1 - 1
2 - 16
3 - 19683
4 - 4294967296 (4.3 billion)
5 - 298023223876953125 (298 quadrillion)
No.258
>>257>with any number of truth-valuesWhat are you going to use for not(not(x))?
No.261
>>258Aha. My impression is that NOT(NOT(p)) has the same truth value as p in most many-valued logics, especially those with a finite number of truth values. The Wikipedia article will give some examples:
https://en.wikipedia.org/wiki/Many-valued_logicThe program I'm writing won't be able to handle intuitionistic logic, where NOT(NOT(p)) =/= p, because intuitionistic logic does not use truth tables. At least, it doesn't use finite ones.
No.286
I am giving Coq another go, this time using
Programs and Proofs:
https://ilyasergey.net/pnp/I expect to lose track of what is going on somewhere around the middle of the third chapter.
No.287
>Coq
>Lego
>Isabelle
You forgot to add TypeScript.
No.291
>>287What do you mean? If this is a joke, I don't get it.
No.292
>>291It is. You'll get it when you're older.
No.302
>>286As expected, it was progressing a bit too fast for me. Before continuing on to chapter 4, I am reading this tutorial:
https://mdnahas.github.io/doc/nahas_tutorialI like that it uses only the most basic parts of Coq and explains them in terms of the Curry-Howard correspondence. It makes me want to write my own proof assistant!
No.315
Is there a better way to repeatedly destruct a hypothesis so that it can be handled in one go like here?
Goal forall n, n = 0 \/ n = 1 \/ n = 2 \/ n = 3 -> n - 3 = 0.
intros n Cs.
destruct Cs as [C|Cs]; try destruct Cs as [C|Cs]; try destruct Cs as [C|C];
rewrite C;
reflexivity.
Qed.
I guess "repeat" would kind of work, except for the last one where the naming wouldn't match.
No.321
>>286I finished this. I liked it a lot, although the last chapter maybe progressed a bit too quickly, I ended skipping most of the exercises there. Maybe I will return to it someday.
Should I continue with Software Foundations or should I try The Little Prover before it?
No.324
OK, it's back up.
>>323>What are you working on, textboard engineering?Nothing so lofty. I'm just contributing in my small way to the SchemeBBS community by providing bugfixes.
No.325
>>321Wow I thought
The Little Schemer will be some quick enjoyable read, but it is quite laborious. It took me a while to figure out how to follow along with the code as the instructions are not very user-friendly. I use "J-Bob/step" for the actual proving and only copy it into the proper "J-Bob/define" once it is done. It is pretty fun though and I am looking forward to reading the actual implementation too. It is just a bit too manual after Coq, you have to type a lot!
No.328
>>325I finished it but I am not satisfied. It could have had more examples on the main techniques, like how to construct the totality claims and such. It did not feel like by the end I understood the main principles, if there were any.
No.331
>>330Nice little website, good job!
No.333
The SchemeBBS "fossil repositories" link gives
https://fossil.textboard.org/502 Bad Gateway
nginx/1.18.0
Posting in the sandbox gives
https://textboard.org/sandbox/1error 502
bad gateway
Anyone else seeing this?
No.334
>>333Nice repeating digits. Yes, for me everything dynamic gives 502 error, even viewing individual posts like here:
https://textboard.org/sandbox/1/1