Axioms are pervasive in mathematics and formulating the axioms for a particular discipline has often been an importantstep in the development of mathematics. One way mathematicians arrive at axioms is by characterizing a given domainthat consists of objects (e.g., numbers or points and lines) and relations between them. We present a software system that,given a set of objects and relations as input, determines, first, a set of first-order formulas that are satisfied in that domain,and, second, a set of axioms from which all of these formulas can be derived. Several domains are used to illustrate ourprogram. By comparing the axioms for different domains, analogies between these domains can be expressed, such asstructural and invariance properties. From the complexities of the implementation and the discussion of various examples,conclusions are drawn about the process of axiomatization in mathematical practice.