Our computational metaphysics group describes its use of automated reasoning tools to study Leibniz’s theory of concepts. We start with a reconstruction of Leibniz’s theory within the theory of abstract objects (henceforth ‘object theory’). Leibniz’s theory of concepts, under this reconstruction, has a non-modal algebra of concepts, a concept-containment theory of truth, and a modal metaphysics of complete individual concepts. We show how the object-theoretic reconstruction of these components of Leibniz’s theory can be represented for investigation by means of automated (...) theorem provers and finite model builders. The fundamental theorem of Leibniz’s theory is derived using these tools. (shrink)

In 2000, a draft note of David Hilbert was found in his Nachlass concerning a 24th problem he had consider to include in the his famous problem list of the talk at the International Congress of Mathematicians in 1900 in Paris. This problem concerns simplicity of proofs. In this paper we review the traces of this problem which one can find in the work of Hilbert and his school, as well as modern research started on it after its publication. We (...) stress, in particular, the mathematical nature of the problem.1. (shrink)