Comment Comment by qrobit It is very much like interactive theorem proving(like LEAN[1])yellow blocks on top are your premisesteal 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 q2) 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 goal5) congratulation![1] https://lean-lang.org/ parent qrobit 2 years ago
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/