1978, Wheels, life and other mathematical amusements. W H Freeman & Co., London, 1985), Douglas Hofstadter [in one of the best popular science books on paradoxes (Hofstadter in Godel, escher, bach: an eternal golden braid, Penguin, London, 2000)], inspired by Gödel's incompleteness theorems), Patrick Hughes and George Brecht (see Hughes and Brecht in Vicious circles and infinity, an anthology of paradoxes. Penguin Books, London, 1993) and Raymond M. Smullyan (the most well known being Smullyan in Forever undecided, puzzle guide to godel. Oxford Paperbacks, Oxford 1988, To Mock a Mockingbird and other logic puzzles. Oxford Paperbacks, Oxford 2000, The lady or the tiger? And other logic puzzles. Dover Publications Inc., Mineola 2009), inter alia. Books by Smullyan (such as Smullyan 1988, 2000) are, however, much more involved, since they introduce learning trajectories and strategies across several subjects of mathematical logic, as difficult as combinatorial logic (see, e.g., Smullyan 2000), computability theory (see Smullyan 1988), and proof theory (see Smullyan 1988, 2009). These books provide solutions to their suggested exercises. Both statements and their solutions are written in the natural language, introducing some informal algorithms. As an exercise in Mathematics we wonder if an easy proof system could be devised to solve the amusing equations proposed by Smullyan in his books. Moreover, university students of logic could well train themselves in constructing deductive systems to solve puzzles instead of a non-uniform treatment one by one. In this paper, addressing students, we introduce one such formal systems, a tableaux approach able to provide the solutions to the puzzles involving either propositional logic, first order logic, or aspect logic. Let the reader amuse herself or himself! " /> Solving smullyan puzzles with formal systems - Poças Diogo | sdvig press