We present a two-sorted algebra, called a Peirce algebra, of relations and sets interacting with each other. In a Peirce algebra, sets can combine with each other as in a Boolean algebra, relations can combine with each other as in a relation algebra, and in addition we have both a set-forming operator on relations (the Peirce product of Boolean modules) and a relation-forming operator on sets (a cylindrification operation). Two applications of Peirce algebras are given. The first points out that Peirce algebras provide a natural algebraic framework for modelling certain programming constructs. The second shows that the so-called terminological logics arising in knowledge representation have evolved a semantics best described as a calculus of relations interacting with sets.
Also available as Tech. Rep. MPI-I-92-229,
MPI für Informatik, Saarbrücken, Germany
(July 1992).
DVI,
PostScript
And available as Research Report RR 140, Department of Mathematics,
Univ. of Cape Town, South Africa (August 1992).
An extended abstract appears in
Nivat, M., Rattray, C., Rus, T. and Scollo, G. (eds),
Algebraic Methodology and Software Technology:
Proceedings of AMAST'93.
Workshops in Computing Series, Springer, London, 165-168
(1994).
DVI,
PostScript
Non-classical logics, and in particular many-valued logics, are increasingly used in the study of formal aspects of computing. or example, a recent paper by P.F. Gibbins in this Journal presents a 3-valued propositional logic for VDM. In the use of such logics one naturally relies on earlier work done by logicians, a case in point being Gibbin's use of the concept of autodescriptivity, introduced by N. Rescher. The purpose of this Note is to sound a warning that Rescher's exposition of autodescriptivity is seriously flawed, and to clarify the autodescriptivity of the logic of VDM.
This paper deals with terminological representation languages for KL-ONE-type knowledge representation systems. Such languages are based on the two primitive syntactic types called concepts and roles, which are usually represented model-theoretically as sets and binary relations respectively. Rather than following the model-theoretic route, we show that the semantics can be naturally accommodated in the context of an equational algebra of relations interacting with sets. Equational logic is then a natural vehicle for computing subsumptions, both of concepts and of roles. We thus propose the algebraic rather than model-theoretic computation of subsumption.
Also in Lehmann, F. (ed.) (1992),
Semantic Networks in Artificial Intelligence, Modern
Applied Mathematics and Computer Science Series 24, Pergamon
Press, Oxford, UK.
Also available as Tech. Rep. TR-ARP-3/90, Automated Reasoning
Project, Australian National Univ., Canberra.
In this paper we focus on the application of description logics to
natural language processing. In cooperation with the PRACMA Project we
have been developing a suitably extended knowledge representation
system, called MOTEL.
In our approach to agent modelling and natural language processing we
use an extension of the well-known description language ALC. Our system
MOTEL serves on one hand as a knowledge base for the natural language
front-end, and on the other hand, it provides powerful logical
representation and reasoning components. As our approach is logic based
we hope that this enhances the overall capabilities of the natural
language processing system.
We present a brief overview of MOTEL and the different extensions we are
working on, i.e. modal extension of description logics, a
cardinality-based approach to quantitative information, reason
maintenance, probablistic, non-monotonic, and abductive reasoning.
MOTEL is a logic-based knowledge representation languages of the KL-ONE family. It contains as a kernel the KRIS language which is a decidable sublanguage of first-order predicate logic (see Baader and Hollunder (1990)). Whereas KRIS is a single-agent knowledge representation system, i.e. KRIS is only able to represent general world knowledge or the knowledge of one agent about the world, MOTEL is a multi-agent knowledge representation system. The MOTEL language allows modal contexts and modal concept forming operators which allow to represent and reason about the believes and wishes of multiple agents. Furthermore it is possible to represent defaults and stereotypes. Beside the basic resoning facilities for consistency checking, classification, and realization, MOTEL provides an abductive inference mechanism. Furthermore it is able to give explanations for its inferences.
This paper reports on empirical performance analysis of four modal
theorem provers on benchmark suites of randomly generated formulae.
The theorem provers tested are
the Davis-Putnam-based procedure KSAT, the
tableaux-based system KRIS,
the sequent-based Logics Workbench,
and a translation approach combined with the first-order theorem
prover SPASS.
Our benchmark suites are sets of multi-modal formulae in a certain
normal form randomly generated according to the scheme of
Giunchiglia and Sebastiani (1996a,1996b).
We investigate the quality of the random modal formulae and show that
the scheme has some shortcomings, which may lead to mistaken conclusions.
We propose improvements to the evaluation method
and show that the translation approach has superior
computational behaviour compared to the other three approaches.
The short version is to appear in
the Proc. IJCAI'97.
Some pictures and the routines for the random generation of modal formulae,
the functional translation and simplification can be found on the page:
Empirical analysis of
decision procedures for modal logic.
This paper investigates the evaluation method of decision procedures for multi-modal logic proposed by Giunchiglia and Sebastiani as an adaptation from the evaluation method of Mitchell et al. of decision procedures for propositional logic. We compare three different theorem proving approaches, namely, the Davis-Putnam-based procedure KSAT, the tableaux-based system KRIS and a translation approach combined with first-order resolution. Our results do not support the claims of Giunchiglia and Sebastiani concerning the computational superiority of KSAT over KRIS, and an easy-hard-easy pattern for randomly generated modal formulae.
The long version is available as Research Report MPI-I-97-2-003, Max-Planck-Institut für Informatik, Saarbrücken, Germany.
This paper reports on an empirical performance analysis of four modal
theorem provers on benchmark suites of randomly generated formulae.
The theorem provers tested are
the Davis-Putnam-based procedure KSAT, the
tableaux-based system KRIS,
the sequent-based Logics Workbench,
and a translation approach combined with the first-order theorem
prover SPASS.
Our benchmark suites are sets of multi-modal formulae in a certain
normal form randomly generated according to the scheme of
Giunchiglia and
Sebastiani (1996a,b).
We investigate the quality of the random modal formulae and show that
the scheme has some shortcomings, which may lead to mistaken conclusions.
We propose improvements to the evaluation method
and show that the translation approach has superior
computational behaviour compared to the other three approaches.
See also On Evaluating Decision Procedures for Modal Logics, to appear in Proc. IJCAI'97.
Normal modal logics can be defined axiomatically as
Hilbert systems, or semantically in terms of Kripke's possible
worlds and accessibility relations. Unfortunately there are Hilbert
axioms which do not have corresponding first-order properties for the
accessibility relation. For these logics the standard semantics-based
theorem proving techniques, in particular, the relational translation
into first-order predicate logic, do not work.
There is an alternative translation, the so-called functional
translation, in which the accessibility relations are replaced by certain
terms which intuitively can be seen as functions mapping worlds to
accessible worlds. In this paper we show that from a certain point of
view this functional language
is more expressive than the relational language, and that certain
second-order frame properties
can be mapped to first-order formulae expressed in the
functional language.
Moreover, we show how these formulae can be computed automatically
from the Hilbert axioms.
This extends the applicability of the functional translation method.
Also available as Research Rep. MPI-I-95-2-008, MPI für Informatik, Saarbrücken (May 1995). PostScript,
In the logic of graded modalities it is possible to talk about sets of finite cardinality. Various calculi exist for graded modal logics and all generate vast amounts of case distinctions. In this paper we present an optimized translation from graded modal logic into many-sorted predicate logic. This translation has the advantage that in contrast to known approaches our calculus enables us to reason with cardinalities of sets symbolically. In many cases the length of proofs for theorems of this calculus is independent of the cardinalities. Our translation is sound and complete.
Also available as Tech. Rep. MPI-I-95-2-008, MPI für Informatik, Saarbrücken, Germany (May 1995). PostScript
Many inference systems used for concept description logics are
constraint systems that employ tableaux methods.
These have the disadvantage that for reasoning with qualified number
restrictions n new constant symbols are generated for each
concept of the form (atleast n R C).
In this paper we present an alternative method that avoids the
generation of constants and uses a restricted form of symbolic
arithmetic considerably different from the tableaux method.
The method we use is introduced in
Ohlbach, Schmidt and Hustadt (1996) for reasoning with graded
modalities.
We exploit the exact correspondence between the concept description
language ALCN and the multi-modal version of the
graded modal logic K and show how the method
can be applied to ALCN as well.
This paper is a condensed version of Ohlbach et al. (May 1995).
We omit proofs and much of the technical details, but we
include some examples.
This thesis investigates terminological representation languages, as used in KL-ONE-type knowledge representation systems, from an algebraic point of view. Terminological representation languages are based on two primitive syntactic types, called concepts and roles, which are usually interpreted model-theoretically as sets and relations, respectively. I propose an algebraic rather than a model-theoretic approach. I show that terminological representations can be naturally accommodated in equational algebras of sets interacting with relations, and I use equational logic as a vehicle for reasoning about concepts interacting with roles.
Also available as Thesis-Reprint TR 011, Dept. of Mathematics, Univ. of Cape Town, South Africa.
In this paper I establish a link between KL-ONE-based knowledge representation concerned with terminological representation and the work of P. Suppes (1976,1979,1981) and M. Böttner (1985,1989) in computational linguistics. I show how this link can be utilised for the problem of finding adequate terminological representations for given information formulated in ordinary English.
Also available as Tech. Rep. MPI-I-92-246, MPI für Informatik, Saarbrücken, Germany (October 1992). DVI, PostScript
Abstract of a talk held at the Dagstuhl Seminar on Relational Methods in Computer Science, Dagstuhl, Germany (January 1994). DVI
In this Note I prove a representation theorem for Peirce algebras
introduced in
Brink, Britz and Schmidt (1994).
I show that the class of full Peirce algebras is characterised by
the class of complete and atomic Peirce algebras in which the set of
relational atoms is restricted by two conditions.
One requires simplicity.
The other requires that each relational element can be uniquely expressed
in terms of Boolean atoms, or equivalently, that each relational element
can be uniquely expressed in terms of relational
identity atoms or relational points.
The result parallels the representation theorems of
Jònsson and Tarski (1952), McKinsey (1940) and
Schmidt and Ströhlein (1985) for full relation algebras.
To this end I investigate the interrelationship of identity elements and
right ideal elements inside any relation algebra and the
interrelationship of identity elements, right ideal elements and Boolean
set elements inside Peirce algebras.
Each form a Boolean algebra.
Inside relation algebras the Boolean algebra of elements below the
identity and the Boolean algebra of right ideal elements are isomorphic.
Inside Peirce algebras each is isomorphic to the underlying Boolean
algebra which is separate from the underlying relation algebra.
As a special case, I correlate the atom sets of these three different but
isomorphic Boolean algebras.
Peirce algebras have many applications, in
modal logics, in particular, dynamic logic, arrow logic, dynamic modal
logic, in logics of programs and in KLONE-based knowledge representation.
See
Brink etal. (1994).
Of particular interest is the class of concrete Peirce algebras and the
class of full Peirce algebras.
The first characterisation of full Peirce algebras appears in the PhD
Thesis of De Rijke (1993).
This is also the first published representation theorem for Peirce algebras.
In his characterisation de Rijke
uses two conditions (besides simplicity), one on the Boolean set algebra
and another on the relation algebra.
These are the algebraic analogues of two irreflexivity rules required
for the completeness proof of the logical analogue of Peirce algebras,
dynamic modal logic.
This Note shows that in Peirce algebras,
because the Boolean set algebra is determined by the
relation algebra, one condition, namely one on the relation algebra,
is sufficient for the representation theorem.
In contrast to the proof of de Rijke which is obtained from the
completeness proof of dynamic modal logic, the proof we present is
algebraic.
In this Note, I show that the classes RA of relation algebras and PA of Peirce algebras are equivalent in a certain sense. Since relation algebras and Peirce algebras are structurally different, the former are one-sorted algebras and the latter are two-sorted algebras, the usual notion of equivalence is inappropriate. Instead, I use the notions of equipollence and equipollent extension for classes of algebras, which are defined in Tarski and Givant (1987) for logics. The result has applications in modal logic, KL-ONE based knowledge representation and other fields.
In this paper I focus on graphic forms of representation for KL-ONE-based knowledge representation languages. I consider the semantic network formalism due to R. Brachman and the system of existential graph due to C. S. Peirce. The semantic networks of Brachman are very weak. Not all the information expressible in a terminological language can be represented as a semantic network. By contrast, the system of Peirce is very powerful. I show how any information expressed in any terminological language can be transformed and displayed as an existential graph and propose that existential graphs be used to complement the semantic network representations.
This paper aims to enhance the practical applicability of relational grammars, which have been devised for the semantic analysis of natural language. We focus on their application in knowledge representation. In particular, we address how the representation problem for KL-ONE-based knowledge representation systems can be automatically solved with the help of relational grammars. New rules are presented for natural language formulations, like has sons and has at least two sons, commonly arising in application domains. For accommodating the latter kind of sentences we introduce a new class of so-called (concrete) graded Peirce algebras. A graded Peirce algebra is a Peirce algebra endowed with a countable set of numerical quantifier operations.
The paper shows satisfiability in many propositional modal systems, including K, KD, KT and KB, their combinations as well as their multi-modal versions, can be decided by ordinary resolution procedures. This follows from a general result that resolution and condensing is a decision procedure for the satisfiability problem of formulae in so-called path logics. Path logics arise from propositional and normal uni- and multi-modal logics by the optimised functional translation method. The decision result provides an alternative decision proof for the relevant modal systems, and related systems in artificial intelligence. However, this alone is not very interesting. A more far-reaching consequence of the result has practical value, namely, any standard first-order theorem prover that is based on resolution can serve as a reasonable and efficient inference tool for modal reasoning.
Earlier version available in Oct. 1996: Abstract, BiBTeX, HDVI (view with xhdvi), PostScript.
The paper shows satisfiability in many propositional modal systems can be decided by ordinary resolution procedures. This follows from a general result that resolution and condensing is a decision procedure for the satisfiability problem of formulae in so-called path logics. Path logics arise from propositional and normal uni- and multi-modal logics by the optimised functional translation method. The decision result provides an alternative decision proof for the relevant modal logics (including K, KD, KT and KB, their combinations as well as their multi-modal versions), and related systems in artificial intelligence. This alone is not interesting. A more far-reaching consequence of the result has practical value, namely, any standard first-order theorem prover that is based on resolution can serve as a reasonable and efficient inference tool for modal reasoning.
The extended abstract version is to appear in Kracht, M., de Rijke, M., Wansing, H. and Zakharyaschev, M. (eds) (1997), Advances in Modal Logic `96, CSLI Publications. Abstract, BiBTeX, PostScript.
This thesis studies the optimised functional translation of propositional modal logics to first-order logic, and first-order resolution as a means for realising modal reasoning. The optimised functional translation maps modal logics to a lattice of clausal logics, called path logics. The general apparatus of inference for path logics is theory resolution. We show that satisfiability in basic path logic and certain extensions can be decided by resolution and condensing without requiring additional refinement strategies. We propose an improved theory unification algorithm for S4, and we present a calculus of ordered E-resolution with normalisation. We show also that some essentially second-order modal logics convert to path logics, which can be exploited for accomodating inference for modal logics with numerical quantifiers in a calculus of resolution and simple arithmetic.
This paper is concerned with the unification problem in the path logics associated by the optimised functional translation method with the modal logics K, KD, KT, KD4, S4 and S5. It presents improved unification algorithms for certain forms of the right identity and associativity laws. The algorithms employ mutation rules, which have the advantage that terms are worked off from the outside inward, making paramodulating into terms superfluous.