Dipartimento di Informatica e Scienze dell'Informazione
May I Borrow Your Logic?
M. Cerioli and J. Meseguer.
In A.M. Borzyszkowski and S. Sokolowski, editors, Proc. of
Mathematical Foundation of Computer Science '93, number 711 in Lecture Notes
in Computer Science, pages 342--351, Berlin, 1993. Springer Verlag.
It can be very advantageous to borrow key components of a logic
for use in another logic. The advantages may be not only conceptual; due to
the existence of software systems supporting mechanized reasoning in a given
logic, it may be possible to reuse a system developed for one logic---for
example, a theorem-prover---to obtain a new system for another.
Translations
between logics by appropriate mappings provide a first way of reusing tools of
one logic in another. This paper generalizes this idea to the case where
entire components---for example, the proof theory---of one of the logics
involved may be completely missing, so that the appropriate mapping could not
even be defined.
The idea then is to borrow the missing components (as well
as their associated tools if they exist) from a logic that has them in order
to create the full-fledged logic and tools that we desire. The relevant
structure is transported using maps that only involve a limited aspect of the
two logics in question---for example, their model theory. The constructions
accomplishing this kind of borrowing of logical structure are very general and
simple. They only depend upon a few abstract properties that hold under very
general conditions given a pair of categories linked by adjoint functors.
The compressed postscript version of this paper is available through anonymous ftp
at ftp.disi.unige.it, in
/person/CerioliM/MFCS93.ps.z
(46889 Kb)