A decidable constraint diagram reasoning system

Gem Stapleton; John Howse; John Taylor

doi:10.1093/logcom/exi041

A decidable constraint diagram reasoning system

Gem Stapleton, John Howse, John Taylor

University of Brighton

Research output: Contribution to journal › Article › peer-review

Abstract

Constraint diagrams are a visual notation designed for use by software engineers to formally specify information systems. In this paper we formalize a fragment of the constraint diagram language. A set of reasoning rules are defined and we prove that this set is both sound and complete. Given constraint diagrams D_1 and D_2 such that D_2 is a semantic consequence of D_1, to prove completeness we construct a proof of D_2 from D_1. A decision procedure can be extracted from this proof construction process and it follows that the system is decidable

Original language	English
Pages (from-to)	975-1008
Number of pages	34
Journal	Journal of Logic and Computation
Volume	15
Issue number	6
DOIs	https://doi.org/10.1093/logcom/exi041
Publication status	Published - 1 Dec 2005

Keywords

Visual logic
formal methods
diagrammatic reasoning

Access to Document

10.1093/logcom/exi041Licence: Unspecified

http://logcom.oxfordjournals.org/content/15/6/975.abstract%22Licence: Unspecified

Cite this

@article{f938406783144305a2ff848d9f3c39c1,

title = "A decidable constraint diagram reasoning system",

abstract = "Constraint diagrams are a visual notation designed for use by software engineers to formally specify information systems. In this paper we formalize a fragment of the constraint diagram language. A set of reasoning rules are defined and we prove that this set is both sound and complete. Given constraint diagrams D_1 and D_2 such that D_2 is a semantic consequence of D_1, to prove completeness we construct a proof of D_2 from D_1. A decision procedure can be extracted from this proof construction process and it follows that the system is decidable",

keywords = "Visual logic, formal methods, diagrammatic reasoning",

author = "Gem Stapleton and John Howse and John Taylor",

year = "2005",

month = dec,

day = "1",

doi = "10.1093/logcom/exi041",

language = "English",

volume = "15",

pages = "975--1008",

journal = "Journal of Logic and Computation",

issn = "0955-792X",

number = "6",

}

TY - JOUR

T1 - A decidable constraint diagram reasoning system

AU - Stapleton, Gem

AU - Howse, John

AU - Taylor, John

PY - 2005/12/1

Y1 - 2005/12/1

N2 - Constraint diagrams are a visual notation designed for use by software engineers to formally specify information systems. In this paper we formalize a fragment of the constraint diagram language. A set of reasoning rules are defined and we prove that this set is both sound and complete. Given constraint diagrams D_1 and D_2 such that D_2 is a semantic consequence of D_1, to prove completeness we construct a proof of D_2 from D_1. A decision procedure can be extracted from this proof construction process and it follows that the system is decidable

AB - Constraint diagrams are a visual notation designed for use by software engineers to formally specify information systems. In this paper we formalize a fragment of the constraint diagram language. A set of reasoning rules are defined and we prove that this set is both sound and complete. Given constraint diagrams D_1 and D_2 such that D_2 is a semantic consequence of D_1, to prove completeness we construct a proof of D_2 from D_1. A decision procedure can be extracted from this proof construction process and it follows that the system is decidable

KW - Visual logic

KW - formal methods

KW - diagrammatic reasoning

U2 - 10.1093/logcom/exi041

DO - 10.1093/logcom/exi041

M3 - Article

SN - 0955-792X

VL - 15

SP - 975

EP - 1008

JO - Journal of Logic and Computation

JF - Journal of Logic and Computation

IS - 6

ER -

A decidable constraint diagram reasoning system

Abstract

Keywords

Access to Document

Fingerprint

Cite this