[HN Gopher] Natural Deduction in Logic (2015)
       ___________________________________________________________________
        
       Natural Deduction in Logic (2015)
        
       Author : Rexxar
       Score  : 9 points
       Date   : 2024-01-11 12:50 UTC (10 hours ago)
        
 (HTM) web link (profs.info.uaic.ro)
 (TXT) w3m dump (profs.info.uaic.ro)
        
       | mcphage wrote:
       | Is there any instructions on how to use this, or what is being
       | asked for?
        
         | abeppu wrote:
         | The 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 wrote:
           | It 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 p) [rule 5]. Current goal becomes
           | (?s and p)
           | 
           | 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/
        
       ___________________________________________________________________
       (page generated 2024-01-11 23:01 UTC)