Constructor-based logics

Daniel Mircea Gaina, Kokichi Futatsugi, Kazuhiro Ogata

Research output: Contribution to journalArticle

12 Citations (Scopus)

Abstract

Many computer science applications concern properties that are true for a restricted class of models. In this paper, a couple of constructor-based institutions are presented. These institutions are defined on top of some base institutions, roughly speaking, by enhancing the syntax with constructor symbols and restricting the semantics to models with elements that are reachable by constructors. The proof rules for the constructor-based Horn logics, formalized as institutions, are defined in this paper, and a proof of completeness is provided in the abstract framework of institutions.

Original languageEnglish
Pages (from-to)2204-2233
Number of pages30
JournalJournal of Universal Computer Science
Volume18
Issue number16
Publication statusPublished - Dec 1 2012

Fingerprint

Logic
Completeness
Computer Science
Model
Computer science
Semantics
Syntax
Class
Framework

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Gaina, D. M., Futatsugi, K., & Ogata, K. (2012). Constructor-based logics. Journal of Universal Computer Science, 18(16), 2204-2233.

Constructor-based logics. / Gaina, Daniel Mircea; Futatsugi, Kokichi; Ogata, Kazuhiro.

In: Journal of Universal Computer Science, Vol. 18, No. 16, 01.12.2012, p. 2204-2233.

Research output: Contribution to journalArticle

Gaina, DM, Futatsugi, K & Ogata, K 2012, 'Constructor-based logics', Journal of Universal Computer Science, vol. 18, no. 16, pp. 2204-2233.
Gaina DM, Futatsugi K, Ogata K. Constructor-based logics. Journal of Universal Computer Science. 2012 Dec 1;18(16):2204-2233.
Gaina, Daniel Mircea ; Futatsugi, Kokichi ; Ogata, Kazuhiro. / Constructor-based logics. In: Journal of Universal Computer Science. 2012 ; Vol. 18, No. 16. pp. 2204-2233.
@article{e5111bca0c59438ca5d210f981ac9883,
title = "Constructor-based logics",
abstract = "Many computer science applications concern properties that are true for a restricted class of models. In this paper, a couple of constructor-based institutions are presented. These institutions are defined on top of some base institutions, roughly speaking, by enhancing the syntax with constructor symbols and restricting the semantics to models with elements that are reachable by constructors. The proof rules for the constructor-based Horn logics, formalized as institutions, are defined in this paper, and a proof of completeness is provided in the abstract framework of institutions.",
author = "Gaina, {Daniel Mircea} and Kokichi Futatsugi and Kazuhiro Ogata",
year = "2012",
month = "12",
day = "1",
language = "English",
volume = "18",
pages = "2204--2233",
journal = "Journal of Universal Computer Science",
issn = "0948-695X",
publisher = "Springer Verlag",
number = "16",

}

TY - JOUR

T1 - Constructor-based logics

AU - Gaina, Daniel Mircea

AU - Futatsugi, Kokichi

AU - Ogata, Kazuhiro

PY - 2012/12/1

Y1 - 2012/12/1

N2 - Many computer science applications concern properties that are true for a restricted class of models. In this paper, a couple of constructor-based institutions are presented. These institutions are defined on top of some base institutions, roughly speaking, by enhancing the syntax with constructor symbols and restricting the semantics to models with elements that are reachable by constructors. The proof rules for the constructor-based Horn logics, formalized as institutions, are defined in this paper, and a proof of completeness is provided in the abstract framework of institutions.

AB - Many computer science applications concern properties that are true for a restricted class of models. In this paper, a couple of constructor-based institutions are presented. These institutions are defined on top of some base institutions, roughly speaking, by enhancing the syntax with constructor symbols and restricting the semantics to models with elements that are reachable by constructors. The proof rules for the constructor-based Horn logics, formalized as institutions, are defined in this paper, and a proof of completeness is provided in the abstract framework of institutions.

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

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

M3 - Article

VL - 18

SP - 2204

EP - 2233

JO - Journal of Universal Computer Science

JF - Journal of Universal Computer Science

SN - 0948-695X

IS - 16

ER -