1994 | ReviewPaper | Chapter
A semantic basis for logic-independent transformation
Author : Junbo Liu
Published in: Recent Trends in Data Type Specification
Publisher: Springer Berlin Heidelberg
Included in: Professional Book Archive
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
This paper is based on previous work by Harper, Sannella and Tarlecki who suggest a framework for giving semantic interpretations to logic representations in the LF logical framework. Besides LF, there are also other approaches that tackle the representation of logics in a meta-logic. The logic-independent aspect in the formal development of software has been investigated intensively based on abstract model theory. Less attention is paid to the proof system aspect. In this paper we treat logic-independence by considering the consequence relation that models a proof system for a logic. The existing work is generalized here to the consideration of any logic as a meta-logic, since there may be meta-logics other than LF that are more suitable and convenient for developing “object” logical systems. This generalized framework is then used for building logic-independent specifications and developments. The setting can eventually be considered as a firm semantic basis for developing logic-independent transformations.