Emeritus Professor School of Computer Science McGill University
Theo and Octopus at the 2006 World Championship for Automated Reasoning Programs Seattle, Washington, August 18, 2006
The Computer History Museum and its exhibit on Computer Chess.
Monty Newborn received his Ph. D. in Electrical Engineering from The Ohio State University in 1967. He was an assistant professor and then associate professor at Columbia University in the Department of Electrical Engineering and Computer Science from 1967-1975. In 1975, he joined the School of Computer Science at McGill University and has been with the School since then, serving as its director from 1976-1983. He has been an ACM Fellow since 1994 and a member of the Canadian Chess Hall of Fame since 2001.
His research has focused on search problems in artificial intelligence where two areas are of particular interest: chess-playing programs and automated theorem-proving programs. He has published seven books on these subjects and a number of research papers as well. He served as chairman of the ACM Computer Chess Committee from 1981 until 1997. In that capacity he organized the first Kasparov versus Deep Blue match (known as the ACM Chess Challenge) in 1996. The following year he served as head of the officials at the second Kasparov versus Deep Blue match won by Deep Blue. Through the 1970s and 1980s, his chess program Ostrich competed in five world championships, coming close to winning in 1974.
Octopus and Theo, two automated theorem-proving programs developed over the last fifteen years are the current focus of his work. They both competed in the recent 2006 World Championship for ATP Systems in Seattle, Washington. Octopus, a multiprocessor version of Theo, ran on 133 PCs in the School's laboratories during the competition, searching in parallel for proofs of theorems chosen by the competition's organizers. In the 2004 competition, Octopus performed admirably, solving more theorems among those that no entry had seen before than any other entry. Octopus and Theo finished best of the North American entries.
Beyond Deep Blue: Chess in the Stratosphere, Springer-Verlag, 2011 (at amazon.com).
Deep Blue: An Artificial Intelligence Milestone, Springer-Verlag, 2003 (at amazon.com).
Automated Theorem Proving: Theory and Practice, Springer-Verlag, 2001 (at amazon.com).
Deep Blue: Computer Chess Comes of Age, Springer-Verlag, 1997 (at amazon.com).
How Computers Play Chess, with D. Levy, WH. Freeman, NY, 1991 (at amazon.com).
All About Chess and Computers, with D. Levy, Computer Sci Press, Potomac, MD, 1982.
More Chess and Computers, with D. Levy, Computer Sci Press, Potomac, MD, 1980.
Computer Chess, Academic Press, NY, 1975.
Wang, Z., and Newborn, M., "Octopus: Combining learning and parallel search," Journal of Automated Reasoning, v. 33, n. 2, pp. 171-218, 2004.
Octopus is an automated theorem proving program that combines learning and parallel search. Running on more than 100 PCs, each computer initially attempts to prove a "weaker" or simpler version of a given theorem. If a proof is found, it uses what it learned to help prove the given theorem. Exactly what is a weaker version and what is learned and then used from its proof are the subject of this paper.
Newborn, M., and Wang, Z., Proofs of Nineteen More 1.0 Rated Theorems in the TPTP Problem Library, School of Computer Science, McGill University, Montreal, Canada, January 2004, Technical Report SOCS-04.1.
Newborn, M., Proofs of Twenty-Four 1.0-Rated Theorems in the TPTP Problem Library, School of Computer Science, McGill University, Montreal, Canada, July 2003, Technical Report SOCS-03.6 with appendices.
Octopus proved a number of theorems over the last year from the TPTP Problem Library. This library is a database of more than 7000 theorems used by researchers in automated theorem proving for testing their systems. Approximately 1000 of these theorems are assigned a rating of 1.0 indicating that no ATP system has obtained a proof thus far when the ATP system was run under the auspices of the database creators. Though not run under the auspices of the database creators, Octopus, nevertheless has proved 43 of these 1.0 rated theorems, and the above two SOCS technical reports present their proofs. Some of the proofs involve several hundred inferences.
Almulla, M., and Newborn, M., "Restricting moves when solving the NxP-puzzle," Proceedings of the 7th Joint Conference on Information Sciences, Sept 26-30, pp. 474-480, 2003.
Can the famous NxP puzzle be solved if the blank is only allowed to move in a clockwise direction? This paper answers this question in the affirmative!
Newborn, M., "Deep Blues contribution to AI,"Annals of Mathematics and Artificial Intelligence, v. 28, pp. 27-30, 2000.
Hyatt, R., & Newborn, M., "Crafty goes deep," International Computer Chess Association Journal, v. 20, n. 2, pp. 7986, Jun 1997.
Newborn, M., "Outsearching Kasparov," American Mathematical Society's Proceeding of Symposia in Applied Mathematics: Mathematical Aspects of Artificial Intelligence, v. 55, pp 175205, 1998. Based on paper presented at the 1996 Winter Meeting of the AMS, Orlando, Florida, Jan 911, 1996.
Was Deep Blue better than Kasparov when it defeated him in their classic chess showdown in 1997? We all know the best player doesn't always win. These three papers explore this issue.
Yu, Q., Almulla, M., & Newborn, M., "Heuristics used by HERBY for semantic tree theorem proving," Annals of Mathematics and Artificial Intelligence, v. 23, pp. 247266, 1998.
Almulla, M., & Newborn, M., "The practicality of generating semantic trees for proofs of unsatisfiability," International Journal of Computer Mathematics, v. 62, n. 12, pp. 4561, 1996.
As has been said, there is more than one way to skin a cat, and there is more than one way to prove a theorem. These two papers explore the practicality of proving theorems by constructing closed semantic trees.
Paul Haroun, Enhancing Theorem Provers by Delayed Clause Construction and Path Attributes, McGill 2005.
Choon Kyu Kim, Parallel Semantic Tree Theorem Proving with Resolutions, McGill 2004, with Korean Telecomm, Seoul, Korea.
Cliff Grossner, Information Deficit in Cooperating Distributed Expert Systems, McGill 1995, Jointly supervised with Prof. T. Radhakrishnan, Concordia University; with Rev D Networks, an Ottawa-based telecom software company.
Mohammed Almulla, The Practicality of Using Semantic Trees for Proving Theorems in First-Order Predicate Calculus, McGill 1995; with Kuwait University.
Brian Patrick, An Analysis of Iterative Deepening A*, McGill 1992; with Trent University, Trent, Ontario.
Nabil Rafla, Drawings of the Complete Graph of Kn, McGill 1988; with Bell Canada, Montreal.
Selim Akl, Stat. Anal. of Some Properties of Solutions to the Traveling Salesman Problem, McGill 1977; with Queens University, Kingston, Ontario. (http://www.cs.queensu.ca/home/akl/)
Joonki Kim, The Synthesis of Nondeterministic Sequential Machines, Columbia 1974; with IBM, Yorktown Heights, NY.
Ron Angner, Switching Rates of Combinatorial Circuits, Columbia 1973; with Management Network Group Incorporated, Kansas.
Hsieh Hao, Trigger Machines, Columbia 1972.
Thomas Arnold, Iteratively Realized Sequential Circuits, Columbia 1970.