Heterogeneous Reasoning with Euler/Venn Diagrams Containing Named Constants and FOL

The main goal of this paper is to present the basis for a heterogeneous Euler/Venn diagram and First Order Logic (FOL) reasoning system. We will begin by defining a homogeneous reasoning system for Euler/Venn diagrams including named constants and show this system to be sound and complete. Then we will propose a heterogeneous rule of inference allowing the extraction of formulas of FOL from an Euler/Venn diagram. In defining this rule we will attempt to capture the “explicit” information content of an Euler/Venn diagram in a way similar to the Observe rule in the Hyperproof [J. Barwise, and J. Etchemendy, Hyperproof, CSLI Publications, Stanford, 1994] system. Two definitions for this heterogeneous rule will be presented, one syntactically based, which is intended to be intuitive and motivational, and a second based upon a framework employing information types to model heterogeneous reasoning previously presented [N. Swoboda, and G. Allwein, Modeling heterogeneous systems, in: Hegarty et al. [7] pp. 131–145]. Lastly we will explore the relationships between these two notions