Resolution for label-based formulas in hierarchical representation.
Order-sorted logic iucludes many and partially ordered sorts as a sort-hierarchy. In the field of knowledge representation and reasoning, it is useful to develop reasoning systems fbr terminological knowledge, together with assertional knowledge. However, the expression of sort-hierarchies cannot sufficiently capture the lexical diversity of terminological knowledge. In addition to sorts, various kinds of symbols: constants, functions and predicates are semantically and hierarchically associated with each other. This is because natural language words identifying these symbols can be employed in the description of terminological knowledge. In this paper, we present a label-based language for consistently handling the variety of hierarchical relationships among symbol names. For this language we develop a sorted resolution system whose reasoning power is enhanced by adding hierarchical inference rules with labeled substitutions.
Introduction
Logical languages with class-hierarchy formally concentrate upon representation
and reasoning for terminological knowledge (and ontologies 7) ), together
with assertional knowledge. The significant feature is that one can specify
classes as sets of individuals and their hierarchical relationships (e.g. is-a rela-
tions) in the languages. In the past, there have been several approaches to
the formalisms: order-sorted logic, 15, 16, 5, 17) typed logic programming, 1, 2, description
logics 8, 13) and object-oriented deduction languages. 12, 18) In particular,
order-sorted logic gives us the advantage of interacting terminological knowledge
and assertional knowledge. This logic theoretically corresponds to a first-order
predicate logic with sort-hierarchy, where sort symbols are many and partially
ordered. The sorted language can represent terminological knowledge as a sort-
hierarchy and assertional knowledge as sorted formulas.
However, the expression of sort-hierarchies cannot su#ciently capture
the lexical diversity of terminological knowledge since hierarchical information
exclusive of sorts is ignored in logical languages. The elements of terminological
knowledge can be regarded as various kinds of symbols in logic: sorts, constants,
functions and predicates, whereas the symbols are semantically separated from
each other and merely used as components in formulas. From the viewpoint
of symbolic knowledge representation, we require that the symbol names be
semantically and hierarchically associated with each other, without losing their
roles. To enrich hierarchical reasoning, Kaneiwa and Tojo 10) proposed an order-sorted
logic with sort and predicate hierarchies, but the hierarchies did not enable
complicated expressions combining di#erent kinds of symbols (e.g. father #
parent as a subordinate relation of a function and a predicate).
The aim of this paper is to provide a logical framework for consistently
handling various hierarchies of symbol names (of sorts, constants, functions and
predicates) and reasoning over them. We generalize an order-sorted logic by
means of consisting of label-based expressions. A label-based language contains
label-based terms and formulas and a label hierarchy, for representing assertional
knowledge and terminological knowledge. Labels denote all the symbol names of
constants, functions and predicates occurring in terms and formulas, and
build a common hierarchy of the symbols. The semantics of the label-based language
is specified in keeping the constraints on hierarchical relationships among
names. More precisely, labels and their hierarchy are interpreted as the
combinations of di#erent roles of symbols. We develop a sorted resolution system
for label-based clausal formulas by introducing labeled substitutions and
hierarchical resolution rules. This system performs reasoning on a label hierar-
chy, gained by various usages of labels and their hierarchical relationships (e.g.
the same label might be used for function and predicate symbols).
This paper is organized as follows. Section 2 explains the notions of
logic with sort-hierarchy 14) and an order-sorted logic with sort predicates. In
Resolution for Label-based Formulas in Hierarchical Representation 3
animal
ancestor descendant
parent child
father mother son daughter
John Tom
human
Fig. 1 A terminological hierarchy
Section 3, we show a requirement for hierarchical expressions, under the discussion
about various usages of labels in a terminological hierarchy. Section 4
provides the syntax and semantics of a label-based language. In Section 5, we
define labeled substitutions and hierarchical resolution rules in an inference system
for label-based expressions. In Section 6, we discuss conclusions and future
work.
-2 Logic with sort-hierarchy
Order-sorted logic is a first-order predicate logic with sort-hierarchy. A
sort-hierarchy is a pair (S, < s ) of a set S of sort symbols s, s 1 , s 2 , . and a
subsort relation < s over S. A subsort relation is defined by a set of subsort
declarations s i < s s j . For instance, father < s parent and mother < s parent
declare that father and mother are subsorts of the sort parent. As shown in
Fig. 1, the hierarchy can be built by subsort declarations. We use sort symbols to
express the restricted domains and ranges of variables, functions and predicates.
A sorted variable is denoted as x: s. For example, x: father is a sorted variable
of the sort father. A function declaration is denoted by f
and a predicate declaration is denoted by p: s 1 - s n .
For knowledge base reasoning, Beierle et al. 4) extended an order-sorted
resolution system that can strongly connect separated terminological knowledge
and assertional knowledge. In the sorted logic, each sort symbol can be used not
only as the sort of a term but also as a unary predicate (called a sort predicate).
clauses, s, s 1 , s 2 be sorts (or sort predicates), # be a sorted
substitution, and t, t 1 , t 2 be sorted terms. In addition to sorted substitutions,
the authors introduced inference rules of sort predicates as follows:
4 Ken KANEIWA
(subsort resolution rule)
C#
(elimination rule)
if t# is a term of the sort s or a subsort of s. Alternatively, in order to explicitly
embed negative information in a sort-hierarchy, Kaneiwa and Tojo 11) developed
an order-sorted resolution system with structured sorts. In both sorted logics,
sort predicates are usefully introduced for interacting terminological knowledge
and assertional knowledge.
-3 Requirements for hierarchical expressions
In this section, we first show possible usages of labels as symbol names
using order-sorted logic, which will entail a requirement for hierarchical expressions
of symbol names. For terminological knowledge, we then discuss the necessity
of a sublabel relation to generally represent di#erent types of subordinate
relations.
Five uses for labels. Given the terminological hierarchy as shown in Fig. 1,
each element of the hierarchy (e.g. John, human, father and child) is available
for the names of various symbols: sorts, constants, functions, unary predicates
and binary predicates. If the label 'John' is used as a constant, then the formula
parent(John) can describe the sentence "John is a parent." If the label
'human' plays the role of a unary predicate, the formula human(John) is the
sentence "John is human," in which 'human' can be relabeled more precisely as
'is human.' For the label `father' as a function that maps from a person into its
father, the term father(T om) expresses Tom's father. If we have the relationship
between a father and his child, then 'child' as a binary predicate coincides
with 'is a child of.' Hence child(T om, John) expresses ``Tom is a child of John.''
Finally, the formula walking(John : father) indicates "John who is a father is
walking" where 'father' is used as a sort.
These usages reflect the meaning and pragmatics of natural language
words. Fig. 2 classifies the roles of symbols as conceivable for the labels. Every
label except for John and Tom can be used as a unary predicate or sort, and
the labels exclusive of animal and human can be regarded as binary predicates.
Resolution for Label-based Formulas in Hierarchical Representation 5
animal
ancestor descendant
parent child
father mother son daughter
John Tom
constants
binary predicates
unary predicates or sorts
functions
human
Fig. 2 The roles of symbols in a terminological hierarchy
Moreover, mother and father can be functions as sublabels of parent, and John
and Tom can be constants as sublabels of human.
When logically supporting the usages, the formality of logic gives rise
to the syntax limited by the rigorous definition of symbol roles. Therefore,
the labels variously used as above cannot be incorporated in the hierarchical
information. To overcome the limitation, we will have to devise a method for
covering various types of subordinate relations, which are composed from sorts,
constants, functions, unary predicates and binary predicates. In other words,
there are di#erent combinations of symbols for each sublabel relation as follows:
types of subordinate relation R i sublabel relation
unary predicate
binary predicate # binary predicate
father # parent
The sort-hierarchy in order-sorted logic does not express such hierarchical
relationships including other kinds of symbols. Even if they are described in
first-order formulas, we lose the conciseness of terminological knowledge, namely,
di#erent types of subordinate relations R 1 , R 2 , . cannot be generally treated
as one sublabel relation. In the next section, we will formalize a label-based
language for concisely representing the various hierarchical relationships.
6 Ken KANEIWA
-4 Label-based language L LB
We present a label-based language where labels are commonly used as the
names of di#erent kinds of symbols. Thus, a hierarchy over a set of labels (which
we will call a label hierarchy) generally imply various hierarchies of first-order
symbols, and the terms and formulas in the language are composed of labels.
4.1 Syntax
Let LB be a set of labels. In the following, we write its elements as
L, M,N , or L 0 , L 1 , L 2 , . A subordinate relation of labels (called a sublabel
relation) is declared as follows:
For example, for bird, animal # LB, the declaration bird # animal indicates
that bird is a sublabel of animal.
A label-based language LLB contains a label hierarchy
where LB is a set of labels and # is a sublabel relation over LB. Note that the
label hierarchy is a partially ordered set of labels. By indexing c, fn, pn, or s to
each label L, the labels
are distinguished as constants, n-ary functions, n-ary predicates and sorts, re-
spectively. Using this notation, symbols in a first-order language are introduced
by the labels.
. C # {L c
| L # LB} is a set of constant symbols of labels,
. Fn # {L fn
| L # LB} is a set of n-ary function symbols of labels,
. Pn # {L pn
| L # LB} is a set of n-ary predicate symbols of labels.
We denote the set of all function symbols by F and the set of all predicate
symbols by P .
| L # LB} be a set of sort symbols of labels. A label-based
sort-hierarchy is obtained by a label hierarchy in such a way that a subsort
relation < s over S is defined on a sublabel relation as below:
if there are L s
Namely, given a label hierarchy label-based sort-hierarchy
is a pair (S, < s ) where S is a set of sort symbols denoted by labels in LB
and <
The domain of each sorted variable
Resolution for Label-based Formulas in Hierarchical Representation 7
(denoted x: L s
in LLB is restricted by a sort L s
i in S. VL s
is a set of variables
, . of sort L s
Remark. Each label-based language can be flexibly defined by containing any
sets C, F, P, S of symbols which labels in LB denote. For example, consider a
language where a label L # LB is employed as a constant L c
# C and a unary
function L f1
F , but another label M # LB is employed only as a unary
predicate M p1
# C and M f1
Definition 4.1 (Labeled signature #LH )
Let LH be a label hierarchy. A signature of a label-based language LLB with
LH (called a labeled signature) is a tuple
. (S, < s ) is a label-based sort-hierarchy,
. C, F, P are sets of constant symbols, function symbols and predicate symbols
of labels with C # F #
. D is a set of sort declarations such that
for every L fn
(function declaration),
# D for every L pn
A labeled signature can include more than one sort declaration for each symbol
in C # F # P . For example, for John c
# C, we have the constant declarations
human s and John c : animal s in D. For each label L # LB, if L fn
and L pn+1
some of their sort declarations might be di#erent but the
condition that L fn : L s
must be satisfied.
In a label-based language, we can view terms and formulas as compositions
of mere labels when the role of each label is undescribed. We suppose that
the expression
is a formula of the form A # B where A, B are atomic formulas. Then, we
recognizes that L 1 (x: are atomic formulas, and the positions
of the labels determine that L 1 , L 3 are unary predicates and L 2 , L 4 are the sorts
of variables x, y. In rigorous formalism, symbols in any formula must respectively
have their unique roles and defer to a labeled signature #LH . For example, we
have
8 Ken KANEIWA
where p1 and s indicate their unique roles as a unary predicate and a sort
respectively. We define expressions of the language LLB : label terms and label
formulas as follows.
Definition 4.2 (Label terms of sort L s)
The set TERML s 0
of label terms of sort L sis defined inductively by the following
rule:
, . , t L s
where
is a label
term of sort L s
s is a label term of sort M s with M s < s L s
The set of label terms of all sorts is denoted by
#S
TERML s .
Example 4.1
Consider the following label terms:
The labels John and Tom are used as constants, the label father is as a unary
function, and the label human is as a sort.
Definition 4.3 (Label formulas)
The set FORM of label formulas is defined inductively by the following rule:
A ::= L pn (t L s, . , t L s
where
Example 4.2
To construct an atomic formula, a label is employed as an n-ary predicate. For
example, the label father is a unary predicate in the following formula:
father p1 (John c : human s )
whereas the same label is a unary function father f1 in Example 4.1.
4.2 Semantics
The semantics of a label-based language LLB is defined in the usual
manner of order-sorted logic. We interpret a label hierarchy LH in restricted
Resolution for Label-based Formulas in Hierarchical Representation 9
structures. Normally, a sort-hierarchy is interpreted by a subset relation of sorts.
In contrast, the interpretation of a label hierarchy implies many relationships
among constants, functions, predicates and sorts (i.e. subordinate relations over
holds in a label hierarchy
LH, then the labels L i , L j can be regarded semantically as various symbols in
S#C#F#P . This observation leads to simple sublabel relations and complicated
sublabel relations.
Simple sublabel relations are obtained by the same role symbols as follows

relation as I(L s
subpredicate relation as I(L pn
there are L X
and I(L X
denotes an interpretation of symbol L X
. A subsort relation L s
of sorts (resp. a subpredicate relation L pn
of n-ary predicates)
can be interpreted by the subset relation of I(L s
and I(L pn
)). For example, let human # animal and parent # ancestor for
human, animal, ancestor, parent # LB. Then, the simple sublabel relations
human s
animal s and parent p2
ancestor p2 are interpreted by I(human s
I(animal s ) and I(parent p2 ) # I(ancestor p2 ). Furthermore, constants and functions
may have a semantic association with the same role symbols, but in this
paper we do not assume their sublabel relations.
Complicated sublabel relations combined by di#erent role symbols are
conceivable as in the following:
relation of constants and sorts as I(L c
subset relation of the ranges of functions and sorts as
{u | (u 1 , . , un , u) # I(L fn
subset relation of sorts and unary predicates as I(L s
In semantics, constant and function symbols are interpreted as mappings into
individuals, and sort symbols are interpreted as sets of individuals. Hence, each
constant (and function) must belong to the sorts denoted by the same label and
its superlabels. For all L c
, the membership relation I(L c
and for all L f
, the subset relation {u | (u 1 , . , un , u) # I(L fn
holds. On the other hand, both unary predicates and sorts correspond
to sets of individuals, so that L s
is interpreted by the subset rela-
tion I(L s
). Analogously, the inverse L p1
j is interpreted as
I(L p1
). For example, let John # human and father # animal
for John, father, human, animal # LB. The complicated sublabel relations
John c
animal s , father f1
animal s and human s
animal p1 are respectively
interpreted by I(John c
I(animal s ) and I(human s
Under these semantic specifications, we define restricted structures on a
labeled signature #LH as follows.
Definition 4.4 (#LH -structure)
Let #LH be a labeled signature. A sorted structure M is a pair (U, I) of a
nonempty set U and an interpretation function I for S # C # F # P such that:
1. I(L s
2.
3. I(L fn
4. I(L pn
A #LH -structure M is a sorted structure such that for all D, the
following conditions hold:
1. I(L s
2. I(L pn
3. I(L c
4. {u | (u 1 , . , un , u) # I(L fn
5. I(L s
6. I(L p1
Remark. Although each #LH -structure satisfies the additional conditions for
the labeled signature #LH , the conditions are imposed only on the symbols introduced
in a label-based language LLB . For each label, any kinds of symbols
are not always introduced. For example, for the labels ancestor, animal #
LB, we can define ancestor p1 , animal p1 , ancestor p2
# P but animal p2
# P in
LLB . In this case, the sublabel relation ancestor # animal imposes the condition
I(ancestor p1 ) # I(animal p1 ) but does not the condition I(ancestor p2
I(animal p2 ).
A variable assignment on a #LH -structure is a mapping
U such that #(x: L s
. The variable assignment
Resolution for Label-based Formulas in Hierarchical Representation 11
#[x: L s /d] is defined as (# - {(x: L s , #(x: L s ))}) # {(x: L s , d)}.
Definition 4.5 (#LH -interpretation)
A #LH -interpretation I is a pair (M, #) where M is a #LH -structure and # is a
variable assignment on M . The denotation
is defined by the following rules:
. [[x: L
.
.
, . ,
#) be a #LH -interpretation. The #LH -interpretation I[x: L s /d]
denotes (M, #[x: L s /d]).
Definition 4.6 (Satisfaction relation)
#) be a #LH -interpretation and F be a label formula. The satisfaction
relation I |= F is defined by the following rules:
. I |= L pn
. I |= -A i# I #|= A,
. I |= A # B i# I |= A and I |= B,
. I |= A # B i# I |= A or I |= B,
. I |= A # B i# I #|= A or I |= B,
. I |= #x: L s A i# for all d # I(L s ), I[x: L s /d] |= A,
. I |= #x: L s A i# for some d # I(L s ), I[x: L s /d] |= A.
Let F be a label formula and # be a set of label formulas. F is #LH -satisfiable if
there exists a #LH -interpretation I such that I |= F (I is called a #LH -model
of F ). # is #LH -satisfiable if there exists a #LH -interpretation I such that for
all F #, I |= F (I is called a #LH -model of #).
-5 Inference system
5.1 Deduction rules
We consider reasoning for clausal label formulas with a label hierarchy
LH. Let l i be an atomic formula or the negation of an atomic formula. The
clausal form l 1 # l n (n # 0) (called a label clause) expresses the label
formula of the universal closure #x 1 - #xm (l 1 # l n ) where x 1 , . , xm are
all the variables occurring in l 1 # l n . The empty clause
by #. We here show enriched deduction for label clauses that conforms to the
interpretation of the simple and complicated sublabel relations we explained in
Section 4.2. Let C be a label clause and -
- be a sequence t 1 , . , t n of label terms.
For a label hierarchy LH, we have the following deduction rules:
(1) L pn
if L pn
(2)
if L s
if L c
k and L s
if L s
C[L fn
if L fn
k and L s
there are L X
and C[t] denotes a label clause C where a term t occurs.
5.2 Labeled substitution and resolution rules
To conform to a practical viewpoint, we will adopt a refutation proof
method obtained by resolution for clausal forms. As a variant of the deduction
system, we develop a resolution system for label clauses, containing sorted and
labeled substitutions and hierarchical resolution rules.
The subsort relation L s
results in deduction rule (2), which can
be implemented by sorted substitutions in the resolution system.
Definition 5.1 (Sorted substitution)
A sorted substitution is a mapping # from a finite set of sorted variables to
TERM such that #(x: L s
i and #(x: L s
Deduction rules (3) and (5) according to the complicated sublabel relations
j and L fn
(explained in Section 4.2) carry out the replacements
of x: L s
into L c
and L fn
. To incorporate these replacements into res-
olution, we define a labeled substitution by extending the sorted substitution.
Definition 5.2 (Labeled substitution)
A labeled substitution is a mapping # + from a finite set of sorted variables to
TERM such that for each variable x: L s
Dom(#), the following condition holds:
Resolution for Label-based Formulas in Hierarchical Representation 13
is a sorted substitution.
A labeled substitution # + is expanded to label terms and formulas E, denoted
by E# . Let E,E # be expressions. A labeled substitution # + is a unifier for E
most general (denoted
by mgu) if for every unifier #
for there exists a labeled substitution
# such that #
#. In order to find a unique mgu, we assume that every
sort-hierarchy is a lower semi-lattice, i.e., there exists the greatest lower bound
for any two sorts. Even if a sort-hierarchy is not a lower semi-lattice, we can
reconstruct it to be the structure, as discussed by Cohn.
Deduction rule (1) captures the interpretation of a subpredicate relation
of n-ary predicates, and deduction rule (4) actualizes that a subset
relation L s
of sorts and unary predicates makes L p1
) valid. These
deduction rules are embedded in the hierarchical resolution rules we will present
as below.
Definition 5.3 (Hierarchical resolution rules)
be label terms, A, A # be atomic label formulas and C, C # be label
clauses. The resolution system for LLB includes the following hierarchical resolution
rules:
Resolution principle
is a mgu for A and A # .
Sublabel rule
-L pn
Elimination rule
, or t#
14 Ken KANEIWA
Reflexivity rule
Transitivity rule
The hierarchical resolution rules are similar to the subsort resolution
rule and the elimination rule (in Section 2), since our resolution system is an
extension of the sorted resolution system with sort predicates. In other words,
ordinary sorted resolution systems correspond to the hierarchical resolution system
without the sublabel rule, the elimination rule and labeled substitutions.
Moreover, the sorted resolution system with sort predicates corresponds to the
hierarchical resolution system without the sublabel rule for n-ary predicates
(n > 1) and labeled substitutions.
The hierarchical resolution system is applied to a knowledge base consisting
of a labeled signature and a set of label clauses.
Definition 5.4 (Knowledge base)
Let LH be a label hierarchy. A knowledge base KB is a pair (#LH , #) where
#LH is a labeled signature with LH and # is a nonempty finite set {C 1 , C 2 , .}
of label clauses except for the empty clause.
We write KB |= C if, for every #LH -model I of # in KB, I |= C.
Definition 5.5 (Consistency)
#) be a knowledge base. We write KB #LH C if C is derivable
from # in KB by applying hierarchical resolution rules. A knowledge base KB
is inconsistent if KB #LH #, and it is consistent otherwise.
The hierarchical relationships among labels generate new logical conclusions
and inconsistent formulas, which are not treated in ordinary sorted
inference systems.
Proposition 5.1
Let #LH be a labeled signature and #) be a knowledge base. KB
is inconsistent if and only if there exists at least one of the following inconsistent
sets
} with KB #LH A 1 , . , KB #LH An :
Resolution for Label-based Formulas in Hierarchical Representation 15
{-L p1 (t)} with t # TERML s ,
{L pn
(-L pn
{-L p1
{-L p1
(L fn
where
Proof. (#) For each inconsistent set, the empty clause can be derived by the
resolution system. (#) Any knowledge base KB does not contain the empty
clause. So, in order to derive the empty clause, at least one resolution rule
must be applied to KB. The resolution principle is applied when the inconsistent
set {A, -A} exists. The sublabel rule can derive the empty clause
if there exists the set {L pn
(-L pn
(-)}. For an application of the elimination
rule, we can conclude that there is either {-L p1 (t)}, {-L p1
{-L p1
(L fn
Proposition 5.2
Let #LH be a labeled signature, # + be a labeled substitution, C be a label clause
and I be a #LH -interpretation. If I |= C, then I |= C#
Proof. Let
n be all the free variables occurring in C, and define
| v: L s
holds. For
we have to check the three
cases:
. For (i), I |=
is a sorted substitution. (ii) if #
then the condition I(L c
in the #LH -structure entails I |= C#
} by the condition {u | (u 1 , . , un , u) #
I(L fn
in the #LH -structure. Therefore, we can derive I |= C#
Theorem 5.1
Let #LH be a labeled signature, C be a label clause and KB be a knowledge
base. If KB #LH C, then KB |= C.
Proof. We verify it for applying (i) sublabel rule and (ii) elimination rule. For (i),
suppose I |= -L pn
(-) #C and I |= L pn
be a mgu for -
- and -
By Proposition 5.2, we have I |= -L pn
Ken KANEIWA
fail
Fig. 3 Resolution steps for a knowledge base
with
let I |= -L p1
C. The conditions of the #LH -structure imply I |= L p1
and then I #|= -L p1
Theorem 5.2
Let #LH be a labeled signature and KB be a knowledge base. If KB has a
#LH -model, then KB is consistent.
Proof. Suppose that KB has a #LH -model. Let us assume that KB is inconsis-
tent. According to Proposition 5.1, there is an inconsistent set {A
such that KB #LH A 1 , . , KB #LH An . Theorem 5.1 and Proposition 5.2 lead
to KB |= A . However, the inconsistent set has no #LH -
model. This is a contradiction. Therefore, KB is consistent.
Corollary 5.1
Let #LH be a labeled signature and KB be a knowledge base. If KB #LH #,
then KB has no #LH -model.
Proof. This can be straightforwardly proved by Theorem 5.2.
5.3 An example of resolution
We give an example of resolution with respect to the terminological
hierarchy shown in Fig. 2. Let the label hierarchy
Resolution for Label-based Formulas in Hierarchical Representation 17
ancestor # animal, descendant # animal, parent # ancestor,
child # descendant, son # child, daughter # child,
father # parent, mother # parent, human # animal,
John # human, Tom # human,
and let the labeled signature
{ animal, ancestor, descendant, human, parent, child,
father, mother, son, daughter },
{ John, Tom },
{ father, mother },
{ animal, ancestor, descendant, human, parent, child,
father, mother, son, daughter },
{ ancestor, descendant, parent, child, father, mother,
son, daughter },
{ John: # human, Tom:# human,
human # human, father: human,
human:#, won in a lottery: #, lucky: #, - }.
Let the knowledge base
{ father(John: human),
won in a lottery(father(T om: human)),
won in a lottery(x) # lucky(x) }.
The first and second facts state that John is a father and Tom's father won in a
lottery, and the rule means that if x won in a lottery, then x was lucky. For the
knowledge base KB, consider the following queries:
In order to decide the answer (yes or no) of each query in KB, the resolution
system attempts to derive the empty clause from the negation of the query and
the knowledge base KB. By applying hierarchical resolution rules, the derivation
processes are given as in Fig. 3. The derivations for the first and second queries
are successful, but the derivation for the final query fails.
Conclusions
Ken KANEIWA
This paper investigates general representation and reasoning for the hierarchies
composed by di#erent kinds of first-order symbols. We have presented
a label-based language as an extended order-sorted logic which provides the
label-based expressions: a label hierarchy, label terms and label formulas. In
the semantic connections of various symbols in the language, a label hierarchy
can be commonly employed to express not only a sort-hierarchy but also hierarchies
of di#erent types of subordinate relations. To develop its reasoning
system, we have defined labeled substitutions and hierarchical resolution rules
that are extensions of sorted substitutions and sorted resolution rules respec-
tively. Beierle et al. enhanced the reasoning power of an order-sorted resolution
system by adding inference rules of sort predicates. Along the way, we have
achieved a further refinement of the sorted resolution system in the label-based
language.
We will need to redesign the hierarchical resolution rules in order to
make the system complete. The derivability of the system is still insu#cient to
correspond to the class of #LH -structures.

Acknowledgment

We thank the anonymous referees for many useful suggestions on this
paper. This research has been partially supported by the Kayamori Foundation
of Informational Science Advancement and the Ministry of Education, Science,
Sports and Culture, Grant-in-Aid for Scientific Research (14780311).



--R



















--TR
A mechanical solution of Schubert''s steamroller by many-sorted resolution
Login: A logic programming language with built-in inheritance
A more expressive formulation of many sorted logic
Many-sorted unification
Attributive concept descriptions with complements
An order-sorted logic for knowledge representation systems
Logical foundations of object-oriented and frame-based languages
An order-sorted resolution in theory and practice
Event, property and hierarchy in order-sorted logic
An Order-Sorted Resolution with Implicitly Negative Sorts
terminological knowledge;label-based expressions;order-sorted logic;knowledge representation;resolution system