XPost: comp.theory, sci.logic, sci.math   
   XPost: comp.lang.prolog   
   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)