A decidable constraint diagram reasoning system

Gem Stapleton, John Howse, John Taylor

Research output: Contribution to journalArticlepeer-review


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 languageEnglish
Pages (from-to)975-1008
Number of pages34
JournalJournal of Logic and Computation
Issue number6
Publication statusPublished - 1 Dec 2005


  • Visual logic
  • formal methods
  • diagrammatic reasoning


Dive into the research topics of 'A decidable constraint diagram reasoning system'. Together they form a unique fingerprint.

Cite this