### 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 | |

Publication status | Published - 1 Dec 2005 |

### Keywords

- Visual logic
- formal methods
- diagrammatic reasoning

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

## Cite this

Stapleton, G., Howse, J., & Taylor, J. (2005). A decidable constraint diagram reasoning system.

*Journal of Logic and Computation*,*15*(6), 975-1008. https://doi.org/10.1093/logcom/exi041