Slashdot Mirror
Mechanical Reasoners Battle It Out In Sydney Today
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."
That's only 7 minutes per.
You are assuming the logic never gets in trouble with the Apple Party Line and gets blacklisted.
Darwin in the lounge with the binary decision diagrams?
(!clue:"mechanical reasoning") -> (!valid(opinion:"esoteric Slashdot article"))
"In a 32-bit world, you're a 2-bit user. You've got your own newsgroup, alt.total.loser." -Weird Al
take a piss test.
What?
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.
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 and Curta, not computer programs.
"Anyone who [rips a CD] is probably engaging in copyright infringement." - David O. Carson
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.
This is where the line wrapped on my monitor. For a second I felt thought Slashdot was threatening me.
I was hoping I'd be seeing some cool old Babbage gear up and running. Programs doing logic? VERY old news.
I piss off bigots.
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.
but the Turks'.
forty-two.
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.)"
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
But...I thought they were all belonged to us?
If you quote this signature there'll be 72 copies of Windows ME waiting for you in Heaven.
I just misread the headline as: "Mechanical Resonator" and then had mental images of dueling vibrators on the streets of Sydney...
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)
PS: I don't reply to ACs.
http://www.angryflower.com/cubepu.gif
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...
--frank[at]unternet.org
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.
Oh yes, I took it there
Disclaimer: I am not god.
We may not be created equal
But we can be treated equal.
This page includes a list of FLOSS automated theorem provers. Fedora 10 adds several of these tools, so you'll be able to easily install and try out some of them.
- David A. Wheeler (see my Secure Programming HOWTO)