Interpolation in logics with constructors

Research output: Contribution to journalArticle

5 Citations (Scopus)

Abstract

We present a generic method for establishing the interpolation property by borrowing it across the logical systems from a base institution to prove it for its constructor-based variant. The framework used is that of the so-called institution theory invented by Goguen and Burstall which is a categorical-based formulation of the informal concept of logical system sufficiently abstract to capture many examples of logics used in computer science and mathematical logic, and expressive enough to elaborate our general results. We illustrate the applicability of the present work by instantiating the abstract results to constructor-based Horn clause logic and constructor-based Horn preorder algebra but applications are also expected for many other logical systems.

Original languageEnglish
Pages (from-to)46-59
Number of pages14
JournalTheoretical Computer Science
Volume474
DOIs
Publication statusPublished - Feb 25 2013
Externally publishedYes

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Interpolation in logics with constructors'. Together they form a unique fingerprint.

  • Cite this