Interpolation in logics with constructors

Research output: Contribution to journalArticle

3 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

Fingerprint

Interpolation
Interpolate
Formal logic
Logic
Computer science
Algebra
Horn clause
Preorder
Categorical
Computer Science
Formulation
Concepts
Framework

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Interpolation in logics with constructors. / Gǎinǎ, Daniel.

In: Theoretical Computer Science, Vol. 474, 25.02.2013, p. 46-59.

Research output: Contribution to journalArticle

@article{da71bdc323124ce6beffaa4648061482,
title = "Interpolation in logics with constructors",
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.",
author = "Daniel Gǎinǎ",
year = "2013",
month = "2",
day = "25",
doi = "10.1016/j.tcs.2012.12.002",
language = "English",
volume = "474",
pages = "46--59",
journal = "Theoretical Computer Science",
issn = "0304-3975",
publisher = "Elsevier",

}

TY - JOUR

T1 - Interpolation in logics with constructors

AU - Gǎinǎ, Daniel

PY - 2013/2/25

Y1 - 2013/2/25

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

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

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

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

U2 - 10.1016/j.tcs.2012.12.002

DO - 10.1016/j.tcs.2012.12.002

M3 - Article

AN - SCOPUS:84873730133

VL - 474

SP - 46

EP - 59

JO - Theoretical Computer Science

JF - Theoretical Computer Science

SN - 0304-3975

ER -