Hacker News Reader

Comment by ColinWright | Hacker News Reader

I would be interested to see why you claim that the FCT was proven by an automated reasoner. My understanding is that Haken and Appel created techniques to create unavoidable configurations, and techniques to prove that a given configuration is reducable. They then programmed a computer to find an unavoidable set of reducable configurations.

In Haken and Appel's proof there was no automated reasoning.

Similarly in this case. The theorem claims that for every C there is an N such that a sequence of length at least N has a sub-configuration of discrepancy at least C. In this case the researchers created a program to show that in a sequence of length at least 1161 there is always a sub-sequence of discrepancy of at least 2.

To the best of my understanding there is no automated reasoning, so I would be interested to see why you claim otherwise.

View on HN

All Automated Reasoning is... is programming a computer to search a space automatically. In First Order Logic, you use the Resolution Rule to generate the search space for example. But at the end of the day... Automated Reasoning is nothing more than a glorified graph traversal.

The FCT was solved with a hybrid method. Yes, you mention that there was significant human input in reducing the problem. However, a computer program was used to find (and prove) a huge number of those configurations.

Search and verification. That is all "automated reasoning" is. In AI circles the FCT is considered to have been solved by Automated Reasoning methods.

http://en.wikipedia.org/wiki/Automated_theorem_proving#Relat...

Knowing the FCT as well as I do, I have to say that I and many of my colleagues do not consider the H-A proof to be anything like automated reasoning. The work that Gowers and associates are now doing is very much so, but programming a computer to conduct a specific search, and for every item found compute whether it has a specific characteristic is really just like getting a machine to carry out a factoring algorithm.

We run the risk of arguing past each other, and potentially being in "violent agreement," but consider this. If you take an 8x8 chessboard and remove any black square and any white square, the resulting mutilated chess-board is guaranteed to be exactly coverable by dominoes, each of which covers exactly two squares. We can program a computer to conduct an exhaustive search to show that this is true. Would you consider the program to be an automated reasoner?

With what I know of this recent result, the work seems equivalent. It's a big problem fed to a SAT solver.

Edit: See the last paragraph of section 1 in the paper: http://arxiv.org/pdf/1402.2184.pdf

Yes, although brute force would be "simple AI", but the basics of AI nonetheless.

One of the many "classic" problems given to students of Artificial Intelligence is the 8-Queens problem: http://en.wikipedia.org/wiki/Eight_queens_puzzle#Exercise_in...

It is a short step to go from "8-Queens Algorithm Design" to "8-Queens Logic Programming", and from there automated reasoning. After all, Logic Programming is purely based on automated reasoning using Horn Clauses. It just so happens to be one of the most optimized forms of automated logic, fast enough to be a general programming language (Prolog is one of the easiest languages to solve the 8-Queens problem)

Automated Reasoning covers new tricks, like tree pruning, different logic systems or methodologies (Tableau Logic)... but no matter how complicated it gets, it all comes back to the same methodology. Its simply a glorified search algorithm, defined over some space. (Prolog at its core is nothing more than a depth first search over the horn clauses specified by the programmer)

For an example that clearly demonstrates the search, here's a Wikipedia link to Tableau type automated reasoning:

http://en.wikipedia.org/wiki/Method_of_analytic_tableaux#Sea...

And of course, the Automated Conference on the Tableaux Automated Reasoning methodology:

http://en.wikipedia.org/wiki/International_Conference_on_Aut...

The "Art" of Automated Reasoning is not in the search methodology (which is almost always just depth-first search + heuristics), but in how to define those spaces. Horn Logic, Tableaux, First Order Logic / Resolution Rule, etc. etc.

So whenever a new "search space" is defined to solve a practical problem, it is always of great interest to the Automated Reasoning community.

  >> If you take an 8x8 chessboard and remove any
  >> black square and any white square, the resulting
  >> mutilated chess-board is guaranteed to be exactly
  >> coverable by dominoes, each of which covers exactly
  >> two squares. We can program a computer to conduct
  >> an exhaustive search to show that this is true.
  >> Would you consider the program to be an automated
  >> reasoner?
	
  > Yes,

That surprises me. That feels a lot like describing Eliza as a conversationalist. Technically true, but ultimately unhelpful and unenlightening.

By way of contrast with the above described brute-force search, which also only works on a fixed size board, here's a proof that works on all NxN boards, where N is even.

We can construct a tour of the squares, visiting each exactly once, each time moving from a square to one of the squares with which it shares a side. Removing one black and one white divides this into two (or possibly only one) segments. Each can easily be shown to be of even length, and therefore each is coverable by dominoes. QED.

If you simply enumerate a very large number of possibilities, it doesn't feel like reasoning.

You seem to be of the opinion that only "Strong AI" should be considered as "intelligence". In contrast, I'm of the opinion that "weak AI" is sufficient for the "intelligence" definition.

Although, since I've done some research in the AI Field, I also recognize the distinction and the two. There is a controversy, even in AI circles, over what constitutes AI. So I'm not going to debate with you the merits of Strong AI vs Weak AI.

It is sufficient enough for me to just inform you... this controversy exists and is real.

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

http://www.i-programmer.info/babbages-bag/297-artificial-int...

>>> This is the curse of strong AI. Whenever you make something work, you know how it works and it no longer seems intelligent.

I think you two are disagreeing about terminology. You're the ecpert in the field, which (correctly) makes you more sensitive to terminological distinctions.

What's not disputed I guess, is the commonly (to CS-educated engineers) held notion that FCT is a high-profile math problem that was solved/proved by intensive automatic means rather than a human written proof, and that that raises questions regarding the meaning of "proof".

At least that's what I took home from it.

Other people claim that FCT was proven by computer. Most of my colleagues say it was proven by Haken and Appel, who programmed a computer to perform a finite search. People who work in the area - including me - say it's like getting Wolfram Alpha to solve your integrals, while you do the actual thinking about what integrals need solving, why, and what to do with the answers.

I see what you nean: the computer as a tool, rather than as the one that does tge proving.

“Computers Are Useless. They Can Only Give You Answers” -- Pablo Picasso

Reply on news.ycombinator.com