4 ms·
Natural Deduction in Logic (2015)
- mcphage 3y agoIs there any instructions on how to use this, or what is being asked for?
- abeppu 3y agoThe top block gives some premises and a conclusion which we're meant to prove. The smaller blocks on the bottom are inference rules which can be used in the proof. I haven't figured out what the colors mean. I think there's also some kind of cursor/state, which I don't understand -- but when you click a rule, I don't understand how you control which expression matches to which term in the rule.
- qrobit 3y agoIt is very much like interactive theorem proving(like LEAN[1]) yellow blocks on top are your premises teal and dark-red blocks on the bottom of the solution-block are your goals(dark red block is your current goal, to which you apply rules) First level can be solved in the following way: 1) replace conjunction (q and r) with q, r[rule 3]. Current goal becomes q 2) replace q with (?s and q) [rule 5]. Current goal becomes (?s and q) 3) apply your premise (p and q) to solve current goal (goal becomes r) 4) apply your premise (r) to solve current goal 5) congratulation! [1] https://lean-lang.org/ https://lean-lang.org/
- kozd 3y agoA big problem is it's practically unusable on mobile (at least for me) Clicking once via finger tap often results in multiple clicks being applied.
- techtangents2 3y agohttps://incredible.pm/ https://incredible.pm/ is better