Slashdot Mirror

← Back to Stories (view on slashdot.org)

Mechanical Reasoners Battle It Out In Sydney Today

Posted by timothy on from the turk-v.-hal dept.

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."

32 of 45 comments (clear)

  1. 12 programs per hour? by Anonymous Coward · · Score: 1, Funny

    That's only 7 minutes per.

    1. Re:12 programs per hour? by gardyloo · · Score: 4, Funny

      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.

    2. Re:12 programs per hour? by Warll · · Score: 1

      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!

    3. Re:12 programs per hour? by spazdor · · Score: 2, Funny

      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.

      --
      DRM: Terminator crops for your mind!
  2. It was... by DarkEntity · · Score: 4, Funny

    Darwin in the lounge with the binary decision diagrams?

  3. For the automata reading this discussion by Jonboy+X · · Score: 4, Funny

    (!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
  4. Make 'em by iminplaya · · Score: 1

    take a piss test.

    --
    What?
  5. Confusing summary by langelgjm · · Score: 5, Insightful

    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
    1. Re:Confusing summary by Normal+Dan · · Score: 3, Informative

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

      --
      A unique way to learn a language: http://languageloom.com
    2. Re:Confusing summary by camperdave · · Score: 1

      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?".

      --
      When our name is on the back of your car, we're behind you all the way!
    3. Re:Confusing summary by Anonymous Coward · · Score: 2, Funny

      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.

    4. Re:Confusing summary by gyrogeerloose · · Score: 3, Funny

      Prove that women are evil:

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

      --
      This ain't rocket surgery.
    5. Re:Confusing summary by cmacb · · Score: 2, Insightful

      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".

  6. Nice touch by Night+Goat · · Score: 1

    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.

  7. Weak in logic by Nerdposeur · · Score: 2, Funny

    ...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.

  8. Ditto. They mean electrical, not mechanical. by EWAdams · · Score: 2, Interesting

    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.
  9. More info please by jshriverWVU · · Score: 1

    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.

    1. Re:More info please by bunratty · · Score: 2, Informative

      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.

      --
      What a fool believes, he sees, no wise man has the power to reason away.
    2. Re:More info please by omuls+are+tasty · · Score: 1

      It's a competition where automated theorem provers for 1st order logic are given a subset of a problem library.

      I don't think any of the provers are using genetic algorithms, since they're suited for optimization, not deduction.

    3. Re:More info please by stephanruby · · Score: 2, Insightful

      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.

    4. Re:More info please by halcyon1234 · · Score: 1

      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".

      --
      UTF-8: There and Back Again
  10. It's nobody's business by Anonymous Coward · · Score: 2, Funny

    but the Turks'.

  11. to save time, the answer is.... by owlnation · · Score: 1, Funny

    forty-two.

  12. Reminds me of Concrete Mathematics... by file_reaper · · Score: 5, Funny

    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.)"

    1. Re:Reminds me of Concrete Mathematics... by retchdog · · Score: 2, Informative

      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.)

      --
      "They were pure niggers." – Noam Chomsky
  13. Ownership... by ZarathustraDK · · Score: 2, Funny

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

    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.
  14. Dough! I Misread the headline.. by Zymergy · · Score: 1

    I just misread the headline as: "Mechanical Resonator" and then had mental images of dueling vibrators on the streets of Sydney...

    1. Re:Dough! I Misread the headline.. by Spasemunki · · Score: 1

      You think you were confused? I was picturing robotic 60 Minutes anchors duking it out in front of the Opera House...

  15. Pretty cool by ThorGod · · Score: 1

    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.
  16. Run it on an iphone? by knarf · · Score: 2, Insightful

    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
  17. And the final puzzle? by VeNoM0619 · · Score: 1

    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.
  18. More info: FLOSS tools and ongoing Fedora work by dwheeler · · Score: 1

    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)