
Viorica Sofroniestokkermans
The main goal of this paper is to explain the link between the algebraic models and the Kripkestyle models for certain classes of propositional nonclassical logics. We consider logics that are sound and complete with respect to varieties of distributive lattices with certain classes of wellbehaved operators for which a Priestleystyle duality holds, and present a way of constructing topological and nontopological Kripkestyle models for these types of logics. Moreover, we show that, under certain additional assumptions on the variety of the algebraic models of the given logics, soundness and completeness with respect to these classes of Kripkestyle models follows...

Juha Nurmonen
We give a combinatorial method for proving elementary equivalence in firstorder logic FO with counting modulo n quantifiers D n . Inexpressibility results for FO(D n ) with builtin linear order are also considered. For instance, the class of linear orders of length divisible by n + 1 cannot be expressed in FO(D n ). Using this result we prove that comparing cardinalities or connectivity of ordered graphs are not definable in FO(D n ). We also show that the height of complete nary trees cannot be expressed in FO(D n ) with linear order. Interpreting the predicate y =...

Melvin Fitting
. Firstorder modal logic, in the usual formulations, is not sufficiently expressive, and as a consequence problems like Frege's morning star/evening star puzzle arise. The introduction of predicate abstraction machinery provides a natural extension in which such di#culties can be addressed. But this machinery can also be thought of as part of a move to a full higherorder modal logic. In this paper we present a sketch of just such a higherorder modal logic: its formal semantics, and a proof procedure using tableaus. Naturally the tableau rules are not complete, but they are with respect to a Henkinization of the...

M. A. Thornton; J. D. Gaiche; J. V. Lemieux
Integer multiplication is a necessary operation for performing many tasks relevant to multimedia and telecommunications processes. Here, we discuss the results of an investigation into the effectiveness of automated synthesis tools as related to a sample of modern Programmable Logic Devices (PLDs). Although it is generally accepted that superior results in terms of required area and circuit delay can generally be obtained through manual implementation of such circuits, the exclusive use of automated synthesis tools based upon an original specification in terms of a Hardware Description Language (HDL) is presented here. The results of several different approaches to multiplier architectures...

Habib Youssef; Sadiq M. Sait; Salman A. Khan
The topology design of campus networks (CNs) is a hard constrained combinatorial optimization problem. Therefore, we resort to heuristics to come up with desirable solutions. A desirable solution must optimize several conflicting objectives such as minimization of cost, minimization of network delay, and minimization of maximum number of hops etc. Furthermore, some of the objectives are imprecise. Fuzzy Logic provides a suitable mathematical framework in such a situation. In this paper, we present an approach based on Simulated Evolution algorithm for the design of campus network topology. The two main phases of the algorithm, namely, evaluation and allocation, have been...

Herman Geuvers; Erik Poll; Jan Zwanenburg
. We present an extension of type theory with a fixed point combinator Y . We are particularly interested in using this Y for doing unbounded proof search in the proof system. Therefore we treat in some detail a typed calculus for higher order predicate logic with inductive types (a reasonable subsystem of the theory implemented in [Dowek e.a. 1991]) and show how bounded proof search can be done in this system, and how unbounded proof search can be done if we add Y . Of course, proof search can also be implemented (as a tactic) in the meta language....

Wolfgang May; Peter H. Schmitt
. Tableaubased proof systems have been designed for many logics extending classical firstorder logic. This paper proposes a sound tableau calculus for temporal logics of the firstorder CTLfamily. Until now, a tableau calculus has only been presented for the propositional version of CTL. The calculus considered operates with prefixed formulas and may be regarded as an instance of a labelled deductive system. The prefixes allow an explicit partial description of states and paths of a potential Kripke counter model in the tableau. It is possible in particular to represent path segments of finite but arbitrary length which are needed to...

Hubert Dubois And; Hubert Dubois
. ELAN is a declarative language based on rewriting logic. The ELAN language is based on labelled conditional rewrite rules and on strategies for controlling their application. ELAN provides a strategy language to control labelled rules. In this paper we show how to use the ELAN strategy language for planning. We describe how to encode situations and actions and take advantage of ELAN strategies to build plans. We give an example of our approach by describing an elevator controller. 1 Introduction Among numerous contributions in the area of logic and changes, rewriting logic has been proposed in [MOM94] as a...

Thornton Moore Cordova; M. A. Thornton
Digital circuit output probabilities provide meaningful information regarding the behavior of combinational logic circuits. The computation of the probability values can be computationally expensive when Boolean equations or netlists are used. When the circuits are represented by compact decision diagrams (DD), efficient algorithms exist for determining the probability values. The use of the probabilities based on decision diagram representations are examined here. Specifically, research results of investigations into spectra computation, synthesis, symmetry detection and DD reordering are surveyed. 1 Introduction The circuit output probability for a combinational logic circuit can be defined as the probability that a given output will...

Ian Horrocks; Graham Gough
This paper describes the logic ALCH R + , which extends ALC R + with a primitive role hierarchy, and presents an appropriate extension to the ALCR + satisfiability testing algorithm. ALCH R + is of interest because it provides useful additional expressive power and, although its satisfiability problem is Exptime complete, the algorithm is relatively simple and is amenable to optimisation. 1 Introduction The importance of transitively closed roles in Description Logics (DLs) has long been recognised [PL94], particularly in domains which are concerned with physically composed objects, for example in medicine [HRG96] and engineering [Sat95]. The logic ALC+...

Gooday And Cohn; J M Gooday; A G Cohn
Visual computer languages exploit the natural language of diagrams and pictures to provide a simple and intelligible approach to programming. Unfortunately, it is difficult to provide them with a formal syntax and semantics. In this paper we show how the RCC spatial calculus can be used to provide an unambiguous, formal description of such languages by systematically describing the syntax of Pictorial Janus. Keywords: Visual programming languages, spatial languages 1 Introduction Computer programming would be much simpler if programming languages were somehow closer to natural language. Unfortunately, specifying algorithms and data structures unambiguously requires a degree of formality not usually...

V. Manca; Vincenzo Manca
) V. Manca June 23, 1997 ADDR: Corso Italia 40,56125 Pisa,Italy. TEL: +3950887111. FAX: +3950887226 Logical Formalizations of Syntactical Properties (Extended Abstract) Vincenzo Manca Universit`a di Pisa Dipartimento di Informatica Corso Italia, 40  56125 Pisa  Italy email: mancav@di.unipi.it 1 Introduction Assume the `marvelous' 7 logical symbols: !;:;;;$;8;9 with the standard syntactical and semantical first order logical notions (equality predicate = is assumed in its usual usage) that can be found in introductory treatises or basic chapters of textbooks in mathematical logic (cf., for example, [1], [6], [15], [16], [3], [2] [13]): 1. variables and constants 2. predicates and...

Yuri Kaluzhny; Alexei Yu. Muravitsky
Introduction Much recent work in artificial intelligence has required formal techniques for working with incomplete knowledge. The new approach clearly necessitated that a distinction be made between logic and the action (i.e. two components of intelligence: the epistemological and the heuristic; cf. [MCC 69]). However, certain new inference procedures associated with the new approach (for example the familiar example of default logic) have, like classical logic, been based on an underlying consistent ontology. (Cf. [GIN 87a]: "It is precisely this `absence of information to the contrary' that makes the inference nonmonotonic...") 1 Philosophers were the first to call attention to...

Marco Devillers
Formal methods are mathematical techniques used to verify safetycritical systems. Recent successful verifications have been credited to newly developed computer tools which mechanically support (parts of) the verification process. My research concentrates on the mechanical support of verifications of systems described as I/O automata. I wish to show how the I/O automata model of Lynch and Tuttle can be mechanically supported, and how this support can be used in a teaching environment. The support is to be implemented in a workbench, which serves as a frontend to other tools. A central research question is how to successfully combine existing technology,...

Ian Horrocks; Sergio Tessaris
A serious shortcoming of many Description Logic based knowledge representation systems is the inadequacy of their query languages. In this paper we present a novel technique that can be used to provide an expressive query language for such systems. One of the main advantages of this approach is that, being based on a reduction to knowledge base satisfiability, it can easily be adapted to most existing (and future) Description Logic implementations. We believe that providing Description Logic systems with an expressive query language for interrogating the knowledge base will significantly increase their utility. Introduction A description logic (DL) knowledge base...

Marco Antoniotti; Bud Mishra
In this paper, we address the problem of the synthesis of controller programs for a variety of robotics and manufacturing tasks. The problem we choose for test and illustrative purposes is the standard "Walking Machine Problem," a representative instance of a real hybrid problem with both logical/discrete and continuous properties and strong mutual influence without any reasonable separation. We aim to produce a "compiler technology" for this class of problems in a manner analogous to the development of the socalled "Silicon Compilers" for the VLSI technology. To cope with the difficulties inherent to the problem, we resort to a novel...

Prabhakaran Raman; Eugene W. Stark
We consider a distributed model for the execution of logic programs, in which a process is assigned to each node of the AND/OR tree for a program, and in which each process communicates directly only with its immediate neighbors in the tree. We derive an interpreter, or execution method, for this model, in which each node process maintains in its state a set of substitutions that represents a current local approximation to the set of answer substitutions. Execution consists of each process repeatedly sending its current state to its neighbors, and updating its state using information it receives. Eventually, "exact"...

Martin Abadi; Gordon D. Plotkin
We define two logics of safety specifications for reactive systems. The logics provide a setting for the study of composition rules. The two logics arise naturally from extant specification approaches; one of the logics is intuitionistic, while the other one is linear. iv Contents 1 Introduction 1 2 Overview 3 2.1 A calculus of sets of behaviors : : : : : : : : : : : : : : : : : : 3 2.2 A calculus of sets of processes : : : : : : : : : : : : : : : : :...

Its Computation; Stefan Brass; Jürgen Dix; Ilkka Niemela; Teodor C. Przymusinski
In recent years, much work was devoted to the study of theoretical foundations of Disjunctive Logic Programming and Disjunctive Deductive Databases. While the semantics of nondisjunctive programs is fairly well understood, the declarative and computational foundations of disjunctive logic programming proved to be much more elusive and difficult. Recently, two new and promising semantics have been proposed for the class of disjunctive logic programs. The first one is the static semantics STATIC , proposed by Przymusinski, and, the other is the disjunctive wellfounded semantics DWFS, proposed by Brass and Dix. Although the two semantics are based on very different ideas,...

Martin Lange; Martin Leucker; Thomas Noll; Stephan Tobies
. We briefly explain the design and implementation of the newly developed tool Truth which serves as a general platform for the systematic investigation of di#erent specification languages, semantic models, and logics for concurrent systems, supported by enhanced visualisation capabilities. Modularity is achieved by employing the Rewriting Logic approach as a semantic framework for concurrency. In its current version, Truth supports tableaubased model checking for the full calculus on finite transition systems. The latter are given in terms of CCS processes for which our tool additionally o#ers interactive visualisation and simulation features. Further extensions of Truth, being in the implementation...