 Returning to the first example (combining a sequent calculus with an axiomatic system), a better solution was proposed in Cruz-Filipe et al. 2008: the idea is to define an abstract formalism for proof systems, general enough as to encode the main proof mechanisms found in the literature. Thus, after reformulating \({{\cal L}}_1\) and \({{\cal L}}_2\) as abstract proof systems of this kind, the resulting combined logic \({{\cal L}}\) is an abstract proof system in which it is possible to recognize the ‘genetic traces’ of the original inference rules of each component within derivations in \({{\cal L}}\). The latter question, namely, how to characterize derivations in a fibred logic in terms of the derivations of the components, was carefully analyzed by S. Marcelino et al. in a series of papers Marcelino et al. 2015; Marcelino and Caleiro  2016; and Marcelino and Caleiro 2017a.  See  subsection 4.3.