How did you open it? Sometimes you can't just double click but have to right-click the app and choose "Open" in the menu, and then again "Open" in the confirmation dialog. I think this is only needed once and then it works normally. Unfortunately I don't have access to a Mac anymore so I can't verify.
No, this is propositional logic only. I have plans for adding first order logic (likely as a separate game as it would probably need some bigger UI changes) too but haven't had time to do it yet
Loved the demo! Would really love to get a function to copypaste the deduction tree you already have, like if you proved in the left subbranch that the statement D is true, you could just drag over the same reasoning tree to the right branch if it is needed, like in the last level of the demo
Thanks! Yeah, such a function could be useful in some places but I think in *most* cases you can find a shorter sub-proof so that it's easy to copy manually ;) I'll keep it in mind for a possible future extension/v2 though!
I agree, but what would be more useful is instead of copy-pasting the same thing everywhere, you write it once and you can reuse it like a function. This will require it to be able to be extracted as a separate tree and then be referenced when needed.
Do you mean essentially like a custom "rule" (lemma) which you could then use like an ordinary rule wherever it fits? So basically a kind of template instead of a plain copy.
Yeah, could be thought of like that. A template being a custom combination of rules that you can use like a normal rule.
Here i use P from P^Q and then Q from P^Q, but instead of using this twice, i would make a template with both rules and it will then say Q from (P^Q)^R. It could be a big technical hurdle to make it work correctly though, or it may end up being easy using the already existing way to create trees from rules, just replacing A, B, C with P, Q, R.
And now that i think about it, functions/templates could be very useful if made persistent.
For example i want to more easily say that things are commutative. I create a new template Q^P from P^Q. Now i can reuse this custom template everywhere like a rule.
A simple solution for persintence could be that every level (at least the named ones), after solved, becomes a new rule you can use. Need some way of organizing so you can easily find them, though. If/when I add first order logic I think something like this would be very useful or the proofs might get very long.
You're right, I even had it at some point but decided to remove it to simplify the UI since not many levels seemed to need it. But you're not the first one to comment about it so maybe I was wrong...
I love backwards solving the “crab” way, but it is also very useful to solve forward. Maybe you could dynamically hide the forward-solving elements of the UI if the level doesn’t need it, but also let the player take control over it just in case i want to do something you didn’t expect.
The full version does not include: <-> (implies and vise versa) -/> (does not imply) <- </- Extra proofs: A, A -/> B | not B A, A <-> B | B not A, A <-> B | not B
Thanks for the comment! I indeed dropped equivalence (<->) because I thought it would clutter the UI without bringing interesting new mechanics. Maybe I'll include it in a future version, though. I'll also add your proof suggestions to a list of possible future additions!
More proofs: A <-> B | A -> B, B -> A A -> B | A -/> not B A -/> B | A -> not B not not A | B A -> B | B -> A A <-> B | A -> B, B -> A A and B | A <-> B not A and not B | A <-> B A <-> B | A and B or not A and not B not A <-> B | not A and B or A and not B Level ideas: 1. Premise: A -/> B Prove: A -> not B 2. Premises: A -> B, B -/> C Prove: A -> not C 3. Premise: A -/> not B Prove: A -> B 4. Premise: A <-> B Prove: A -> B and B -> A 5. Premise: A and B Prove: not(A -/> B) 6. Prove: (not A) -/> A 7. Prove: (A and A-/> B) -> (A <-> B)
← Return to game
Comments
Log in with itch.io to leave a comment.
I just bought the full game (mac) and it said the file is damaged. Any solutions, nonpop?
How did you open it? Sometimes you can't just double click but have to right-click the app and choose "Open" in the menu, and then again "Open" in the confirmation dialog. I think this is only needed once and then it works normally. Unfortunately I don't have access to a Mac anymore so I can't verify.
There's no confirmation dialogue, it just says that the file is broken and should be moved to the trash. Is your game perhaps running on 32x?
I believe it's 64-bit if that's what you mean. Can you try these steps?
Thanks very much. This helped! :)
I really enjoyed the demo! It took me a few rounds to get the hang of it, but once I did it was really fun!
Good to hear, thanks!
Is first order logic included in the later levels?
No, this is propositional logic only. I have plans for adding first order logic (likely as a separate game as it would probably need some bigger UI changes) too but haven't had time to do it yet
Loved the demo! Would really love to get a function to copypaste the deduction tree you already have, like if you proved in the left subbranch that the statement D is true, you could just drag over the same reasoning tree to the right branch if it is needed, like in the last level of the demo
Thanks! Yeah, such a function could be useful in some places but I think in *most* cases you can find a shorter sub-proof so that it's easy to copy manually ;) I'll keep it in mind for a possible future extension/v2 though!
I agree, but what would be more useful is instead of copy-pasting the same thing everywhere, you write it once and you can reuse it like a function. This will require it to be able to be extracted as a separate tree and then be referenced when needed.
Do you mean essentially like a custom "rule" (lemma) which you could then use like an ordinary rule wherever it fits? So basically a kind of template instead of a plain copy.
Yeah, could be thought of like that. A template being a custom combination of rules that you can use like a normal rule.
Here i use
P from P^Qand thenQ from P^Q, but instead of using this twice, i would make a template with both rules and it will then sayQ from (P^Q)^R. It could be a big technical hurdle to make it work correctly though, or it may end up being easy using the already existing way to create trees from rules, just replacing A, B, C with P, Q, R.And now that i think about it, functions/templates could be very useful if made persistent.
For example i want to more easily say that things are commutative. I create a new template
Q^P from P^Q. Now i can reuse this custom template everywhere like a rule.A simple solution for persintence could be that every level (at least the named ones), after solved, becomes a new rule you can use. Need some way of organizing so you can easily find them, though. If/when I add first order logic I think something like this would be very useful or the proofs might get very long.
Fun game, very repetitive though. Kind of fun to switch you brain off and just play off vibes
Thanks for the comment! Glad you're having fun :)
I don't get it, but i like it
I'll count that as success :)
it would be so convenient if we could also go forward from the premises so we don't have to prove B is true 3 times
You're right, I even had it at some point but decided to remove it to simplify the UI since not many levels seemed to need it. But you're not the first one to comment about it so maybe I was wrong...
I love backwards solving the “crab” way, but it is also very useful to solve forward. Maybe you could dynamically hide the forward-solving elements of the UI if the level doesn’t need it, but also let the player take control over it just in case i want to do something you didn’t expect.
I'll keep this idea in mind 👍
The full version does not include:
<-> (implies and vise versa)
-/> (does not imply)
<-
</-
Extra proofs:
A, A -/> B | not B
A, A <-> B | B
not A, A <-> B | not B
Thanks for the comment! I indeed dropped equivalence (<->) because I thought it would clutter the UI without bringing interesting new mechanics. Maybe I'll include it in a future version, though. I'll also add your proof suggestions to a list of possible future additions!
More proofs: A <-> B | A -> B, B -> A
A -> B | A -/> not B
A -/> B | A -> not B
not not A | B
A -> B | B -> A
A <-> B | A -> B, B -> A
A and B | A <-> B
not A and not B | A <-> B
A <-> B | A and B or not A and not B
not A <-> B | not A and B or A and not B
Level ideas:
1.
Premise: A -/> B
Prove: A -> not B
2.
Premises: A -> B, B -/> C
Prove: A -> not C
3.
Premise: A -/> not B
Prove: A -> B
4.
Premise: A <-> B
Prove: A -> B and B -> A
5.
Premise: A and B
Prove: not(A -/> B)
6.
Prove: (not A) -/> A
7.
Prove: (A and A-/> B) -> (A <-> B)