1. Forum
  2. USENET
  3. comp.lang.prolog

  • When halt provers are allowed to reject bad inputs the remaining domain is decidable

    From olcott@polcott333@gmail.com to comp.theory,sci.logic,sci.math,comp.lang.prolog,comp.ai.philosophy on Wed Feb 4 10:47:50 2026
    From Newsgroup: comp.lang.prolog


    A halt prover attempts to prove halting 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.

    *Halting Problem and Proof Theoretic Semantics* https://www.researchgate.net/publication/400341134_Halting_Problem_and_Proof_Theoretic_Semantics


    This change makes
    "true on the basis of meaning expressed in language"
    reliably computable for the entire body of knowledge.
    --
    Copyright 2026 Olcott<br><br>

    My 28 year goal has been to make <br>
    "true on the basis of meaning expressed in language"<br>
    reliably computable for the entire body of knowledge.<br><br>

    This required establishing a new foundation<br>

    --- Synchronet 3.21b-Linux NewsLink 1.2
  • From Richard Damon@Richard@Damon-Family.org to comp.theory,sci.logic,sci.math,comp.lang.prolog,comp.ai.philosophy on Wed Feb 4 21:34:57 2026
    From Newsgroup: comp.lang.prolog

    On 2/4/26 11:47 AM, olcott wrote:

    A halt prover attempts to prove halting and when it
    detects that the proof of its input does not form

    *a well-founded justification tree within Proof*
    *theoretic semantics*

    But Programs are not based on a "justification tree", so your definition
    is just meaningles.


    Then it is correct to reject this input as bad data.

    No, it it correct to reject you concept as just a category error



    *Halting Problem and Proof Theoretic Semantics*
    https://www.researchgate.net/ publication/400341134_Halting_Problem_and_Proof_Theoretic_Semantics


    This change makes
    "true on the basis of meaning expressed in language"
    reliably computable for the entire body of knowledge.



    Since your input just isn't a valid program. as it is incomplete, all
    you are doing is proving your own stupidity.

    It seems you just fundamentally don't understand that yoy neec to know
    what you are talking about and use language properly.

    This is what has made you just an ignorant pathological liar.
    --- Synchronet 3.21b-Linux NewsLink 1.2
  • From Mikko@mikko.levanto@iki.fi to comp.theory,sci.logic,sci.math,comp.lang.prolog,comp.ai.philosophy on Thu Feb 5 12:45:28 2026
    From Newsgroup: comp.lang.prolog

    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
    --- Synchronet 3.21b-Linux NewsLink 1.2