
Florence Le Ber; Amedeo Napoli; Jeanluc Metzger
Abstract: In this paper, we present the knowledgebased system rosa working on spatial and functional organizations in agriculture. The reasoning in rosa combines hierarchical classification, casebased reasoning, and qualitative spatial reasoning. The goal of the system is twofold: formalizing and building a case base holding on farm spatial and functional organizations, and helping the analysis of new cases. Domain knowledge and cases are modeled with the help of the socalled spatial organization graphs (sogs), and represented within a description logic system. Hierarchical casebased reasoning, involving classification and qualitative spatial reasoning, is used to compare and explain farm spatial structures modeled...

Michael Fisher; Alexei Lisitsa
In this paper, we pursue the goal of automatic deductive verification for certain classes of ASM. In particular, we base our work on a translation of general ASMs to full firstorder temporal logic. While such a logic is, in general, not finitely axiomatisable, recent work has identified a fragment, termed the monodic fragment, that is finitely axiomatisable and many of its subfragments are decidable. Thus, in this paper, we define a class of monodic ASMs whose semantics in terms of temporal logic fits within the monodic fragment. This, together with recent work on clausal resolution methods for monodic fragments, allows...

Tadeusz Litak
Abstract. This paper introduces an algebraic semantics for hybrid logic with binders H(↓, @). It is known that this formalism is a modal counterpart of the bounded fragment of the firstorder logic, studied by Feferman in the 1960’s. The algebraization process leads to an interesting class of boolean algebras with operators, called substitutionsatisfaction algebras. We provide a representation theorem for these algebras and thus provide an algebraic proof of completeness of hybrid logic.

Balder Ten Cate; Gaëlle Fontaine; Tadeusz Litak
This paper provides several examples of how known results in modal logic can be applied to the XML document navigation language XPath. The applications concern complete axiomatizations and expressive power.

Sofiene Tahar; Paul Curzon
Interactive formal proof and automated verification based on decision graphs are two contrasting formal hardware verification techniques. In this paper, we compare these two approaches. In particular we consider HOL and MDG. The former is an interactive theorem proving system based on higherorder logic, while the latter is an automatic system based on Multiway Decision Graphs. As the basis for our comparison we have used both systems to independently verify a fabricated ATM communications chip: the Fairisle 4 by 4 switch fabric.

Graham Hetherington; Richard Simpson; High Speed

Jianjun Wu; Honggang Liu; Qizhi Chen
Abstract: This paper focuses on a qualitative fault diagnosis method based on the integration and fusion of shallow and deep knowledge for liquidpropellant rocket engines (LRE). The paper firstly clarifies the concept and the types of LRE diagnosis knowledge. Later, from the isomorphic transform point of view, the paper analyses the correlation of different knowledge and knowledge representation, and formulate the LRE fault diagnosis. Then, the ways of acquisition, representation and organization for knowledgebased hybrid models constructed by signed directed graphs, rules, prepositional logic models, and qualitative deviation models are given. The intelligent diagnosis strategies for LRE, which reason and...

Martin Hell; Thomas Johansson
Abstract. The bitsearch generator (BSG) was proposed in 2004 and can be seen as a variant of the shrinking and selfshrinking generators. It has the advantage that it works at rate 1/3 using only one LFSR and some selection logic. We present various attacks on the BSG based on the fact that the output sequence can be uniquely defined by the differential of the input sequence. By knowing only a small part of the output sequence we can reconstruct the key with complexity O(L 3 2 0.5L). This complexity can be significantly reduced in a data/time tradeoff manner to achieve...

Johan Van Benthem
Dov Gabbay is a prolific logician just by himself. But beyond that, he is quite good at making other people investigate the many further things he cares about. As a result, King's College London has become a powerful attractor in our field worldwide. Thus, it is a great pleasure to be an organizer for one of its flagship events: the Augustus de Morgan Workshop of 2005. Benedikt Loewe and I proposed the topic of 'interactive logic ' for this occasion, with an emphasis on social software – the logical analysis and design of social procedures – and on games, arguably...

Yves Moinard; Raymond Roll
Abstract Circumscription uses classical logic in order to modelize rules with exceptions and implicit knowledge. Formula circumscription is known to be easier to use in order to modelize a situation. We describe when two sets of formulas give the same result, when circumscribed. Two kinds of such equivalence are interesting: the ordinary one (two sets give the same circumscription) and the strong one (when completed by any arbitrary set, the two sets give the same circumscription) which corresponds to having the same closure for logical “and ” and “or”. In this paper, we consider only the finite case, focusing on...

Sectio Ai; Waldemar Suszyński A; Wiesława Kuniszykjóźkowiak A
The presented article constitutes a fragment of research which aims at automatic recognition of disfluencies in the speech of stuttering people. In the utterances of such people difficulties frequently appear in words beginning with stop consonants. On the basis of acoustical analyses of the episodes, procedures for their automatic detection have been elaborated. The procedures apply fuzzy logic. 1.

J. J. Sarbo; J. I. Farkas
Abstract We are concerned with the problem of summarizing the contents of a coherent text. In this paper we argue that complex units of symbols like sentences, for example, are signs and the meaning of a text arises via their interaction. We introduce a model for the generation of summaries and illustrate its potential by a realistic example. Keywords: C.S. Peirce, logic, summarization, semiotics, meaning 1

In [ksl Kehne
In [KSL92], Kehne et al. present a protocol (KSL) for key distribution. Their protocol allows for repeated authentication by means of a ticket. They also give a proof in BAN logic [BAN89] that the protocol provides the principals with a reasonable degree of trust in the authentication and key distribution. They present an optimality result that their protocol contains a minimal number of messages. Nonetheless, in [NS93] Neuman and Stubblebine present a protocol (NS) as an explicit alternative to KSL that requires one less message in the initial authentication and key distribution. One goal of this paper is to examine...

O. V. Ramana Murthy; R. K. P. Bhatt; N. Ahmad
The dynamic fuzzy logic system (DFLS) consists of static fuzzy logic system added with a dynamic element—the integrator—with a feedback constant α. It was shown to possess the important universal approximation capability. Further, Lee and Vukovich developed DFLS based stable indirect adaptive control scheme via Lyapunov synthesis approach for a class of nonlinear systems of the form x = f(X) + bu. In this paper, this is extended so that now, it can be applied to a larger class of nonlinear dynamic systems, i.e., of the form x = f(X) + g(X)u. It was successfully investigated on a chaotic systemmodified...

Marek Zaionc
Abstract. This paper presents the number of results concerning problems of asymptotic densities in the variety of propositional logics. We investigate, for propositional formulas, the proportion of tautologies of the given length n against the number of all formulas of length n. We are specially interested in asymptotic behavior of this fraction. We show what the relation between a number of premises of an implicational formula and asymptotic probability of finding a formula with this number of premises is. Furthermore we investigate the distribution of this asymptotic probabilities. Distribution for all formulas is contrasted with

Junping Wang ∗a; Xiaodong Tao A; Deokhwa Hong A; Hyungsuck Cho A
Proportional control based visual controller is the main method used in the visual serving, but small proportional gain results in the slowly response and large proportional gain will result in large overshoot or make the system instable. A PD visual controller for microassembly system is presented to acquire better dynamic response. The fuzzy logic is applied to tuning the controller gains which is a model free method. Thus, the difficulty in obtaining precise and detailed system model is avoided and we can get satisfactory performance which is robust to modeling error and external disturbances. Furthermore, image moments are selected as...

Logic emulation enables designers to functionally verify complex integrated circuits prior to chip fabrication. However, traditional FPGAbased logic emulators have poor interchip communication bandwidth, commonly limiting gate utilization to less than 20 percent. Global routing contention mandates the use of expensive crossbar and PCboard technology in a system of otherwise lowcost, commodity parts. Even with crossbar technology,current emulators only use a fraction of potential communication bandwidth because they dedicate each FPGA pin (physical wire) to a single emulated signal (logical wire). Virtual Wires overcome pin limitations by intelligently multiplexing each physical wire among multiple logical wires and pipelining these connections...

Leendert W.N. van der Torre; YaoHua Tan
The deontic logic dus is a deontic update semantics for prescriptive obligations based on the update semantics of Veltman. In dus the definition of logical validity of obligations is not based on static truth values but on dynamic action transitions. In this paper prescriptive prima facie obligations are formalized in update semantics. The logic formalizes the specificity principle, has reinstatement and does not have an irrelevance problem. Moreover, it handles the diagnostic problem by distinguishing

Tomoyuki Yamada
Abstract. If we are to take the notion of speech act seriously, we must be able to treat speech acts as acts. In this paper, we will try to model changes brought about by various acts of commanding in terms of a variant of update logic. We will combine a multiagent variant of the language of monadic deontic logic with a dynamic language to talk about the situations before and after the issuance of commands, and the commands that link those situations. Although the resulting logic inherits various inadequacies from monadic deontic logic, some interesting principles are captured and seen...

Hahnsang Kim; Thierry Turletti; Amar Bouali
The software approach to developing Digital Signal Processing (DSP) applications brings some great features such as flexibility, reusability of resources and easy upgrading of applications. However, it requires long and tedious tests and verification phases because of the increasing complexity of the software. This implies the need of a software programming environment capable of putting together DSP modules and providing facilities to debug, verify and validate the code. The objective of the work is to provide such facilities as simulation and verification for developing DSP software applications. This led us to develop an extension toolkit, EPspectra, built upon Pspectra, one...