Re: Some Simple Questions

stephen_at_nomail.com
Date: 03/23/05 

Date: 23 Mar 2005 18:25:15 GMT

In sci.math Charlie-Boo <chvol@aol.com> wrote:

: step...@nomail.com wrote:

:> If you download nqthm you can find the entire input to
:> the theorem prover for the proof of the unsolvability of
:> the halting problem in in examples/basic/unsolv.events
:>
:> You can build the theorem prover, and then run it
:> and see the output it produces that shows how it
:> proves the unsolveability of the halting problem.
:> It produces many pages of output. The justifications
:> for each step are often quite wordy. An example is:
:> Linear arithmetic and the lemmas CDR-LESSP, CAR-LESSP, and
: UNPACK-LESSP
:> can be used to show that the measure (COUNT X) decreases according
: to the
:> well-founded relation LESSP in each recursive call. Hence, SEXP is

:> accepted under the principle of definition. Note that:
:> (OR (FALSEP (SEXP X))
:> (TRUEP (SEXP X)))
:> is a theorem.
:>
:> Of course if anyone was really interested in this they
:> could download, build and run the program themselves.
:>
:> Stephen

: 1. What is the logical convincing argument that HP is unsolvable that
: is formalized in that paper?

The paper demonstrates how their theorem prover proved
the unsolvability of the halting problem. The paper
describes in great detail how they phrased the question
so that it could be handled by their theorem prover.
If you want to see the proof generated by the prover,
download the program and run it. It is sitting there
publically available for anyone to test.

The goal of their paper was to demonstrate that a program
could produce a proof of the unsolvability of the halting
problem. Do you consider a program produced proof formal or not?

: 2. What is its (1) formal representation?

: 3. How was that formal representation (2) created?

: 4. What is the general means of mapping such a formal representation
: into a logical convincing argument?

: 5. How is that general means (4) applied to this formal representation
: (2) to produce the logical convincing argument (1)?

: C-B

The paper you are talking about is an example of what
their theorem prover is capable of. It does not describe
the theorem prover in great detail because that was done
in earlier papers. You can find a more detailed description
at
        http://www.cs.utexas.edu/users/moore/best-ideas/nqthm/

You can find the answer to your questions there and in their
other work. You can also download and run their theorem prover and
see how it works. That is what the goal of their work
was: to build a system that actually generates proofs.
You claim their system is a fraud, despite the fact that you have
apparently never bothered to actually look at it, and despite
the fact that other people have actually used it.

Stephen

Relevant Pages

  • Re: Some Simple Questions
    ... > the theorem prover for the proof of the unsolvability of ... > You can build the theorem prover, ... What is the logical convincing argument that HP is unsolvable that ... How was that formal representation created? ...
    (sci.math)
  • Re: Some Simple Questions
    ... > the theorem prover for the proof of the unsolvability of ... > You can build the theorem prover, ... What is the logical convincing argument that HP is unsolvable that ... How was that formal representation created? ...
    (sci.logic)
  • Re: Some Simple Questions
    ... :> You can build the theorem prover, ... :> could download, build and run the program themselves. ... the unsolvability of the halting problem. ... How was that formal representation created? ...
    (sci.logic)
  • Re: proof of undecidability of halting problem
    ... Moore's theorem prover, and thus easily refute your lies; ... The point is that Boyer & Moore have a theorem prover ... to show a correspondence between the formal representation and the ... The set of programs that halts no on itself is r.e. ...
    (sci.logic)
  • Re: Some Simple Questions
    ... Mathematical expressions and English In the ... :> the theorem prover in great detail because that was done ... Since you seem to know the system and how it proves HP unsolvability, ... I am mainly just responding to your accusations of fraud. ...
    (sci.logic)