Dipartimento di Informatica e Scienze dell'Informazione
May I Borrow Your Logic?
(Transporting Logical Structures along Maps)
M. Cerioli and J. Meseguer.
Theoretical Computer Science, 1996.
To appear.
It can be very advantageous to borrow key components of a logic
for use in another logic. The advantages are both conceptual and practical;
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 natural 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/TCS96.ps.gz
(120631 Kb)