# How did the Logic Theorist prove the Pons Asinorum?

I was reading about the Logic Theorist proving many of the Whitehead and Russell's Principia's theorems. However, I cannot find any technical explanation on how the program proved those theorems and specifically what method did it use to solve the Pons Asinorum. I'm interested in understanding how "independent" it was in providing those proofs, mostly since it is celebrated as an "AI" program.

## 1 Answer

If you google "logic theorist source code" you find this which is clearly not the original source code, but presumably is a modernization of the ideas in the code. You can also find this 1963 RAND memorandum which is a more contemporary description of the system. It seems to include a complete code listing as well as descriptions in terms of flowcharts.

As far as I can tell, it proved basic statements in essentially classical propositional logic. The main idea is backward chaining.

Page 52 of Perspectives on the History of Mathematical Logic shows the (erroneous) proof of Theorem 2.85 in Principia Mathematica and the proof Logic Theorist produced. Theorem 2.85 (using more common notation) is $$((P\lor Q)\Rightarrow(P\lor R))\Rightarrow(P\lor(Q\Rightarrow R))$$ which (ironically) is actually easier to read in Logic Theorist's notation, (((PVQ)I(PVR))I(PV(QIR))), than it is in the aforementioned page. As you should be able to tell, this has no particular connection to any geometrical theorem, let alone the isosceles triangle theorem. I have no idea why it's linked that way on Wikipedia. You could, however, take e.g. Tarski's axioms for planar geometry and apply the same proof search techniques to questions in Euclidean geometry as done in Automated Development of Tarski's Geometry by Art Quaife. I can't find a good reference, but I'm fairly certain novel and elegant proofs have been found when automated theorem proving (in this style) has been applied to planar geometry. This isn't surprising as these systems tend to search the proof space starting from the shortest proof candidates.