Structuring Metatheory on Inductive Definitions

Matthews, Seán; Basin, David A.

Local TagsRelease HistoryDetailsSummary

Structuring Metatheory on Inductive Definitions

Matthews, S., & Basin, D. A. (2000). Structuring Metatheory on Inductive Definitions. Information and Computation, 162(1/2), 80-95.

Item is Released

show all hide all

Basic

show hide

Item Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-346F-B Version Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-3470-5

Genre: Journal Article

Files

show Files

Locators

show

Creators

show

hide

Creators:
Matthews, Seán¹, Author
Basin, David A.¹, Author

Affiliations:
1Programming Logics, MPI for Informatics, Max Planck Society, ou_40045

Content

show

hide

Free keywords: -

Abstract: We examine a problem for machine supported metatheory. There are statements true about a theory that are true of some (but only some) extensions; however standard theory-structuring facilities do not support selective inheritance. We use the example of the deduction theorem for modal logic and show how a statement about a theory can explicitly formalize the closure conditions extensions should satisfy for it to remain true. We show how metatheories based on inductive definitions allow theories and general metatheorems to be organized hierarchically this way, and report on a case study using the theory FS0.

Details

show

hide

Language(s): eng - English

Dates: Modified: 2010-03-12Date issued: 2000

Publication Status: Issued

Pages: -

Publishing info: -

Table of Contents: -

Rev. Type: Peer

Identifiers: eDoc: 519678
Other: Local-ID: C1256104005ECAFC-DA2CA92C2B0BE77E412566FA003F1C39-BasinMatthews98a

Degree: -

Event

show

Legal Case

show

Project information

show

Source 1

show

hide

Title: Information and Computation

Source Genre: Journal

Creator(s):

Affiliations:

Publ. Info: -

Pages: - Volume / Issue: 162 (1/2) Sequence Number: - Start / End Page: 80 - 95 Identifier: ISSN: 0890-5401