Drexel dragonThe Math ForumDonate to the Math Forum



Search All of the Math Forum:

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


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

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,227
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 <newberr...@gmail.com> 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

STANDARD MODUS PONENS (Depth Limited)



---------------------

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.

A BOUND COMPLEXITY SET THEORY is also possible.

set1 = { M | prove X true }

set2 = { M | prove X false }

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

---------------------------------------------

Herc

--

http://phpPROLOG.com

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

SELECT HEADS.id
FROM QUERY
INNER JOIN HEADS
ON QUERY.ref=HEADS.ref
AND QUERY.term=HEADS.term

DATABASE QUERY
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]

© Drexel University 1994-2014. All Rights Reserved.
The Math Forum is a research and educational enterprise of the Drexel University School of Education.