A Heterogeneous Logic with Tables (Extended Abstract) Ryo Takemura Nihon University, Japan Email: takemura.ryo@nihon-u.ac.jp Abstract—Correspondence tables are a basic yet widely ap- In addition to the static reading of given tables, we can plied graphical/diagrammatical representation method. We in- use tables dynamically to solve a given problem. This involves vestigate a certain type of reasoning with tables by exploiting constructing a table and adding pieces of information, before local conditions, which specify the data in some table entries, manipulating, and finally reading the table. For example, let us and global conditions, which are constraints over every row consider a situation where we assign a working day to each of and column. To formalize such a reasoning, we introduce a heterogeneous logic with tables by combining the usual first-order six people. We should establish a one-to-one correspondence formulas in the framework of natural deduction. In order to between the six people and the working days in a week. formalize tables and formulas in the same framework, we apply In such a situation, we are usually given further pieces of the syntax and semantics of many-sorted logic. 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 I. I NTRODUCTION problem, we are, in general, given certain constraints over the framework of the given problem such as a one-to-one Since the 1990s, logicians have studied diagrammatic and correspondence between people and days, which we call global graphical representations from a formal logical viewpoint. As conditions, and we are also given some particular pieces of a result, it has been shown that they can be studied as formal information such as information about who can or cannot objects equivalent to logical formulas. Formal syntax and se- work on specific days, which we call local conditions. This mantics have been defined, logical properties of diagrammatic type of reasoning task is found, for example, in civil servant systems, such as soundness and completeness, have been in- examinations in Japan and in so-called logic puzzles, and is vestigated, and proof-theory has also been developed. Further- one of the most natural reasoning that could be formalized in more, studies on the characteristics of diagrammatic systems, combination with the first-order formulas. such as their expressive power, drawing techniques, effective usage, and cognitive properties, have also been conducted. Barker-Plummer and Swoboda [2] discussed similar prob- For more information on these studies, see proceedings, e.g., lems. They consider n-ary relationships among objects, and [10], [7], [5], of Diagrams conference series on the theory and their system is defined to be simple and have as few rules as application of diagrams. possible. On the other hand, we concentrate on basic tables representing the binary relationship between objects, and we On the basis of such research, a natural next step is to study design our inference rules so that we take full advantage of heterogeneous reasoning, combining various diagrammatic, the effectiveness of our tables. Furthermore, our system is graphical, and sentential representations. Jon Barwise, one of heterogeneous by combining tables and first-order formulas. the first logicians to investigate the logical status of diagrams, pointed out the importance of studying heterogeneous systems We propose a heterogeneous logic with tables based on in an early work [1], and he introduced a heterogeneous Gentzen’s natural deduction. We first illustrate the type of system combining graphical representations and first-order reasoning discussed in this paper. We then introduce the syntax formulas on a blocks world, e.g., [1], [3]. His Hyperproof and semantics of our heterogeneous logic with tables, HLT. In project has recently been extended to the Openproof project. order to formalize tables and formulas in the same framework, Heterogeneous systems based on Venn (and Euler) diagrams we apply the syntax and semantics of many-sorted logic. and first-order formulas have also been studied, e.g., [8], [11]. Furthermore, a heterogeneous system based on spider diagrams II. A HETEROGENEOUS LOGIC WITH TABLES and its implementation has been developed [12]. In Section II-A, we first specify, through some examples, In this paper, we study a heterogeneous system based on the type of reasoning considered in this paper. We then define first-order formulas and tables. Tables and their usage have the syntax of HLT in Section II-B, and its semantics in Section been studied in the diagrammatic reasoning community, for II-C. We introduce the inference rules of HLT in Section example, in [4], [9], [2]. Our tables are correspondence tables II-D, and define, in Section II-E, the translation of tables into represented by a rectangular arrangement of given data such formulas. This demonstrates the soundness and completeness as symbols, characters, or numbers. Tables are one of the theorems of HLT via the theorems of many-sorted logic. most basic graphical representations, and have been applied for A. Examples of reasoning with tables various usages. From a cognitive science viewpoint, Shimojima [9] studied the semantic mechanism of extracting information Let us investigate the following examples of reasoning with from a given table. tables, and then discuss the characteristics of such reasoning. 9   M T W F M T W F M T W F M T W F a ⃝ × a × × ⃝ ×  a × × ⃝ × a × × ⃝ × b × × b × × b × × b × × × c × c × c × c × × d ⃝ d ⃝ × d d     T0 T1 T2 T3     M T W F M T W F M T W F M T W F a × × ⃝ × a × × ⃝ × a × × ⃝ × a × × ⃝ ×  × ⃝ × × × × × b × ⃝ × ×  b × ⃝ × × b b ⃝  × × × × × × c × × c ×  × c c ⃝ ⃝ × d ⃝ × × ×  d ⃝ × × × d ⃝ × × × d      T4 T5 T6 T7   Fig. 1 Example 1. Consider four people a, b, c, d who are scheduled Next, let us solve the same problem using a correspondence to work separately on one of Monday, Tuesday, Wednesday, table. We construct a table in which the rows are labeled ac- and Friday. The following constraints are known: cording to the workers a, b, c, d, and the columns are labeled by days, M (for Monday), T (for Tuesday), W (for Wednesday), (1) a works on Wednesday; and F (for Friday). Based on the given conditions (1), (2), and (2) Neither b nor c can work on Monday; (3), we insert ⃝ into each entry (x, Y ) for which “x works on (3) On Friday, either c or d should work. 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 Under these conditions, how we can arrange who works on applied condition (5) (stated previously) instead of the given which day? condition (3). In terms of tables, condition (4) is divided into the following two conditions: Let us first consider this problem without using tables. Note that, in addition to conditions (1), (2), and (3), we know that: (6) In each row, exactly one entry should be marked as ⃝, and the other entries should be ×; (4) There is a one-to-one correspondence between the persons and the days. (7) In each column, exactly one entry should be marked as ⃝, and the other entries should be ×. First, condition (1) states that “a works on Wednesday.” Thus, Thus, from the fact that the (a, W )-entry is ⃝ and (6), we by (4), we find that “a does not work on Monday.” Then, by find that the (a, M ), (a, T ) entries are ×, as illustrated in T1 . combining this with (2) and (4), we find that “d works on Similarly, because the (a, M ), (b, M ), (c, M ) entries are all ×, Monday.” we find that (d, M ) must be ⃝ by (7), as illustrated in T2 . In the given situation, conditions (3) and (4) imply the Hence, by successively applying conditions (6) and (7), we following (in fact, under (4), conditions (3) and (5) are finally get the complete table T7 . From this, we can read off equivalent): complete information about the working day of a, b, c, d. (5) “a does not work on Friday, and b does not work on Although all entries are either ⃝ or × in the above Friday.” example, in general, some entries may not be determined. For example, if we remove condition (3), we obtain a partial table Because we have already determined that “d works on Mon- in which (b, T ), (b, F ), (c, T ), (c, F ) remain indeterminate. day,” (4) implies that “d does not work on Friday.” Then, as the above facts can be combined to give that “Neither a nor Let us consider another example, in which the number of b nor d works on Friday,” we find by (4) that “c works on days worked by each person and the number of people working Friday.” on a given day are changed from Example 1. Example 2. Each person should work exactly two days, and As for b, because we already know that “a works on exactly two people should work on each day. Conditions (1) Wednesday,” “c works on Friday,” and “d works on Monday,” and (2) are the same as in Example 1. Condition (3) is replaced we have from (4) that “b works on Tuesday.” by: (8) On Friday, c and d should work together. In this case, In this way, we are able to determine the working day of how can we arrange the allocation of working days to a, b, c, d? a, b, c, d. Using tables, we are able to apply essentially the same strategy Note that in the above reasoning, the condition (4) is as for Example 1. Note that conditions (6) and (7) in Example necessary to derive any piece of information. Further note 1 become the following: that there are various ways to solve the above problem. For (9) In each row, exactly two entries should be marked as example, in the above solution, we converted condition (3) ⃝, and the other entries should be ×; with disjunction into (5) without disjunction. Alternatively, we could have divided (3) into two cases, and examined each case (10) In each column, exactly two entries should be marked individually. as ⃝, and the other entries should be ×. 10   M T W F M T W F M T W F a ⃝ ⃝ × M T W F a ⃝ a ⃝ ⃝ a ⃝ × ⃝ ×  b × b × b × × b × × c × ⃝ c × ⃝ c × ⃝ c × ⃝ ⃝ d ⃝ ⃝ d ⃝ ⃝ d ⃝ ⃝ d     T8 T9 T10 T11     M T W F M T W F M T W F M T W F a ⃝ × ⃝ × a ⃝ × ⃝ × a ⃝ × ⃝ × a ⃝ × ⃝ × b × ⃝ ⃝ ×  b × ⃝ ⃝ × b × ⃝ ⃝ × b × ⃝ ⃝ × × ⃝ × × × c × ⃝ c ⃝ c ⃝ c ⃝ ⃝ d ⃝ ⃝ d ⃝ × × ⃝ d ⃝ × × ⃝ d ⃝ × × ⃝       T12 T13 T14 T15   Fig. 2 We begin with the table T8 in Fig. 2. Because the item (I) in the above procedure. Furthermore, a given condi- (b, M ), (c, M ) entries are ×, we find, by (10), that tion, such as an implicational sentence, may be decomposed (a, M ), (d, M ) are ⃝, as illustrated in T9 . In a similar way, using basic information obtained from item (III). In these we obtain T10 . Then, because the entries of (a, M ), (a, W ) are complex cases, we must repeat the whole procedure several ⃝, we find, by (9), that (a, T ) is ×, as in T11 , and in a similar times. way to Example 1, we finally obtain table T15 . Thus, a natural system of formalizing our reasoning with In the above examples, although the number of ⃝ is fixed tables is a heterogeneous logical system combining tables to be the same (i.e., one or two) in every row and column, this and first-order formulas. Our formalization here is based on is not necessarily the case. We do not assume such a restriction Gentzen’s natural deduction. in our formalization of reasoning with tables. By investigating Examples 1 and 2, we find that there are B. Syntax of HLT two types of condition in our problems. One is a “constraint In order to formalize our heterogeneous reasoning with over the framework of a given problem” (e.g., condition (4) tables, we adopt two-sorted logic, in which constants and above), and we call these global conditions. In view of tables, variables of the first-order language are divided into two our global conditions are constraints over every row and sorts: sorts of row and column. Although usually distinguished column. The other type is a “specific condition for each object” explicitly by sort symbols in many-sorted logic, we distinguish (e.g., (1) above), and we call these local conditions. In view the two by lower- and uppercase letters: a constant (resp. of tables, local conditions specify only particular entries. Our variable) of the row sort is denoted by a (resp. x), and that of reasoning with tables is essentially conducted by combining the column sort is denoted by A (resp. X). (See, for example, global conditions and local conditions. [6] for many-sorted logic.) Then, by ⃝(a, B) we mean “a and One of the remarkable facts of our reasoning with tables is B are in a certain positive relation.” Thus, sentences such as that, even if the given local and global conditions change, we “a is B,” “a matches B,” and “a corresponds to B” are all are able to apply essentially the same strategy: that is, we check expressed as ⃝(a, B). each row or column, and apply appropriate global conditions controlling rows and columns. Thus, based on the local and We begin by specifying some vocabulary. global conditions, our reasoning using tables is conducted as follows. Definition 3 (Vocabulary). We use the following symbols. (I) We decompose, if necessary, the given conditions Row-constants: a1 , a2 , . . . ; Col-constants: A1 , A2 , . . . into local conditions (i.e., atomic sentences or their Row-variables: x1 , x2 , . . . ; Col-variables: X1 , X2 , . . . negation, such as “a does not work on Friday” and “b Predicate: ⃝( , ) does not work on Friday”) by applying logical laws Constants and variables are collectively called terms, and are (e.g., (3) ∧ (4) → (5)). denoted by s, t, u, . . . . (II) We construct a correspondence table using these local conditions (e.g., T0 ). Using the above symbols, we construct our formulas as (III) By applying the global conditions, that is, by exploit- follows. ing constraints over the number of ⃝ or × in a row or column, we further insert ⃝ and × into the table. Definition 4. An atomic formula is of the form ⃝(s, t) for (IV) Finally, we extract information from the table. a row-constant/variable s and a col-constant/variable t. Based on atomic formulas, complex formulas are defined inductively Although most of the given conditions in the above ex- as usual: amples are already local conditions, more complex conditions may generally be given. In such cases, we frequently apply φ := ⃝(s, t) φ ∧ φ φ ∨ φ φ → φ ¬φ 11 ∀x.φ ∃x.φ ∀X.φ ∃X.φ in which rows are labeled by distinct row-constants a1 , . . . , am and columns are labeled by distinct col-constants A1 , . . . , An . In particular, we denote the negation of an atom ¬⃝(s, t) In a specific representation of a table, we usually omit the by ×(s, t). Formulas of the forms ⃝(s, t) and ×(s, t) are symbol “b” and leave the entry blank. collectively called literals. Literals containing no variables are called ground literals (or closed literals), and they are denoted Remark 8. A table T is abstractly defined as the function by α, α1 , α2 , . . . . We denote by α the ground literal ×(a, B) T : R × C −→ {⃝, ×, b}, where R (resp. C) is some finite set when α is ⃝(a, B), and ⃝(a, B) when α is ×(a, B). Formulas of row-constants (resp. col-constants) of T . containing no free variables are said to be closed. Note that no entry can be marked with more than one of We sometimes write ⃝(s, t) as t(s), and ×(s, t) as ¬t(s). ⃝, ×, b at the same time. As usual, any pair of tables, say T1 and T2 , are identical In order to express sentences of the form “among n objects, if they consist of the same constants, and if the ⃝, × marks there are exactly i objects that are A,” we introduce a kind of of all entries in T1 and T2 are also identical. This is formally counting quantifier, and write the sentence as ∃i/n x.A(x), i.e., defined as follows. ∃i/n x.⃝(x, A). Definition 9 (Equivalence of tables). A table T1 is a subtable Definition 5 (Global formula). For fixed sets of row-constants of T2 , written as T1 ⊆ T2 , when: R = {a1 , . . . , an } or of col-constants C = {A1 , . . . , An }, the following forms of formulas are called global formulas: For • all row- and col-constants of T1 are also those of T2 ; any A and a, • 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 . ∃i/n x ∈ R.A(x), ∃i/n x ∈ R.¬A(x), ∃i/n X ∈ C.X(a), ∃i/n X ∈ C.¬X(a). T1 and T2 are (syntactically) equivalent when T1 ⊆ T2 and T2 ⊆ T1 hold. If a set of constants is clear from the context, it is abbreviated as ∃i/n x.A(x). Note that, by definition, two specific tables that differ only Global formulas are simply abbreviations of the appropriate in the orders of their rows and columns are equivalent. first-order formulas. Let σ be a permutation of the given row-constants a1 , . . . , an , and Sn be the set of all their C. Semantics of HLT permutations. We then define ∃i/n x ∈ R.A(x) as: We now define the semantics of our HLT as a particular ∨ ( ) case of the semantics of many-sorted logic. (See [6] for the A(aσ1 ) ∧ · · · ∧ A(aσi ) ∧ ¬A(aσi+1 ) ∧ · · · ∧ ¬A(aσn ) semantics of many-sorted logic.) σ∈Sn Definition 10. A structure M is (Mrow , Mcol , I), where: We treat ∃i/n x ∈ R.¬A(x) in a similar manner. Mrow and Mcol are disjoint non-empty domains for the row Let σ be a permutation of the given col-constants A1 , . . . , An , and column sorts, respectively. and Sn be the set of all their permutations. We then define I is an interpretation function such that: ∃i/n X ∈ C.X(a) as: • I(a) ∈ Mrow for each row-constant a; ∨ ( ) Aσ1 (a) ∧ · · · ∧ Aσi (a) ∧ ¬Aσi+1 (a) ∧ · · · ∧ ¬Aσn (a) • I(A) ∈ Mcol for each col-constant A; σ∈Sn • I(⃝) ⊆ Mrow × Mcol . We again treat ∃i/n X ∈ C.¬X(a) similarly. Definition 11. A valuation v in M is a function that assigns Example 6. For example, for some row-constant a and every row-variable x an entity of Mrow , i.e., v(x) ∈ Mrow , col-constants C = {A1 , A2 , A3 }, the global formula and every col-variable X an entity of Mcol , i.e., v(X) ∈ Mcol . ∃2/3 X ∈ C.X(a) is the abbreviation of the following formula: Definition 12 (Truth conditions). The notion of satisfaction ( ) of a formula φ in a structure M with a valuation v, written A1 (a) ∧ A2 (a) ∧ ¬A3 (a) M |= φ[v], is defined inductively as follows: ( ∨ ) A1 (a) ∧ A3 (a) ∧ ¬A2 (a) • M |= ⃝(s, t)[v] if and only if (I(s)[v], I(t)[v]) ∈ I(⃝), ( ∨ ) where I(s)[v] = I(a) when s is a row-constant a, and A2 (a) ∧ A3 (a) ∧ ¬A1 (a) I(s)[v] = v(x) when s is a row-variable x; Similarly for t; where we omit trivial permutations such as A2 (a) ∧ A1 (a) ∧ • M |= ¬φ[v] if and only if M ̸|= φ[v]; ¬A3 (a), which is equivalent to the first disjunct in the above. Truth conditions for other connectives ∧, ∨, → are Next, we define our tables. defined as usual; Definition 7. A table T is an m × n-matrix over symbols • M |= ∀x.φ[v] if and only if, for all m ∈ Mrow , M |= {⃝, ×, b}; that is, a rectangular arrangement of the symbols, φ[v(x 7→ m)], 12 [φ]n [ψ]n .. .. .. .. .. .. .. .. .. .. .. .. .. .. φ ψ φ1 ∧ φ2 φi φ ∨ ψ θ θ ∧I ∧Ei (i = 1, 2) ∨I ∨E, n φ∧ψ φi φ1 ∨ φ2 i (i = 1, 2) θ [φ]n [φ] n [¬φ]n .. .. .. .. .. .. .. .. .. .. .. .. .. .. .. .. ψ φ φ→ψ ⊥ φ ¬φ ⊥ ⊥ RAA, n → I, n →E ¬E φ→ψ ψ ¬φ ¬I, n ⊥ φ ⊥E φ .. .. .. .. .. .. .. .. φ φ ∀x.φ ∀X.φ ∀Ir ∀Ic ∀Er ∀Ec ∀x.φ ∀X.φ φ[x := t] φ[X := t] where, in ∀Ir (and ∀Ic), the variable x (resp. X) may not occur free in any open hypothesis on which φ depends; in ∀Er (and ∀Ec), t is a row-variable/constant (resp. col-variable/constant). .. .. [φ]n [φ]n .. .. .. .. .. .. .. .. .. .. φ[x := t] φ[X := t] ∃x.φ ψ ∃X.φ ψ ∃Ir ∃Ic ∃Er, n ∃Ec, n ∃x.φ ∃X.φ ψ ψ where, in ∃Ir (and ∃Ic), t is a row-variable/constant (resp. col-variable/constant); in ∃Er (and ∃Ec), x (resp. X) may not occur free in ψ nor in any open hypothesis on which ψ depends, except in φ. Fig. 3 Inference rules for formulas in HLT where v(x 7→ m) is the valuation that is exactly the Rules for formulas are the rules for ∧, ∨, →, ¬, ∀, ∃, and same as v except for x, and x is assigned to m; ⊥E and RAA listed in Fig. 3. • M |= ∀X.φ[v] if and only if, for all m ∈ Mcol , M |= Rules for tables are the following in, row, col, ext rules: φ[v(X 7→ m)]; • M |= ∃x.φ[v] if and only if there exists m ∈ Mrow such ... Ai ... ... Ai ... that M |= φ[v(x 7→ m)]; a a • M |= ∃X.φ[v] if and only if there exists m ∈ Mcol such ⃝(a, Ai ) in⃝ ×(a, Ai ) in× that M |= φ[v(X 7→ m)]; ... Ai ... ... Ai ... × • M |= T for a table T if and only if M |= ⃝(s, t) for a ⃝ a any entry (s, t) of T that is ⃝, and M |= ×(s, t) for any entry (s, t) of T that is ×. M is said to be a model of φ, written as M |= φ, when In order to describe the same types of rules, we use the symbol M |= φ[v] holds for any valuation v in M . ⊗, which denotes either ⃝ or ×. Furthermore, ⊗ denotes ⃝ if ⊗ is ×, and denotes × if ⊗ is ⃝. The following four rules The semantic consequence relation in our HLT is defined of row and col are duplicated depending on whether ⊗ is ⃝ as follows. or ×. Definition 13 (Semantic consequence). Let Γ be a set of closed Let σ be a permutation of columns A1 , . . . , An . Under the formulas, let G be a set of global formulas, and let T be a table. permutation, we assume that entries marked as ⃝ and those A closed formula φ is said to be a semantic consequence of marked as × are grouped. Γ, G, T , written as Γ, G, T |= φ, when any model of Γ, G, and T is also a model of φ. Aσ1 ... Aσi Aσi+1 ... Aσn a ⊗ ... ⊗ □ ... □ D. Inference rules of HLT ∃i/n X. ⊗ (a, X) row⊗ Aσ1 ... Aσi Aσi+1 ... Aσn In this section, we introduce the inference rules of HLT, which consist of the usual natural deduction rules for formulas a ⊗ ... ⊗ ⊗ ... ⊗ 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. where each □ is blank or ⊗. 13 M T W F a W (c) ∨ F (c) ∃1/4 X.X(c) b c ¬M (c) ∧ ¬T (c) d W (a) ¬M (b) ¬M (c) ¬T (c) in⃝, × M T W F a ⃝ b × c × × d ∃1/4 X.X(a) row× M T W F a × × ⃝ × b × c × × d ∃1/4 x.M (x) col⃝ M T W F a × × ⃝ × b × c × × d ⃝ ∃1/4 x.W (x) col× M T W F a × × ⃝ × b × × c × × × d ⃝ × M T W F a × × ⃝ × b × ⃝ × × c × × × ⃝ d ⃝ × × × M (d) ∧ T (b) ∧ W (a) ∧ F (c) Fig. 4 A proof in HLT of Example 1. In the figure, each double line is an abbreviation of some applications of inference rules. Aσ1 ... Aσi Aσi+1 ... Aσn T ∧ ∧ ext {⃝(aj , Ai ) | (aj , Ai ) is ⃝ in T } ∧ {×(aj , Ai ) | (aj , Ai ) is × in T } a □ ... □ ⊗ ... ⊗ ∃i/n X. ⊗ (X, a) row⊗ The in-rule enables us to convert ground literals into a Aσ1 ... Aσi Aσi+1 ... Aσn table, and, conversely, the ext-rule enables us to convert a table a ⊗ ... ⊗ ⊗ ... ⊗ into a conjunction of literals. The row and col rules pertain to the manipulation of tables. where each □ is blank or ⊗. The notion of proof is defined inductively as usual in Let σ be a permutation of rows a1 , . . . , am . Under the per- natural deduction. mutation σ, we assume that entries marked as ⃝ and those Definition 15. Let Γ be a set of closed formulas, let G be a marked as × are grouped. A set of global formulas, and let T be a table. A closed formula □ aσ1 . . φ is provable from Γ, G, T , written as Γ, G, T ⊢ φ, when there A . . . . exists a proof of φ from the open assumption Γ, G, T . aσ1 ⊗ aσj □ . . . . aσj+1 ⊗ Example 16. A proof in HLT of Example 1 is given in Fig. 4. . . aσj ⊗ . . . . aσj+1 □ . . aσm ⊗ ∃j/m x. ⊗ (A, x) E. Translation of tables . . col⊗ . . . . A □ ∃j/m x. ⊗ (A, x) We give a translation of the rules for tables into those aσm aσ1 ⊗ col⊗ . . for usual natural deduction without tables, from which the A . . aσ1 ⊗ . . soundness and completeness theorems of HLT are obtained. aσj ⊗ . . . . aσj+1 ⊗ We first define the following terminology. . . aσj ⊗ . . . . aσj+1 ⊗ . . Definition 17. A conjunction of literals is said to be consistent aσm ⊗ when it has a model. . . . . . . aσm ⊗ We define the translation of tables into a formula. This is where each □ is blank or ⊗. where each □ is blank or ⊗. completely parallel to the ext-rule of HLT. 14 [A1 ∧ A3 ∧ ¬A2 ]1 A1 ∧ A2 [A2 ∧ A3 ∧ ¬A1 ]1 A1 ∧ A2 ∧E ∧E ∧E ∧E ¬A2 A2 ¬A1 A1 [A1 ∧ A2 ∧ ¬A3 ]1 ¬E ¬E ⊥ ⊥ ∧E ⊥E ⊥E ∃ 2/3 X.X(a) ¬A3 ¬A3 ¬A3 ∨E, 1 ¬A3 A1 ∧ A2 ∧I A1 ∧ A2 ∧ ¬A3 Fig. 5 A translation given in Example 20 Definition 18. Each table T is translated into a conjunction by the definition of the permutation for ∃i/n X.X(a). of (consistent ground) literals T ◦ as follows: Hence, by applying the ⊥E-rule, we obtain ¬Aσn . ∧ T ◦ = {⃝(aj , Ai ) | (aj , Ai ) is ⃝ in T } 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 . ∧ {×(aj , Ai ) | (aj , Ai ) is × in T } As we have Aσi by the initial assumption, by applying the Conversely, it is easily seen that, for any consistent con- ∧I-rule, we obtain Aσi ∧ ¬Aσn , which is the translation of junction of ground literals, there exists a corresponding table. the conclusion of the given row×-rule. Thus, we may regard a table T and a consistent conjunction L Example 20. Let us consider the following application of the of ground literals to be interchangeable, and (slightly abusing row×-rule: A1 A2 A3 our notation) we write, for example, L ⊆ T . a ⃝ ⃝ ∃2/3 X.X(a) Based on the translation of tables, we give a translation of row× A1 A2 A3 table manipulations into rules of natural deduction. (See also a ⃝ ⃝ × Example 20 below.) Note that ∃2/3 X.X(a) := (A1 ∧ A2 ∧ ¬A3 ) ∨ (A1 ∧ A3 ∧ Theorem 19 (Translation). If G, T1 ⊢ T2 with only row and ¬A2 ) ∨ (A2 ∧ A3 ∧ ¬A1 ), where we abbreviate Ai (a) as Ai col rules in HLT, then G, T1◦ ⊢ T2◦ in natural deduction without and omit trivial permutations. This application of the row×- tables. rule is translated as in Fig. 5. Proof: It is sufficient to give a translation of row and col The soundness of HLT is obtained straightforwardly by the rules into combinations of rules of natural deduction without above theorem of translation, because each rule for tables is tables. translated into a combination of rules for formulas by Theorem Because all cases are treated in a similar way, we show 19, and each rule for formulas, i.e., of many-sorted logic, is only the following row×-rule (we assume that all □ of the known to be sound. rule are blank for simplicity). Theorem 21 (Soundness of HLT). Let Γ be a set of closed Aσ1 ... Aσi Aσi+1 ... Aσn formulas, G be a set of global formulas, T be a table, and φ a ⃝ ... ⃝ ∃i/n X.X(a) be a closed formula. If Γ, G, T ⊢ φ in HLT, then Γ, G, T |= φ. row× Aσ1 ... Aσi Aσi+1 ... Aσn a ⃝ ... ⃝ × ... × Because our inference rules and semantics of HLT “without tables” are just particular cases of those of many-sorted logic, From our translation of tables, the table in the premises of the following completeness theorem of HLT holds via the the row×-rule is translated into Aσ1 (a) ∧ · · · ∧ Aσi (a). Note theorem of many-sorted logic. (See [6] for the completeness ( another premise of the row×-rule ∃ X.X(a) )is i/n of many-sorted logic.) also that ∨ τ ∈Sn Aτ 1 (a) ∧ · · · ∧ Aτ i (a) ∧ ¬Aτ i+1 (a) ∧ · · · ∧ ¬Aτ n (a) . Theorem 22 (Completeness of HLT). Let Γ be a set of closed Given these two formulas, we construct a natural deduction formulas, G be a set of global formulas, T be a table, and φ proof. be a closed formula. If Γ, G, T |= φ, then Γ, G, T ⊢ φ in HLT. We denote by Aτ i the conjunction Aτ 1 (a) ∧ · · · ∧ Aτ i (a), Proof: Based on the translation of tables, a table T and by ¬Aτ n the conjunction ¬Aτ ∨ i+1 (a) ∧ · · · ∧ ¬Aτ n (a). and the consistent set of ground literals T ◦ are equivalent. Then, we can write ∃i/n X.X(a) as τ ∈Sn (Aτ i ∧ ¬Aτ n ). Thus, Γ, G, T |= φ is equivalent to Γ, G, T ◦ |= φ. Then, In order to apply the ∨E-rule of natural deduction, we by the completeness theorem of many-sorted logic, we have divide the following cases according to the form of each Γ, G, T ◦ ⊢ φ. Again, by the translation (more precisely, by the disjunct Aτ i ∧¬Aτ n of the above ∃i/n X.X(a), and we derive ext-rule of HLT for T ), we have Γ, G, T ⊢ φ in HLT. ¬Aσn in each case. III. C ONCLUSION AND FUTURE WORK 1) When τ = σ, or when Aσi ↔ Aτ i holds, we apply the ∧E-rule of natural deduction to Aτ i ∧ ¬Aτ n to We investigated reasoning with tables by exploiting local obtain ¬Aτ n , which is equivalent to ¬Aσn . and global conditions. This type of reasoning is not just a mere 2) Otherwise, we apply the ∧E-rule to Aτ i ∧ ¬Aτ n , puzzle, but can be applied to simple scheduling problems. In and obtain ¬Aτ n . Note that at least one of the order to formalize our reasoning with tables, we introduced a conjuncts of ¬Aτ n contradicts a conjunct of Aσi heterogeneous logic with tables, HLT, with a combination of 15 first-order formulas. For the formalization of HLT, we applied manipulations on the table, i.e., by dealing only with the the syntax and semantics of many-sorted logic. Although we number of ⃝, × symbols in each row and column. Further- actually applied two-sorted logic, as we studied the most more, there are two ways, in a sentential system, to derive a basic binary relationship between objects, our system can be statement, say “d works on Monday (M (d))”: deriving M (d) extended to cover the n-ary relationship between objects, as from ¬M (a), ¬M (b), ¬M (c) by checking every person on in [2], by applying the general many-sorted logic. Monday, and from ¬T (d), ¬W (d), ¬F (d) by checking every possible working day of d. These derivations correspond, in We defined inference rules for HLT that consist of the our table system, to an application of col rule and row rule, usual natural deduction rules for the first-order formulas and respectively. table manipulation rules. These were designed to reflect our intuitive and effective manipulation of the tables. We inves- These comparison between sentential systems and our tigated the translation of tables and their manipulations into table system should be investigated by combining logic and formulas and natural deduction inference rules. Then, based cognitive science methods. on these translations, we obtained soundness and completeness theorems of HLT by reducing them to the usual many-sorted R EFERENCES logic theorems. [1] Gerard Allwein and Jon Barwise, eds., Logical reasoning with diagrams, In this paper, for the sake of simplicity, we concentrated Oxford Studies In Logic And Computation Series, 1996. on the most basic global formulas, such as “among n objects, [2] Dave Barker-Plummer and Nik Swoboda, Reasoning with coincidence grids–A sequent-based logic and an analysis of complexity, Journal of there are ‘exactly i objects’ . . . .” Our system can be easily Visual Languages and Computing, 22 (1), 56-65, 2011. extended by introducing the following forms for the global [3] Jon Barwise and John Etchemendy, A Computational Architecture for formulas: Heterogeneous Reasoning, Proceedings of the Seventh Conference on Theoretical Aspects of Rationality and Knowledge, 1-14, 1998. • ∃≤i/n x.A(x) meaning “among n objects, there are [4] Jon Barwise and Eric Hammer, Diagrams and the concept of logical ‘at most’ i objects that are A,” and system, in Logical reasoning with diagrams, G. Allwein and J. Barwise, eds., Oxford Studies In Logic And Computation Series, 1996. • ∃≥i/n x.A(x) meaning “among n objects, there are [5] Philip T. Cox, Beryl Plimmer, Peter Rodgers eds., Diagrammatic Rep- ‘at least’ i objects that are A.” resentation and Inference: 7th International Conference, Diagrams 2012, Lecture Notes in Computer Science, Vol. 7352, 2012. Similarly, we could consider ∃≤i/n X.X(a) and ∃≥i/n X.X(a), [6] Herbert B. Enderton, A Mathematical Introduction to Logic, Second as well as negative literals. These formulas are also just Edition, Academic Press, 2000. abbreviations of appropriate first-order formulas, similar to the [7] Ashok K. Goel, Mateja Jamnik, N. Hari Narayanan eds., Diagrammatic definition of ∃i/n in Section II-B. 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 Based on the informal analysis of Examples 1 and 2 and Journal of Formal Logic, Volume 35, Number 1, 73-87, 1994. the translation between tables and formulas (Theorem 19 and [9] Atsushi Shimojima, The Inferential-Expressive Trade-Off: A Case Study Example 20), we may point out the following differences, for of Tabular Representations, Diagrams 2002, 116–130, 2002. example, between the usual sentential systems and our table [10] Gem Stapleton, John Howse, John Lee Eds., Diagrammatic Representa- tion and Inference: 5th International Conference, Diagrams 2008, Lecture system. Notes in Computer Science, Vol. 5223, 2008. (1) In a sentential system, on the one hand, we need to derive [11] Nik Swoboda and Gerard Allwein, Heterogeneous Reasoning with each statement corresponding to an entry of a table one by Euler/Venn Diagrams Containing Named Constants and FOL, Electronic Notes in Theoretical Computer Science, 134, 153-187, 2005. one. On the other hand, in our table system, by an application [12] Matej Urbas and Mateja Jamnik, Heterogeneous Proofs: Spider Dia- of our rule, a number of entries are filled with ⃝ or × at grams Meet Higher-Order Provers, Interactive Theorem Proving, Lecture once, that is, a number of statements are derived at once. This Notes in Computer Science, Volume 6898, 376-382, 2011. 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 (∃1/4 x.W (x))” is translated as “there is exactly one ⃝ in column W ”), reasoning with the table is conducted by completely graphical or geometrical 16