Using DAG Transformations to Verify Euler/Venn Homogeneous and Euler/Venn FOL Heterogeneous Rules of Inference
Nik Swoboda, Gerard Allwein · Electronic Notes in Theoretical Computer Science · 2003
In this paper we will present a graph-transformation based method for the verification of heterogeneous first order logic (FOL) and Euler/Venn proofs. It has been shown that a special collection of directed acyclic graphs (DAGs) can be used interchangeably with Euler/Venn diagrams in reasoning processes [4]. 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. In the work reported 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.