A normal form for Euler diagrams with shading

Andrew Fish, Chris John, John Taylor

Research output: Chapter in Book/Conference proceeding with ISSN or ISBNConference contribution with ISSN or ISBNpeer-review

Abstract

In logic, there are various normal forms for formulae; for example, disjunctive and conjunctive normal form for formulae of propositional logic or prenex normal form for formulae of predicate logic. There are algorithms for ‘reducing’ a given formula to a semantically equivalent formula in normal form. Normal forms are used in a variety of contexts including proofs of completeness, automated theorem proving, logic programming etc. In this paper, we develop a normal form for unitary Euler diagrams with shading. We give an algorithm for reducing a given Euler diagram to a semantically equivalent diagram in normal form and hence a decision procedure for determining whether two Euler diagrams are semantically equivalent. Potential applications of the normal form include clutter reduction and automated theorem proving in systems based on Euler diagrams.
Original languageEnglish
Title of host publicationProceedings of the 5th International Conference on the Theory and Application of Diagrams
Place of PublicationBerlin Heidelberg
PublisherSpringer-Verlag
Pages206-221
Number of pages16
Volume5223
ISBN (Electronic)9783540877301
ISBN (Print)9783540877295
DOIs
Publication statusPublished - 1 Jan 2008
EventProceedings of the 5th international conference on the theory and application of diagrams - Herrsching, Germany, 19-21 September, 2008
Duration: 1 Jan 2008 → …

Publication series

NameLecture Notes in Computer Science

Conference

ConferenceProceedings of the 5th international conference on the theory and application of diagrams
Period1/01/08 → …

Fingerprint

Dive into the research topics of 'A normal form for Euler diagrams with shading'. Together they form a unique fingerprint.

Cite this