A Heterogeneous Logic with Tables

Abstract

-Correspondence tables are a basic yet widely applied graphical/diagrammatical representation method. We investigate a certain type of reasoning with tables by exploiting local conditions, which specify the data in some table entries, and global conditions, which are constraints over every row and column. To formalize such a reasoning, we introduce a heterogeneous logic with tables by combining the usual first-order formulas in the framework of natural deduction. In order to formalize tables and formulas in the same framework, we apply the syntax and semantics of many-sorted logic.

I. INTRODUCTION

Since the 1990s, logicians have studied diagrammatic and graphical representations from a formal logical viewpoint. As a result, it has been shown that they can be studied as formal objects equivalent to logical formulas. Formal syntax and semantics have been defined, logical properties of diagrammatic systems, such as soundness and completeness, have been investigated, and proof-theory has also been developed. Furthermore, studies on the characteristics of diagrammatic systems, such as their expressive power, drawing techniques, effective usage, and cognitive properties, have also been conducted. For more information on these studies, see proceedings, e.g., [10], [7], [5], of Diagrams conference series on the theory and application of diagrams.

On the basis of such research, a natural next step is to study heterogeneous reasoning, combining various diagrammatic, graphical, and sentential representations. Jon Barwise, one of the first logicians to investigate the logical status of diagrams, pointed out the importance of studying heterogeneous systems in an early work [1], and he introduced a heterogeneous system combining graphical representations and first-order formulas on a blocks world, e.g., [1], [3]. His Hyperproof project has recently been extended to the Openproof project. Heterogeneous systems based on Venn (and Euler) diagrams and first-order formulas have also been studied, e.g., [8], [11]. Furthermore, a heterogeneous system based on spider diagrams and its implementation has been developed [12].

In this paper, we study a heterogeneous system based on first-order formulas and tables. Tables and their usage have been studied in the diagrammatic reasoning community, for example, in [4], [9], [2]. Our tables are correspondence tables represented by a rectangular arrangement of given data such as symbols, characters, or numbers. Tables are one of the most basic graphical representations, and have been applied for various usages. From a cognitive science viewpoint, Shimojima [9] studied the semantic mechanism of extracting information from a given table.

In addition to the static reading of given tables, we can use tables dynamically to solve a given problem. This involves constructing a table and adding pieces of information, before manipulating, and finally reading the table. For example, let us consider a situation where we assign a working day to each of six people. We should establish a one-to-one correspondence between the six people and the working days in a week. In such a situation, we are usually given further pieces of information about who can or cannot work on specific days. We are able to solve such a problem effectively by constructing a correspondence table. (See Examples 1 and 2.) In such a problem, we are, in general, given certain constraints over the framework of the given problem such as a one-to-one correspondence between people and days, which we call global conditions, and we are also given some particular pieces of information such as information about who can or cannot work on specific days, which we call local conditions. This type of reasoning task is found, for example, in civil servant examinations in Japan and in so-called logic puzzles, and is one of the most natural reasoning that could be formalized in combination with the first-order formulas.

Barker-Plummer and Swoboda [2] discussed similar problems. They consider n-ary relationships among objects, and their system is defined to be simple and have as few rules as possible. On the other hand, we concentrate on basic tables representing the binary relationship between objects, and we design our inference rules so that we take full advantage of the effectiveness of our tables. Furthermore, our system is heterogeneous by combining tables and first-order formulas.

We propose a heterogeneous logic with tables based on Gentzen’s natural deduction. We first illustrate the type of reasoning discussed in this paper. We then introduce the syntax and semantics of our heterogeneous logic with tables, HLT. In order to formalize tables and formulas in the same framework, we apply the syntax and semantics of many-sorted logic.

II.

A HETEROGENEOUS LOGIC WITH TABLES

In Section II-A, we first specify, through some examples, the type of reasoning considered in this paper. We then define the syntax of HLT in Section II-B, and its semantics in Section II-C. We introduce the inference rules of HLT in Section II-D, and define, in Section II-E, the translation of tables into formulas. This demonstrates the soundness and completeness theorems of HLT via the theorems of many-sorted logic. A. Examples of reasoning with tables

Let us investigate the following examples of reasoning with tables, and then discuss the characteristics of such reasoning. M ⃝ ⃝ F M ⃝

T1 T ⃝ T5 ⃝ W ⃝ F ⃝ M ⃝

T2 T ⃝ T6 ⃝ W ⃝ F M ⃝

T3 T ⃝ T7 ⃝ W ⃝ F ⃝ Example 1. Consider four people a; b; c; d who are scheduled to work separately on one of Monday, Tuesday, Wednesday, and Friday. The following constraints are known: ( 1 ) ( 2 ) ( 3 ) ( 4 ) a works on Wednesday; Neither b nor c can work on Monday;

On Friday, either c or d should work.

Under these conditions, how we can arrange who works on which day? Let us first consider this problem without using tables. Note that, in addition to conditions ( 1 ), ( 2 ), and ( 3 ), we know that: There is a one-to-one correspondence between the persons and the days.

First, condition ( 1 ) states that “a works on Wednesday.” Thus, by ( 4 ), we find that “a does not work on Monday.” Then, by combining this with ( 2 ) and ( 4 ), we find that “d works on Monday.”

In the given situation, conditions ( 3 ) and ( 4 ) imply the following (in fact, under ( 4 ), conditions ( 3 ) and ( 5 ) are equivalent): ( 5 ) “a does not work on Friday, and b does not work on Friday.” Because we have already determined that “d works on Monday,” ( 4 ) implies that “d does not work on Friday.” Then, as the above facts can be combined to give that “Neither a nor b nor d works on Friday,” we find by ( 4 ) that “c works on Friday.”

As for b, because we already know that “a works on Wednesday,” “c works on Friday,” and “d works on Monday,” we have from ( 4 ) that “b works on Tuesday.”

In this way, we are able to determine the working day of a; b; c; d.

Note that in the above reasoning, the condition ( 4 ) is necessary to derive any piece of information. Further note that there are various ways to solve the above problem. For example, in the above solution, we converted condition ( 3 ) with disjunction into ( 5 ) without disjunction. Alternatively, we could have divided ( 3 ) into two cases, and examined each case individually.

Next, let us solve the same problem using a correspondence table. We construct a table in which the rows are labeled according to the workers a; b; c; d, and the columns are labeled by days, M (for Monday), T (for Tuesday), W (for Wednesday), and F (for Friday). Based on the given conditions ( 1 ), ( 2 ), and ( 3 ), we insert ⃝ into each entry (x; Y ) for which “x works on Y ” holds, and insert when “x does not work on Y ” holds. Thus, we obtain the table T0 shown in Fig. 1. Note that we applied condition ( 5 ) (stated previously) instead of the given condition ( 3 ). In terms of tables, condition ( 4 ) is divided into the following two conditions: ( 6 ) ( 7 )

In each row, exactly one entry should be marked as ⃝, and the other entries should be ; In each column, exactly one entry should be marked as ⃝, and the other entries should be .

Thus, from the fact that the (a; W )-entry is ⃝ and ( 6 ), we find that the (a; M ); (a; T ) entries are , as illustrated in T1. Similarly, because the (a; M ); (b; M ); (c; M ) entries are all , we find that (d; M ) must be ⃝ by ( 7 ), as illustrated in T2.

Hence, by successively applying conditions ( 6 ) and ( 7 ), we finally get the complete table T7. From this, we can read off complete information about the working day of a; b; c; d.

Although all entries are either ⃝ or in the above example, in general, some entries may not be determined. For example, if we remove condition ( 3 ), we obtain a partial table in which (b; T ); (b; F ); (c; T ); (c; F ) remain indeterminate.

Let us consider another example, in which the number of days worked by each person and the number of people working on a given day are changed from Example 1.

Example 2. Each person should work exactly two days, and exactly two people should work on each day. Conditions ( 1 ) and ( 2 ) are the same as in Example 1. Condition ( 3 ) is replaced by: ( 8 ) On Friday, c and d should work together. In this case, how can we arrange the allocation of working days to a; b; c; d? Using tables, we are able to apply essentially the same strategy as for Example 1. Note that conditions ( 6 ) and ( 7 ) in Example 1 become the following: ( 9 ) ( 10 )

In each row, exactly two entries should be marked as ⃝, and the other entries should be ; In each column, exactly two entries should be marked as ⃝, and the other entries should be . M ⃝ ⃝

T8 ⃝ ⃝ ⃝ F ⃝ ⃝ ⃝ ⃝ M ⃝ ⃝ T9 T ⃝ T13 ⃝ W ⃝ ⃝ ⃝ ⃝

F ⃝ ⃝ ⃝ ⃝ M ⃝ ⃝ ⃝ T10

T ⃝ ⃝ T14

W ⃝ ⃝

F ⃝ ⃝ ⃝ ⃝ M ⃝ ⃝

T ⃝ ⃝ T15

W ⃝ ⃝ ⃝ ⃝ F ⃝ ⃝ We begin with the table T8 in Fig. 2. Because the (b; M ); (c; M ) entries are , we find, by ( 10 ), that (a; M ); (d; M ) are ⃝, as illustrated in T9. In a similar way, we obtain T10. Then, because the entries of (a; M ); (a; W ) are ⃝, we find, by ( 9 ), that (a; T ) is , as in T11, and in a similar way to Example 1, we finally obtain table T15.

In the above examples, although the number of ⃝ is fixed to be the same (i.e., one or two) in every row and column, this is not necessarily the case. We do not assume such a restriction in our formalization of reasoning with tables.

By investigating Examples 1 and 2, we find that there are two types of condition in our problems. One is a “constraint over the framework of a given problem” (e.g., condition ( 4 ) above), and we call these global conditions. In view of tables, our global conditions are constraints over every row and column. The other type is a “specific condition for each object” (e.g., ( 1 ) above), and we call these local conditions. In view of tables, local conditions specify only particular entries. Our reasoning with tables is essentially conducted by combining global conditions and local conditions.

One of the remarkable facts of our reasoning with tables is that, even if the given local and global conditions change, we are able to apply essentially the same strategy: that is, we check each row or column, and apply appropriate global conditions controlling rows and columns. Thus, based on the local and global conditions, our reasoning using tables is conducted as follows.

(I) (II) (III) (IV)

We decompose, if necessary, the given conditions into local conditions (i.e., atomic sentences or their negation, such as “a does not work on Friday” and “b does not work on Friday”) by applying logical laws (e.g., ( 3 ) ^ ( 4 ) ! ( 5 )).

We construct a correspondence table using these local conditions (e.g., T0).

By applying the global conditions, that is, by exploiting constraints over the number of ⃝ or in a row or column, we further insert ⃝ and into the table.

Finally, we extract information from the table.

Although most of the given conditions in the above examples are already local conditions, more complex conditions may generally be given. In such cases, we frequently apply item (I) in the above procedure. Furthermore, a given condition, such as an implicational sentence, may be decomposed using basic information obtained from item (III). In these complex cases, we must repeat the whole procedure several times.

Thus, a natural system of formalizing our reasoning with tables is a heterogeneous logical system combining tables and first-order formulas. Our formalization here is based on Gentzen’s natural deduction.

B. Syntax of HLT

In order to formalize our heterogeneous reasoning with tables, we adopt two-sorted logic, in which constants and variables of the first-order language are divided into two sorts: sorts of row and column. Although usually distinguished explicitly by sort symbols in many-sorted logic, we distinguish the two by lower- and uppercase letters: a constant (resp. variable) of the row sort is denoted by a (resp. x), and that of the column sort is denoted by A (resp. X). (See, for example, [6] for many-sorted logic.) Then, by ⃝(a; B) we mean “a and B are in a certain positive relation.” Thus, sentences such as “a is B,” “a matches B,” and “a corresponds to B” are all expressed as ⃝(a; B).

We begin by specifying some vocabulary.

Definition 3 (Vocabulary). We use the following symbols.

Row-constants: a1; a2; : : : ; Col-constants: A1; A2; : : : Row-variables: x1; x2; : : : ; Col-variables: X1; X2; : : : Predicate: ⃝( ; ) Constants and variables are collectively called terms, and are denoted by s; t; u; : : : .

Using the above symbols, we construct our formulas as follows.

Definition 4. An atomic formula is of the form ⃝(s; t) for a row-constant/variable s and a col-constant/variable t. Based on atomic formulas, complex formulas are defined inductively as usual: φ := ⃝(s; t) φ ^ φ φ _ φ φ ! φ :φ In particular, we denote the negation of an atom :⃝(s; t) by (s; t). Formulas of the forms ⃝(s; t) and (s; t) are collectively called literals. Literals containing no variables are called ground literals (or closed literals), and they are denoted by ; 1; 2; : : : . We denote by the ground literal (a; B) when is ⃝(a; B), and ⃝(a; B) when is (a; B). Formulas containing no free variables are said to be closed.

We sometimes write ⃝(s; t) as t(s), and (s; t) as :t(s). ∨ ( 2Sn 2Sn

In order to express sentences of the form “among n objects, there are exactly i objects that are A,” we introduce a kind of counting quantifier, and write the sentence as 9i=nx:A(x), i.e., 9i=nx:⃝(x; A).

Definition 5 (Global formula). For fixed sets of row-constants R = fa1; : : : ; ang or of col-constants C = fA1; : : : ; Ang, the following forms of formulas are called global formulas: For any A and a, 9i=nx 2 R:A(x); 9i=nX 2 C:X(a); 9i=nx 2 R::A(x); 9i=nX 2 C::X(a): If a set of constants is clear from the context, it is abbreviated as 9i=nx:A(x).

Global formulas are simply abbreviations of the appropriate first-order formulas. Let be a permutation of the given row-constants a1; : : : ; an, and Sn be the set of all their permutations. We then define 9i=nx 2 R:A(x) as: A(a 1) ^ ^ A(a i) ^ :A(a i+1) ^ ^ :A(a n) ) We treat 9i=nx 2 R::A(x) in a similar manner.

Let be a permutation of the given col-constants A1; : : : ; An, and Sn be the set of all their permutations. We then define 9i=nX 2 C:X(a) as: ∨ ( ) A 1(a) ^ ^ A i(a) ^ :A i+1(a) ^ ^ :A n(a) We again treat 9i=nX 2 C::X(a) similarly.

Example 6. For example, for some row-constant a and col-constants C = fA1; A2; A3g, the global formula 92=3X 2 C:X(a) is the abbreviation of the following formula: ( ( (

A1(a) ^ A2(a) ^ :A3(a)

_ A1(a) ^ A3(a) ^ :A2(a)

_ A2(a) ^ A3(a) ^ :A1(a) ) ) ) where we omit trivial permutations such as A2(a) ^ A1(a) ^ :A3(a), which is equivalent to the first disjunct in the above.

Next, we define our tables.

Definition 7. A table T is an m n-matrix over symbols f⃝; ; bg; that is, a rectangular arrangement of the symbols, in which rows are labeled by distinct row-constants a1; : : : ; am and columns are labeled by distinct col-constants A1; : : : ; An. In a specific representation of a table, we usually omit the symbol “b” and leave the entry blank.

Remark 8. A table T is abstractly defined as the function T : R C ! f⃝; ; bg, where R (resp. C) is some finite set of row-constants (resp. col-constants) of T .

Note that no entry can be marked with more than one of ⃝; ; b at the same time.

As usual, any pair of tables, say T1 and T2, are identical if they consist of the same constants, and if the ⃝, marks of all entries in T1 and T2 are also identical. This is formally defined as follows.

Definition 9 (Equivalence of tables). A table T1 is a subtable of T2, written as T1 T2, when: all row- and col-constants of T1 are also those of T2; for any (ai; Aj )-entry of T1: if it is ⃝ in T1, it is also ⃝ in T2, and if it is in T1, it is also in T2.

T1 and T2 are (syntactically) equivalent when T1 T2 T1 hold.

T2 and

Note that, by definition, two specific tables that differ only in the orders of their rows and columns are equivalent.

C. Semantics of HLT

We now define the semantics of our HLT as a particular case of the semantics of many-sorted logic. (See [6] for the semantics of many-sorted logic.) Definition 10. A structure M is (Mrow; Mcol; I), where: Mrow and Mcol are disjoint non-empty domains for the row and column sorts, respectively.

I is an interpretation function such that:

I(a) 2 Mrow for each row-constant a; I(A) 2 Mcol for each col-constant A; I(⃝)

Mrow

Mcol.

Definition 11. A valuation v in M is a function that assigns every row-variable x an entity of Mrow, i.e., v(x) 2 Mrow, and every col-variable X an entity of Mcol, i.e., v(X) 2 Mcol.

Definition 12 (Truth conditions). The notion of satisfaction of a formula φ in a structure M with a valuation v, written M j= φ[v], is defined inductively as follows:

M j= ⃝(s; t)[v] if and only if (I(s)[v]; I(t)[v]) 2 I(⃝), where I(s)[v] = I(a) when s is a row-constant a, and I(s)[v] = v(x) when s is a row-variable x; Similarly for t; M j= :φ[v] if and only if M ̸j= φ[v];

Truth conditions for other connectives ^; _; ! are defined as usual; M j= 8x:φ[v] if and only if, for all m 2 Mrow, M j=

φ[v(x 7! m)], :E . . . .

?φ ?E . . .

.

8X:φ φ[X := t] 8Ec . . .

. ! I; n

^I where, in 8Ir (and 8Ic), the variable x (resp. X) may not occur free in any open hypothesis on which φ depends; in 8Er (and 8Ec), t is a row-variable/constant (resp. col-variable/constant). . . .

. φ[x := t] 9x:φ 9Ir . . .

. φ[X := t] 9X:φ 9Ic . . .

. 9x:φ where, in 9Ir (and 9Ic), t is a row-variable/constant (resp. col-variable/constant); in 9Er (and 9Ec), x (resp. X) may not occur free in nor in any open hypothesis on which depends, except in φ. where v(x 7! m) is the valuation that is exactly the same as v except for x, and x is assigned to m; M j= 8X:φ[v] if and only if, for all m 2 Mcol, M j=

φ[v(X 7! m)]; M j= 9x:φ[v] if and only if there exists m 2 Mrow such

that M j= φ[v(x 7! m)]; M j= 9X:φ[v] if and only if there exists m 2 Mcol such

that M j= φ[v(X 7! m)]; M j= T for a table T if and only if M j= ⃝(s; t) for any entry (s; t) of T that is ⃝, and M j= (s; t) for any entry (s; t) of T that is .

M is said to be a model of φ, written as M j= φ, when M j= φ[v] holds for any valuation v in M .

The semantic consequence relation in our HLT is defined as follows.

Definition 13 (Semantic consequence). Let be a set of closed formulas, let G be a set of global formulas, and let T be a table.

A closed formula φ is said to be a semantic consequence of

; G; T , written as ; G; T j= φ, when any model of , G, and T is also a model of φ.

D. Inference rules of HLT

In this section, we introduce the inference rules of HLT, which consist of the usual natural deduction rules for formulas and rules of table manipulation.

Definition 14 (Inference rules). The inference rules of HLT consist of the following rules for formulas and rules for tables. _E; n Rules for formulas are the rules for ^; _; !; :; 8; 9, and ?E and RAA listed in Fig. 3.

Rules for tables are the following in; row; col; ext rules: : : :

Ai : : : : : :

Ai : : : : : :

⃝(a; Ai) in⃝ Ai : : : : : :

(a; Ai) in

Ai : : : a a In order to describe the same types of rules, we use the symbol , which denotes either ⃝ or . Furthermore, denotes ⃝ if is , and denotes if is ⃝. The following four rules of row and col are duplicated depending on whether is ⃝ or .

Let be a permutation of columns A1; : : : ; An. Under the permutation, we assume that entries marked as ⃝ and those marked as are grouped.

A 1 : : :

row

Let be a permutation of rows a1; : : : ; am. Under the permutation , we assume that entries marked as ⃝ and those marked as are grouped.

a A ... □ ...

□ a 1

... a j a j+1

... a m 9j=mx: (A; x)

A a 1

... ... a j a j+1

... ...

a m where each □ is blank or . col 9j=mx: (A; x)

E. Translation of tables

T ∧f⃝(aj ; Ai) j (aj ; Ai) is ⃝ in T g ^ ∧f (aj ; Ai) j (aj ; Ai) is

The in-rule enables us to convert ground literals into a table, and, conversely, the ext-rule enables us to convert a table into a conjunction of literals. The row and col rules pertain to the manipulation of tables.

The notion of proof is defined inductively as usual in natural deduction.

Definition 15. Let be a set of closed formulas, let G be a set of global formulas, and let T be a table. A closed formula φ is provable from ; G; T , written as ; G; T ⊢ φ, when there exists a proof of φ from the open assumption ; G; T . Example 16. A proof in HLT of Example 1 is given in Fig. 4.

We give a translation of the rules for tables into those for usual natural deduction without tables, from which the soundness and completeness theorems of HLT are obtained.

We first define the following terminology.

Definition 17. A conjunction of literals is said to be consistent when it has a model.

We define the translation of tables into a formula. This is completely parallel to the ext-rule of HLT. 92=3X:X(a)

^E :E ? :A3 ?E

_E; 1

Conversely, it is easily seen that, for any consistent conjunction of ground literals, there exists a corresponding table. Thus, we may regard a table T and a consistent conjunction L of ground literals to be interchangeable, and (slightly abusing our notation) we write, for example, L T .

Based on the translation of tables, we give a translation of table manipulations into rules of natural deduction. (See also Example 20 below.) Theorem 19 (Translation). If G; T1 ⊢ T2 with only row and col rules in HLT, then G; T1◦ ⊢ T2◦ in natural deduction without tables.

Proof: It is sufficient to give a translation of row and col rules into combinations of rules of natural deduction without tables.

Because all cases are treated in a similar way, we show only the following row -rule (we assume that all □ of the rule are blank for simplicity). a

A 1 : : : ⃝ : : :

A i ⃝

From our translation of tables, the table in the premises of the row -rule is translated into A 1(a) ^ ^ A i(a). Note also that another premise of the row -rule 9i=nX:X(a) is ∨ 2Sn (A 1(a) ^ ^ A i(a) ^ :A i+1(a) ^ ^ :A n(a)). Given these two formulas, we construct a natural deduction proof.

We denote by A i the conjunction A 1(a) ^ ^ A i(a), and by :A n the conjunction :A i+1(a) ^ ^ :A n(a). Then, we can write 9i=nX:X(a) as ∨ 2Sn (A i ^ :A n).

In order to apply the _E-rule of natural deduction, we divide the following cases according to the form of each disjunct A i ^ :A n of the above 9i=nX:X(a), and we derive :A n in each case.

1) 2)

When = , or when A i $ A i holds, we apply the ^E-rule of natural deduction to A i ^ :A n to obtain :A n, which is equivalent to :A n.

Otherwise, we apply the ^E-rule to A i ^ :A n, and obtain :A n. Note that at least one of the conjuncts of :A n contradicts a conjunct of A i by the definition of the permutation for 9i=nX:X(a).

Hence, by applying the ?E-rule, we obtain :A n. Therefore, in every case, we obtain :A n from A i ^ :A n. Thus, by applying the _E-rule, we obtain a proof of :A n.

As we have A i by the initial assumption, by applying the ^I-rule, we obtain A i ^ :A n, which is the translation of the conclusion of the given row -rule.

Example 20. Let us consider the following application of the row -rule: a

A1 ⃝

A2 ⃝ a

A3 A1 ⃝

A2 ⃝ 92=3X:X(a) A3 row Note that 92=3X:X(a) := (A1 ^ A2 ^ :A3) _ (A1 ^ A3 ^ :A2) _ (A2 ^ A3 ^ :A1), where we abbreviate Ai(a) as Ai and omit trivial permutations. This application of the row rule is translated as in Fig. 5.

The soundness of HLT is obtained straightforwardly by the above theorem of translation, because each rule for tables is translated into a combination of rules for formulas by Theorem 19, and each rule for formulas, i.e., of many-sorted logic, is known to be sound.

Theorem 21 (Soundness of HLT). Let be a set of closed formulas, G be a set of global formulas, T be a table, and φ be a closed formula. If ; G; T ⊢ φ in HLT, then ; G; T j= φ.

Because our inference rules and semantics of HLT “without tables” are just particular cases of those of many-sorted logic, the following completeness theorem of HLT holds via the theorem of many-sorted logic. (See [6] for the completeness of many-sorted logic.) Theorem 22 (Completeness of HLT). Let be a set of closed formulas, G be a set of global formulas, T be a table, and φ be a closed formula. If ; G; T j= φ, then ; G; T ⊢ φ in HLT.

Proof: Based on the translation of tables, a table T and the consistent set of ground literals T ◦ are equivalent. Thus, ; G; T j= φ is equivalent to ; G; T ◦ j= φ. Then, by the completeness theorem of many-sorted logic, we have ; G; T ◦ ⊢ φ. Again, by the translation (more precisely, by the ext-rule of HLT for T ), we have ; G; T ⊢ φ in HLT.

III.

CONCLUSION AND FUTURE WORK

We investigated reasoning with tables by exploiting local and global conditions. This type of reasoning is not just a mere puzzle, but can be applied to simple scheduling problems. In order to formalize our reasoning with tables, we introduced a heterogeneous logic with tables, HLT, with a combination of first-order formulas. For the formalization of HLT, we applied the syntax and semantics of many-sorted logic. Although we actually applied two-sorted logic, as we studied the most basic binary relationship between objects, our system can be extended to cover the n-ary relationship between objects, as in [2], by applying the general many-sorted logic.

We defined inference rules for HLT that consist of the usual natural deduction rules for the first-order formulas and table manipulation rules. These were designed to reflect our intuitive and effective manipulation of the tables. We investigated the translation of tables and their manipulations into formulas and natural deduction inference rules. Then, based on these translations, we obtained soundness and completeness theorems of HLT by reducing them to the usual many-sorted logic theorems.

In this paper, for the sake of simplicity, we concentrated on the most basic global formulas, such as “among n objects, there are ‘exactly i objects’ . . . .” Our system can be easily extended by introducing the following forms for the global formulas: 9 i=nx:A(x) meaning “among n objects, there are ‘at most’ i objects that are A,” and 9 i=nx:A(x) meaning “among n objects, there are ‘at least’ i objects that are A.” Similarly, we could consider 9 i=nX:X (a) and 9 i=nX:X (a), as well as negative literals. These formulas are also just abbreviations of appropriate first-order formulas, similar to the definition of 9i=n in Section II-B.

Based on the informal analysis of Examples 1 and 2 and the translation between tables and formulas (Theorem 19 and Example 20), we may point out the following differences, for example, between the usual sentential systems and our table system. ( 1 ) In a sentential system, on the one hand, we need to derive each statement corresponding to an entry of a table one by one. On the other hand, in our table system, by an application of our rule, a number of entries are filled with ⃝ or at once, that is, a number of statements are derived at once. This suggests that the number of steps of inference is reduced by our row and col rules as illustrated in Example 20. ( 2 ) However, the above difference appears in a fragment where our tables and row and col rules work most effectively. In other words, our table fragment of HLT, consisting only of rules for tables (row; col; in; ext rules) without rules for formulas, is not complete with respect to our semantics. That is, there exists a formula which is semantically valid, but is not provable with only rules for tables. In contrast, the natural deduction system without tables is complete, and there are no restriction on a given problem. ( 3 ) Once a table is constructed, and sentences are translated into the table (for example, “a works on Wednesday (W (a))” is translated as “(a; W )-entry is ⃝,” and “exactly one person should work on Wednesday (91=4x:W (x))” is translated as “there is exactly one ⃝ in column W ”), reasoning with the table is conducted by completely graphical or geometrical manipulations on the table, i.e., by dealing only with the number of ⃝; symbols in each row and column. Furthermore, there are two ways, in a sentential system, to derive a statement, say “d works on Monday (M (d))”: deriving M (d) from :M (a); :M (b); :M (c) by checking every person on Monday, and from :T (d); :W (d); :F (d) by checking every possible working day of d. These derivations correspond, in our table system, to an application of col rule and row rule, respectively.

These comparison between sentential systems and our table system should be investigated by combining logic and cognitive science methods.

References

[1] Gerard Allwein and Jon Barwise, eds., Logical reasoning with diagrams , Oxford Studies In Logic And Computation Series , 1996 .

[2] Dave Barker-Plummer and Nik Swoboda, Reasoning with coincidence grids-A sequent-based logic and an analysis of complexity , Journal of Visual Languages and Computing , 22 ( 1 ), 56 - 65 , 2011 .

[3] Jon Barwise and John Etchemendy , A Computational Architecture for Heterogeneous Reasoning , Proceedings of the Seventh Conference on Theoretical Aspects of Rationality and Knowledge , 1 - 14 , 1998 .

[4] Jon Barwise and Eric Hammer, Diagrams and the concept of logical system, in Logical reasoning with diagrams, G. Allwein and J. Barwise, eds., Oxford Studies In Logic And Computation Series , 1996 .

[5] Philip T. Cox , Beryl Plimmer, Peter Rodgers eds., Diagrammatic Representation and Inference: 7th International Conference, Diagrams 2012, Lecture Notes in Computer Science , Vol. 7352 , 2012 .

[6] Herbert B. Enderton , A Mathematical Introduction to Logic, Second Edition, Academic Press, 2000 .

[7] Ashok K. Goel , Mateja Jamnik, N. Hari Narayanan eds., Diagrammatic Representation and Inference: 6th International Conference, Diagrams 2010, Lecture Notes in Computer Science , Vol. 6170 , 2010 .

[8] Eric Hammer , Reasoning with Sentences and Diagrams , Notre Dame Journal of Formal Logic , Volume 35 , Number 1 , 73 - 87 , 1994 .

[9] Atsushi Shimojima , The Inferential-Expressive Trade-Off: A Case Study of Tabular Representations, Diagrams 2002 , 116 - 130 , 2002 .

[10] Gem Stapleton , John Howse, John Lee Eds., Diagrammatic Representation and Inference: 5th International Conference, Diagrams 2008, Lecture Notes in Computer Science , Vol. 5223 , 2008 .

[11] Nik Swoboda and Gerard Allwein , Heterogeneous Reasoning with Euler/Venn Diagrams Containing Named Constants and FOL , Electronic Notes in Theoretical Computer Science, 134 , 153 - 187 , 2005 .

[12] Matej Urbas and Mateja Jamnik , Heterogeneous Proofs: Spider Diagrams Meet Higher-Order Provers , Interactive Theorem Proving, Lecture Notes in Computer Science , Volume 6898 , 376 - 382 , 2011 .