[HN Gopher] The Foundation of a Generic Theorem Prover (1989) [pdf]
       ___________________________________________________________________
        
       The Foundation of a Generic Theorem Prover (1989) [pdf]
        
       Author : 082349872349872
       Score  : 45 points
       Date   : 2024-05-10 07:41 UTC (1 days ago)
        
 (HTM) web link (arxiv.org)
 (TXT) w3m dump (arxiv.org)
        
       | i_don_t_know wrote:
       | See also "Designing a Theorem Prover"
       | https://arxiv.org/pdf/cs/9301110
       | 
       | And chapter 10 of ML for the working programmer, freely available
       | at https://www.cl.cam.ac.uk/~lp15/MLbook/pub-details.html
        
       | zermelo44 wrote:
       | Great paper for exploring the foundations of Isabelle. It's a
       | shame the rest of the literature needed to properly understand
       | Isabelle is scattered amongst many papers.
        
         | timmg wrote:
         | Any suggestions for those papers?
        
       | hackandthink wrote:
       | What are the limits of a generic implementation?
       | 
       | The individual object calculi are already complicated, when does
       | the meta-logic reach its limits?
        
       ___________________________________________________________________
       (page generated 2024-05-11 23:00 UTC)