home bbs files messages ]

Forums before death by AOL, social media and spammers... "We can't have nice things"

   sci.logic      Logic -- math, philosophy & computationa      262,912 messages   

[   << oldest   |   < older   |   list   |   newer >   |   newest >>   ]

   Message 262,807 of 262,912   
   Mikko to olcott   
   Re: When halt provers are allowed to rej   
   05 Feb 26 12:45:28   
   
   XPost: comp.theory, sci.math, comp.lang.prolog   
   XPost: comp.ai.philosophy   
   From: mikko.levanto@iki.fi   
      
   On 04/02/2026 18:47, olcott wrote:   
      
   > A halt prover attempts to prove halting   
      
   To prove that a computation halts is simple. Just show the execution   
   trace from the start to the halting. The hard problem is to prove   
   that an execution does not halt.   
      
   > and when it detects that the proof of its input does not form   
   >   
   > *a well-founded justification tree within Proof*   
   > *theoretic semantics*   
   >   
   > Then it is correct to reject this input as bad data.   
      
   No, that does not follow. That only means that it is correct to reject   
   the proof. The conclusion of the proof may still be correct.   
      
   --   
   Mikko   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)   

[   << oldest   |   < older   |   list   |   newer >   |   newest >>   ]


(c) 1994,  bbs@darkrealms.ca