Author name cluster

Seán Matthews

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

1 paper

1 author row

I&C Journal 2000 Journal Article

Structuring Metatheory on Inductive Definitions

David Basin
Seán Matthews

We examine a problem for machine supported metatheory. There are true statements 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 this way and report on a case study using the theory FS0.

Details DOI