×

Welcome to the Slashdot Beta site -- learn more here. Use the link in the footer or click here to return to the Classic version of Slashdot.

Thank you!

Before you choose to head back to the Classic look of the site, we'd appreciate it if you share your thoughts on the Beta; your feedback is what drives our ongoing development.

Beta is different and we value you taking the time to try it out. Please take a look at the changes we've made in Beta and  learn more about it. Thanks for reading, and for making the site better!

Mechanical Reasoners Battle It Out In Sydney Today

timothy posted more than 5 years ago | from the turk-v.-hal dept.

Math 45

Stephan Schulz writes "Today, the CADE ATP System Competition will pit about 20 of the worlds most powerful mechanical mathematicians against each other — and for the first time they can win not only honour, but a monetary prize. The systems will reason against the clock on tasks ranging from undergraduate math problems and Cluedo-like puzzles to figuring out the possible responsibility for terrorist attacks from giant knowledge bases. If you think that is not impressive enough, they are doing it at a rate of 12 problems per hour, all day long. The competition starts at 10 a.m. in Sydney, Australia, which is midnight UTC. Live results will be available at the competition page. For added geek appeal, most of the contenders are available under open source licenses, so if you are weak in logic you can hack up your own brain extension and run it on an iPhone."

cancel ×
This is a preview of your comment

No Comment Title Entered

Anonymous Coward 1 minute ago

No Comment Entered

45 comments

butt sex (-1, Offtopic)

Anonymous Coward | more than 5 years ago | (#24590403)

stick it in the butt

12 programs per hour? (1, Funny)

Anonymous Coward | more than 5 years ago | (#24590421)

That's only 7 minutes per.

Re:12 programs per hour? (4, Funny)

gardyloo (512791) | more than 5 years ago | (#24590575)

Sweet! I want to get me some of those 84 minute hours like they have in Australia!

    P.S. I think you should volunteer your mathematical abilities to the teams.

Re:12 programs per hour? (1)

Warll (1211492) | more than 5 years ago | (#24591041)

Sweet! I want to get me some of those 84 minute hours like they have in Australia!

You think that's nice? Wait till you try metric time!

Re:12 programs per hour? (0)

Anonymous Coward | more than 5 years ago | (#24591849)

?
Seriously?
Am I missing a joke here?

Re:12 programs per hour? (2, Funny)

spazdor (902907) | more than 5 years ago | (#24605537)

The theorem-proving race was neck-in-neck until we got to the fourth event, the Halting Problem.

No clear winner for this one yet. Stay tuned.

Oh, can you smell what I'm cooking? (-1, Redundant)

Anonymous Coward | more than 5 years ago | (#24590465)

no summary available

FIRST POST bitches

I brought it, you live it, now suck it

Re:Oh, can you smell what I'm cooking? (0, Offtopic)

Anonymous Coward | more than 5 years ago | (#24590615)

I am sorry, but you have failed your one mission and goal in life.

The sword is to your right. Do with it what you must.

Go eat scrambled Buckcake. (-1, Offtopic)

Anonymous Coward | more than 5 years ago | (#24590643)

Posh Spice says High.

Run it on an iphone?? (0)

Anonymous Coward | more than 5 years ago | (#24590495)

You are assuming the logic never gets in trouble with the Apple Party Line and gets blacklisted.

For the automata reading this discussion (4, Funny)

Jonboy X (319895) | more than 5 years ago | (#24590559)

(!clue:"mechanical reasoning") -> (!valid(opinion:"esoteric Slashdot article"))

Foreign policy from a select few "inteligent" is (-1, Offtopic)

Anonymous Coward | more than 5 years ago | (#24590599)

lame. Aside from Mathematics, the same trained mathemetacians, having no style of arithmetic accreditted to them other than what was allowed to be taught to them under the guise of education, are reasoning foreign policy towards terrorist attack. Fat joke from creatures of no productive export outside of Intellectual Property. They always find ways to spend someone else's money on somthing they couldn't do with their own available money themselves; and worse, it's all just a divertion from their bad habits. If you have a terrorist problem or illegal alien problem (for that matter), all you can be sure of is what you can do about your own problem and report to your neighbor for any reception to assist them in resolving theirs. So far, the #1 remedy to a militant is equality; military was once a civil question taken into execution, but has now become just another corporation offering cleansing service ritually applied by libel of review (hence often read in a captain's journal his offence durring the Vietnamese War is colored as "cleansed the area").

Confusing summary (5, Insightful)

langelgjm (860756) | more than 5 years ago | (#24590647)

Was I the only one who was confused by the summary? When I read "mechanical mathematicians", I was thinking along the lines of the Bomba [wikipedia.org] and Curta [wikipedia.org], not computer programs.

Re:Confusing summary (3, Informative)

Normal Dan (1053064) | more than 5 years ago | (#24590745)

I was thinking it meant humans who work on the mathematics of machines.

Re:Confusing summary (2, Funny)

Anonymous Coward | more than 5 years ago | (#24591749)

I was thinking along the lines of a mechanical proof:

Prove that women are evil:
1) Women require time and money
Women= Time * Money
2) Time is money, therefore
Women= Money^2
3) Money is the root of all evil
Money=sqrt(Evil)^2
4) Therefore,
Women=Evil
Q.E.D.

Re:Confusing summary (3, Funny)

gyrogeerloose (849181) | more than 5 years ago | (#24592103)

Prove that women are evil:

What is this "woman" thing of which you speak?

Re:Confusing summary (0)

Anonymous Coward | more than 5 years ago | (#24592525)

It's kinda like an anus, but smells better.

You know, that bacon and eggs you had this morning * flip-flops. Basically every chevy 350 bolted you've ever drove bolted to a th400 tranny in the world at once. I mean, seriously, what the hell is it about day-lilies that make my chair squeak so much? You know, the bath-tub and all (nudge, nudge).

Yea, I went there.

Ditto. They mean electrical, not mechanical. (2, Interesting)

EWAdams (953502) | more than 5 years ago | (#24591081)

I was hoping I'd be seeing some cool old Babbage gear up and running. Programs doing logic? VERY old news.

You mean "electronic" (0)

Anonymous Coward | more than 5 years ago | (#24592049)

But yes, me too. The image of gear-driven designs battling to finish difficult problems first was entirely charming, and increased my admiration for Aussie quirk & gumption quite a bit.

But no, this is Automated Theorem Proving, runing on some LinTel boxes. A pox on the submitter and editor, though not of course the entirely respectable CADE organizers.

And as if they needed more proof of geek cred, that has to be one of the worst t-shirt designs ever. Well done lads.
http://www.cs.miami.edu/~tptp/CASC/J4/T-shirtGIF.html [miami.edu]

Re:Confusing summary (1)

camperdave (969942) | more than 5 years ago | (#24591477)

I was thinking along those lines too, though moreso mathematicians who operate such devices. In other words, that the contest was a sliderule showdown, or an abacus race, but with more mechanical devices. When I saw that they were talking about automated mathematical software, my next thought was "What's a software going to do with prize money?".

Re:Confusing summary (2, Insightful)

cmacb (547347) | more than 5 years ago | (#24592425)

Ditto. I went looking for some use of the word "mechanical" other than this "summary". Didn't find any.

So I'm guess that this article was submited in Chinese and then run through several language translations (maybe even mechanical ones) before being rendered into "English".

Nice touch (1)

Night Goat (18437) | more than 5 years ago | (#24590663)

I like how they included the t-shirt sizes next to each entrant. They skew a bit toward the Large and X-Large sizes. Very logical.

Weak in logic (2, Funny)

Nerdposeur (910128) | more than 5 years ago | (#24590841)

...so if you are weak in logic you can hack up your own brain

This is where the line wrapped on my monitor. For a second I felt thought Slashdot was threatening me.

More info please (1)

jshriverWVU (810740) | more than 5 years ago | (#24591095)

Perhaps I'm the only one who doesnt understand what this is, can someone else elaborate? From my understanding of the page these are programs if given a dataset or description of a dataset can tell you how that data was derived. I can see this being useful in AI. If you have significant dataset of possibilities and trying to yield the best algorithm you could spawn a million children processes with their own genetic algorithm to come up with variations. Perhaps I'm way off. Would like some clarification or pointers to more info.

Re:More info please (2, Informative)

bunratty (545641) | more than 5 years ago | (#24591133)

It's computers automatically solving logic problems. That includes deduction games such as Clue (aka Cluedo), logic puzzles like you can find in magazines, proving mathematical theorems, etc.

Re:More info please (2, Insightful)

stephanruby (542433) | more than 5 years ago | (#24592211)

That includes deduction games such as Clue (aka Cluedo), logic puzzles like you can find in magazines, proving mathematical theorems, etc.

If they're in magazines already, I hope they can use google and just google the answers.

Re:More info please (1)

halcyon1234 (834388) | more than 5 years ago | (#24614059)

Nah, they wouldn't use an already published ones. But you can expect posts like these to Yahoo Answers and Dr. Math at the rate of 12/hour:

ReasonBot07281 asks:

plz hlp need answer. whut iz proof for even numz?! not hmwork just wanderin the answers plz send quick tnkx!!!!!!!!!!1

Which will only get better once the users of said forums catch onto what's going on, and l33tteam's mechanical reasoner starts returning answers like "2=1+I like to lick balls". "For all x, there exists an n where the owners of this machine are fags".

It's nobody's business (2, Funny)

Anonymous Coward | more than 5 years ago | (#24591135)

but the Turks'.

Reminds me of Concrete Mathematics... (5, Funny)

file_reaper (1290016) | more than 5 years ago | (#24591651)

The book...not mathematics of concrete as is said in the book...

"When DEK taught Concrete Mathematics at Stanford for the first time he explained the somewhat strange title by saying that it was his attempt to teach a math course that was hard instead of soft. He announced that, contrary to the expectations of some of his colleagues, he was not going to teach the Theory of Aggregates, not Stone's Embedding Theorem, nor even the Stone-Cech compactification. (Several students from the civil engineering department got up and quietly left the room.)"

Re:Reminds me of Concrete Mathematics... (2, Informative)

retchdog (1319261) | more than 5 years ago | (#24592433)

And DEK's further note about the name: "Not even I was brazen enough to call the course `distinuous mathematics'."

(For those unfamiliar, the idea of the book (and I presume the course) was to build up to elegant concepts and results like in advanced calculus (continuous mathematics), while using an elementary discrete combinatoric context. Hence, con-crete math.)

mo3 0p (-1, Redundant)

Anonymous Coward | more than 5 years ago | (#24592629)

schemes. Fra8kly d1stribution. As

Ownership... (2, Funny)

ZarathustraDK (1291688) | more than 5 years ago | (#24593395)

...to figuring out the possible responsibility for terrorist attacks from giant knowledge bases.

But...I thought they were all belonged to us?

mo3 d9own (-1, Flamebait)

Anonymous Coward | more than 5 years ago | (#24594809)

gave the BSD take a llok at the Which don't use the bloc in order to in the sun. In the but many mfind it that supports population as well

Pretty cool (1)

ThorGod (456163) | more than 5 years ago | (#24595999)

I've heard about this kind of thing in the past. I didn't realize they had working programs, though.

I have to admit, of course, that this does somewhat scare me. After all, it would seem they're going after the usefulness of my Bachelor's of Science! ;) (NOTTTTTTTTT)

Run it on an iphone? (2, Insightful)

knarf (34928) | more than 5 years ago | (#24596317)

I'd say there are many better options to run an extention to your brain on than a proprietary, chained and DRM-encumbered device with a remote kill switch under control of a for-profit organisation...

And the final puzzle? (1)

VeNoM0619 (1058216) | more than 5 years ago | (#24599605)

It's all a clever gimmick where they give them increasingly difficult problems, and then for the final puzzle, give them an hour to solve Mercury Rising [wikipedia.org].

Oh yes, I took it there
Check for New Comments
Slashdot Account

Need an Account?

Forgot your password?

Don't worry, we never post anything without your permission.

Submission Text Formatting Tips

We support a small subset of HTML, namely these tags:

  • b
  • i
  • p
  • br
  • a
  • ol
  • ul
  • li
  • dl
  • dt
  • dd
  • em
  • strong
  • tt
  • blockquote
  • div
  • quote
  • ecode

"ecode" can be used for code snippets, for example:

<ecode>    while(1) { do_something(); } </ecode>
Sign up for Slashdot Newsletters
Create a Slashdot Account

Loading...