=Paper=
{{Paper
|id=Vol-1132/paper2
|storemode=property
|title=A Heterogeneous Logic with Tables
|pdfUrl=https://ceur-ws.org/Vol-1132/paper2.pdf
|volume=Vol-1132
}}
==A Heterogeneous Logic with Tables==
https://ceur-ws.org/Vol-1132/paper2.pdf
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