The Math Forum

Search All of the Math Forum:

Views expressed in these public forums are not endorsed by NCTM or The Math Forum.

Math Forum » Discussions » sci.math.* » sci.math

Notice: We are no longer accepting new posts, but the forums will continue to be readable.

Topic: Very dumb question
Replies: 1   Last Post: Jun 18, 2013 1:57 AM

Advanced Search

Back to Topic List Back to Topic List Jump to Tree View Jump to Tree View  
Graham Cooper

Posts: 4,495
Registered: 5/20/10
Re: Very dumb question
Posted: Jun 18, 2013 1:57 AM
  Click to see the message monospaced in plain text Plain Text   Click to reply to this topic Reply

On Jun 18, 1:26 pm, Newberry <> wrote:
> Let M(x) be a partially decidable predicate. Let Cm be a characteristic function of M(x). Assume that ~M(325) is true. We have computer program that computes Cm. And we want to find out if ~M(325). So we feed 325 to our program and wait. After six hours of staring at the blank screen and 14 quadrillion computer cycles, the brighter types will realize that we will never get there this way. We need to prove the theorem ~M(325).
> Does undecidability imply unprovability?

That is called BLACK BOX analysis.

You can then use WHITE BOX analysis and work out Why the Function is
not halting by tracing the program code, you may find some constraint
for it to halt that would violate a precondition and prove a result
from that.

You can also work within a bounded framework and say "~M within 14
quadrillion cycles".

This happens in PROLOG a lot because it tries to blindly solve queries
using all available options and can go into infinite loops.

---- USER QUERY I/O ----

prove THM true :-
prv THM [z[z[z[z 0]]]]

prove THM false :-
prv [ ! THM ] [z[z[z[z 0]]]]

NOTE: the 4 levels deep of inference searching
is arbitrary and for any logically solvable
problem there exists a finite level that
the solution will be found.


prv R [ z Z ] :-
t R

prv R [ z Z ] :-
if L R
prv L Z



By using a depth limit on how many inferences can be made for any
formula (1 less for each level of sub-formulas and so on..)

it is guaranteed to halt and try all possible branches wide.

That way the Theory can return True or False values.


prove [ + 1 1 4 ] ANS ?

ANS = false


after trying 4 levels deep of

prove THM true :-
prv THM [z[z[z[z 0]]]]

and failing, it then tries to prove it false.


In this way you have a deterministic TRUE or FALSE predicate system,
although bounded by some predefined depth limit.


set1 = { M | prove X true }

set2 = { M | prove X false }

[ e M set1 ] <-> [ not [ e M set2 ]]




A.I. Software / Database on the Web!
Powered By SQL


id ref term ref term
---------------------- ----------------
6 1 test1
6 2 aaa
7 1 test1 <=> 1 test1
7 2 bbb <=> 2 bbb
---------------------- ----------------

Point your RSS reader here for a feed of the latest messages in this topic.

[Privacy Policy] [Terms of Use]

© The Math Forum at NCTM 1994-2018. All Rights Reserved.