
Lingzhong Zhao; Tianlong Gu; Junyan Qian; Guoyong Cai
Decorated tree semantics is a goalindependent denotational semantics for Prolog that deals with the control rules of Prolog and cut operator. This semantics was designed with the aim to provide a general framework for abstract analysis of generic properties of logic programs and has been specialized into computed answer (ca) semantics and call pattern (cp) semantics. In this paper we show that the methods for achieving semantics for the “correct ” observables (i.e. observables related to successful derivations), correct partial answers (cpa) and correct call patterns (ccp) in particular, are not trivial extensions of the methods for achieving ca and...

O. Univ. Prof Dipl. ing; Dr. Techn Thomas Eiter; Abteilung Für Wissensbasierte Systeme; A Wien
und

We present a cutelimination proof for simple type theory with axiom of choice modeled after Takahashi’s proof of cutelimination for simple type theory with extensionality. The same proof works when types are restricted, for example for secondorder classsical logic with axiom of choice. 1 Introduction: Simple Type Theory

M. Fikret Ercan
Electrical engineering graduates need to be imbued with the knowledge of electronic design and software development. Furthermore, they have to be familiar with electronic components such as sensors, motors, logic devices, microprocessors and many others. This paper reports a project based learning initiative where autonomous minirobots are developed for research, education and entertainment purposes. The objective of this work is hence two folds. One is to design and develop identical robots to perform a task cooperatively so that they can be used as a platform on multirobotics research. Second, to expose students to a challenging engineering project where they can...

Servicebased systems are distributed systems which have the major advantage of enabling rapid composition of distributed applications, regardless of the programming languages and platforms used in developing and running different components of the applications. In these systems, various capabilities are provided by different organizations as services interconnected by various types of networks. The services can be integrated following a specific workflow to achieve a mission goal for users. For largescale servicebased systems involving multiple organizations, high confidence and adaptability are of prime concern in order to ensure that users can use these systems anywhere, anytime with various devices, knowing that...

Isar Stubbe; Département De Mathématique; Université Catholique De Louvain
It is common practice in both theoretical computer science and theoretical physics to describe the (static) logic of a system by means of a complete lattice. When formalizing the dynamics of such a system, the updates of that system organize themselves quite naturally in a quantale, or more generally, a quantaloid. In fact, we are lead to consider cocomplete quantaloidenriched categories as fundamental mathematical structure for a dynamic logic common to both computer science and physics. Here we explain the theory of totally continuous cocomplete categories as generalization of the wellknown theory of totally continuous suplattices. That is to say,...

Michael Melholt Quottrup
Abstract — This paper describes how a network of interacting timed automata can be used to model, analyze, and verify motion planning problems in a scenario with multiple robotic vehicles. The method presupposes an infrastructure of robots with feedback controllers obeying simple restriction on a planar grid. The automata formalism merely presents a highlevel model of environment, robots and control, but allows composition and formal symbolic reasoning about coordinated solutions. Composition is achieved through synchronization, and the verification software UPPAAL is used for a symbolic verification against specification requirements formulated in computational tree logic (CTL). In this way, all feasible...

Tom Mcdermott; Philip Ryan; Mark Sh; David Skellern; Terry Percival; Neil Weste
We have implemented the digital section of a wireless local area network (WLAN) demodulator in a reconfigurable interface card called the PCI Pamette. The entire baseband section of the demodulator has been implemented in the Pamette and a simple analog to digital mezzanine board. This is the second implementation of the demodulator, the first being a cardbased design using a mixture of discrete and reconfigurable logic. The Pamette implementation took far less time to complete than the cardbased design. Moreover, the reconfigurable substrate is much more versatile. This paper describes the Pamette implementation and discusses our experiences with the two...

Jeremy E Dawson
Communicated by Editor’s name We present a general theorem capturing conditions required for the termination of abstract reduction systems. We show that our theorem generalises another similar general theorem about termination of such systems. We apply our theorem to give interesting proofs of termination for typed combinatory logic. Thus, our method can handle most pathorderings in the literature as well as the reducibility method typically used for typed combinators. Finally we show how our theorem can be used to prove termination for incrementally defined rewrite systems, including an incremental general path ordering. All proofs have been formally machinechecked in Isabelle/HOL.

Tran Cao; Son Enrico Pontelli
Abstract. We present a declarative language, PP, for the specification of preferences between possible solutions (or trajectories) of a planning problem. This novel language allows users to elegantly express nontrivial, multidimensional preferences and priorities over them. The semantics of PP allows the identification of most preferred trajectories for a given goal. We also provide an answer set programming implementation of planning problems with PP preferences. 1

Chong H. Lee; Douglas V. Hall; Marek A. Perkowski; David S. Jun
This paper describes the concept of selftestable and selfrepairable GAL (Generic Array Logic) devices for high security and safety applications. A design methodology is proposed for selfrepairing of a GAL which is a kind of EPLDs (Electrically Programmable Logic Devices). The faultlocating and faultrepairing architecture with electrically reconfigurable GALs is presented. It uses universal test sets, faultdetecting logic, and selfrepairing circuits with spare devices. The design method allows to detect, diagnose, and repair of all multiple stuckat faults which might occur on E 2 CMOS cells in programmable AND plane. A selfrepairing methodology is presented, based on our design architecture....

Frank M. Brown
Abstract: The nonmonotonic logic called Autoepistemic Logic is shown to be representable in a monotonic Modal Quantificational Logic whose modal laws are stronger than S5. Specifically, it is proven that a set of sentences of First Order Logic is a fixedpoint of the fixedpoint equation of Autoepistemic Logic with an initial set of axioms if and only if the meaning or rather disquotation of that set of sentences is logically equivalent to a particular modal functor of the meaning of that initial set of sentences. This result is important because the modal representation allows the use of powerful automatic deduction...

Lunjin Lu
This paper presents an abstract semantics that uses information about execution paths to improve precision of data semantics by abstracting execution paths using call strings domains that have been developed for logic program analyses can be used with the new abstract semantics without modification.

Guido Governatori; Antonino Rotolo
In this paper we show that the Hilbert system of agency and ability presented by Dag Elgesem is incomplete with respect to the intended semantics. We argue that completeness result may be easily regained. Finally, we shortly discuss some issues related to the philosophical intuition behind his approach. This is done by examining Elgesem’s modal logic of agency and ability using semantics with different flavours. 1

Tran Cao; Son Enrico Pontelli
Abstract. We present a declarative language, ÈÈ, for the specification of preferences between possible solutions (or trajectories) of a planning problem. This novel language allows users to elegantly express nontrivial, multidimensional preferences and priorities over them. The semantics of ÈÈ allows the identification of most preferred trajectories of a given goal. We provide a transformation to logic programming with negation as failure, that allows the use of existing logic programming systems to solve planning problems with ÈÈ preferences. 1

Chen Zhao; Nuermaimaiti. Heilili; Shengping Liu; Zuoquan Lin
RoleBased Access Control (RBAC) has been recognized as a strategy which reduces the cost and complexity of security administration in largescale networked applications. A general family of RBAC models called RBAC96 was proposed by Sandhu et al. [1], which formally defines the relations among user, role and permission using the notion of set membership. Constraints is an important aspect of RBAC, which impose restrictions on acceptable configurations of the different components of RBAC. Nevertheless, it was discussed informally in the RBAC96 model. There has been some efforts to present a logical framework for the access control models. Most of these...

Yu Yongbin; Liao Xiaofeng; Yu Juebang
Abstract A novel framework for nonManhattan channel routing considering crosstalk and wire length reduction is proposed. To handle crosstalk and wire length reduction problem, an improved nonManhattan router in the gridded routing model is developed, and a novel rerouting algorithm based on segmentrerouting technique and layer reassignment is presented. Simulation experiments demonstrate that our algorithm achieves very good results. Key words crosstalk; wire length; track; channel routing; nonManhattan; layer reassignment With the recent advances in VLSI fabrication technology, the device sizes have shrunk blow 0.1 μm. Due to the scaling down of device geometry in deepsubmicron technologies, the crosstalk between...

Abstract—The operationcentric hardware abstraction is useful for describing systems whose behavior exhibits a high degree of concurrency. In the operationcentric style, the behavior of a system is described as a collection of operations on a set of state elements. Each operation is specified as a predicate and a set of simultaneous stateelement updates, which may only take effect in case the predicate is true on the current state values. The effect of an operation’s state updates is atomic, that is, the legal behaviors of the system constitute some sequential interleaving of the operations. This atomic and sequential execution semantics permits...

Jinzhao Wu
Abstract. We argue that some symmetric structure in logic programs should be taken into account when implementing semantics in logic programming. This can enhance the declarative or expressive power of the semantics. The work presented here may be seen as some representative examples along this line. The main focus is on the derivation of negative information and some other classical semantic issues. We first define a permutation group associated with a given logic program and expose the relationships between minimal models as well as completed models of the program and its socalled Greduced form newly derived via this permutation group....

Peter Habermehl; Radu Iosif
Abstract. We introduce a new decidable logic for reasoning about infinite arrays of integers. The logic is in the ∃ ∗ ∀ ∗ firstorder fragment and allows (1) Presburger constraints on existentially quantified variables, (2) difference constraints as well as periodicity constraints on universally quantified indices, and (3) difference constraints on values. In particular, using our logic, one can express constraints on consecutive elements of arrays (e.g. ∀i. 0 ≤ i < n → a[i+1] = a[i]−1) as well as periodic facts (e.g. ∀i. i ≡2 0 → a[i] = 0). The decision procedure follows the automatatheoretic approach: we translate...