Axioms and inference rules form the foundation of deductive systems
and are crucial in the study of reasoning with logics over structures.
Historically, axiomatizations have been discovered manually with much
expertise and effort. In this paper we show the feasibility of using synthesis
techniques to discover axiomatizations for different classes of
structures, and in some contexts, automatically prove their
completeness. For evaluation, we apply our technique to find axioms
for (1) classes of frames in modal logic characterized in first-order
logic and (2) the class of language models with regular operations.