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

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.