Proof editor now shows you the proof tree you're building as you type proof commands https://personal.cis.strath.ac.uk/robert.atkey/cs208/2019/nd/natural-deduction.html …pic.twitter.com/WCwj8ohPSN
-
That's a very cool piece of work. I could have done with that a long time ago in lots of different contexts.
Thanks! You might enjoy the coursework I'm getting the students to do with it: https://personal.cis.strath.ac.uk/robert.atkey/cs208/2019/cw2/assessment.html …
-
-
Is there an issue with "Evaluating Programs" parts 5 and 6? (can't click "apply Mul" or "Select rule" for 1 \Downarrow 3 for these two parts)pic.twitter.com/yJ0o4YcxF9
-
You're trying to prove that (-10) * 10 evaluates to 0, and Mul won't let you. Similarly, there is no rule that lets you evaluate 1 to 3. Hint: you needed to choose 'IfFalse' when evaluating the 'if'.
- Još 7 drugih odgovora
Novi razgovor -
-
-
that is absolutely a fantastic piece of kit!pic.twitter.com/kzEyIkxjkp
Hvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi
-
-
-
Very nice examples/test! I taught natural deduction for years but with proofs by hand. I looked at Rod Burstall's LEGO system but it was a bit unwieldy. I also taught formal semantics and buckets of lambda calculus. Your system would have been great for all these.
Hvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi
-
Čini se da učitavanje traje već neko vrijeme.
Twitter je možda preopterećen ili ima kratkotrajnih poteškoća u radu. Pokušajte ponovno ili potražite dodatne informacije u odjeljku Status Twittera.