 Along with the problem itself  three solutions are posted:  Shanahan 2004,   Lifschitz 1998b,  and a version of   Morgenstern 2001.  Comparing the solutions is instructive: similarities outweigh differences.  All the authors think of this as a planning problem, and use a versions of the Situation Calculus or the Event Calculus in the formalization. Each axiomatization is modular, with, for instance, separate modules devoted to the relevant geometrical and material properties.  Each author provides a “proof of concept” for the formalization by showing that the axioms support a proof of the correctness of a plan to crack the egg in the simple case.  None of the authors considers all of Davis’ elaborations of the problem, but the axioms are framed with elaboration in mind and some elaborations are considered.  It isn’t clear whether any of the authors actually implemented the formalization (for instance, using a theorem prover). 