TY - GEN

T1 - May I borrow your logic?

AU - Cerioli, Maura

AU - Meseguer, José

N1 - Funding Information:
This proliferation of logics--although certainly a sign of vitality and intellectual creativity--brings with it important conceptual challenges. In a sense, each logic is a different language and, as in the case of natural languages, there is often a * Partially supported by Progetto Finalizzato Sistemi Informatici e Calcolo Parallelo of C.N.R. (Italy), MURST-40% Modem e Specifiche di Sistemi Concorrenti, by the US Office of Naval Research under contracts N00014-90-C-0086 and N00014-92-C-0518, and by the Information Technology Promotion Agency, Japan, as a part of the R ~z D of Basic Technology for Future Industries KNew Models for Software Architecture" sponsored by NEDO (New Energy and Industrial Technology Development Organization).
Publisher Copyright:
© 1993, Springer Verlag. All rights reserved.

PY - 1993

Y1 - 1993

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85029591029&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85029591029&partnerID=8YFLogxK

U2 - 10.1007/3-540-57182-5_26

DO - 10.1007/3-540-57182-5_26

M3 - Conference contribution

AN - SCOPUS:85029591029

SN - 9783540571827

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 342

EP - 351

BT - Mathematical Foundations of Computer Science 1993 - 18th International Symposium, MFCS 1993, Proceedings

A2 - Borzyszkowski, Andrzej M.

A2 - Sokolowski, Stefan

PB - Springer

T2 - 18th International Symposium on Mathematical Foundations of Computer Science, MFCS 1993

Y2 - 30 August 1993 through 3 September 1993

ER -