Volume 3, Number 2, 136-149, DOI: 10.1007/s10270-003-0044-8

Using DAG transformations to verify Euler/Venn homogeneous and Euler/Venn FOL heterogeneous rules of inference

Nik Swoboda and Gerard Allwein

View Related Documents

Abstract

In this paper we will present a graph-transformation based method for the verification of heterogeneous first order logic (FOL) and Euler/Venn proofs. In previous work, it has been shown that a special collection of directed acyclic graphs (DAGs) can be used interchangeably with Euler/Venn diagrams in reasoning processes. Thus, proofs which include Euler/Venn diagrams can be thought of as proofs with DAGs where steps involving only Euler/Venn diagrams can be treated as particular DAG transformations. Here we will show how the characterization of these manipulations can be used to verify Euler/Venn proofs. Also, a method for verifying the use of heterogeneous Euler/Venn and FOL reasoning rules will be presented that is also based upon DAG transformations .

Keywords  Euler and Venn diagrams - Diagrammatic reasoning - Graph transformation - Proof verification

Fulltext Preview

Image of the first page of the fulltext document