
Cesar Analide; Paulo Novais; José Machado; José Neves
Abstract. Traditional programming languages do not support the description of certain behaviours which usually involve computational agents. In this work, it is presented an alternative way to evaluate the qualitative knowledge of virtual entities, such as computational agents, living in virtual worlds and that are able to represent legal organizations or personalities. In this sense, it is possible to determine the attitudes revealed by the interaction, in community, of such virtual entities, pursuing social or human goals. The agent’s knowledge bodies are described in terms of an extension to a logic programming language, allowing the representation of imperfect knowledge. 1

Dale Miller
Abstract. Higherorder hereditary Harrop formulas, the underlying logical foundation of Prolog [NM88], are more expressive than rstorder Horn clauses, the logical foundation of Prolog. In particular, various forms of scoping and abstraction are supported by the logic of higherorder hereditary Harrop formulas while they are not supported by rstorder Horn clauses. Various papers have argued that the scoping and abstraction available in this richer logic can be used to provide for modular programming [Mil89b], abstract data types [Mil89a], and state encapsulation [HM90]. None of these papers, however, have dealt with the problems of programminginthelarge, that is, the essentially linguistic problems...

Abstract. We establish a connection between the geometric methods developed in the combinatorial theory of small cancellation and the propositional resolution calculus. We define a precise correspondence between resolution proofs in logic and diagrams in small cancellation theory, and as a consequence, we derive that a resolution proof is a 2dimensional process. The isoperimetric function defined on diagrams corresponds to the length of resolution proofs.

Maria A. Gil B; Henk A. L. Kiers C
For the last decades, research studies have been developed in which a coalition of Fuzzy Sets Theory and Statistics has been established with different purposes. These namely are: (i) to introduce new data analysis problems in which the objective involves either fuzzy relationships or fuzzy terms; (ii) to establish wellformalized models for elements combining randomness and fuzziness; (iii) to develop uni and multivariate statistical methodologies to handle fuzzyvalued data; and (iv) to incorporate fuzzy sets to help in solving traditional statistical problems with nonfuzzy data. In spite of a growing literature concerning the development and application of fuzzy techniques in...

Radosław Piotr Katarzyniak
Abstract: An original approach to modelling internal structure of artificial cognitive agents and the phenomenon of language grounding is presented. The accepted model for the internal cognitive space reflects basic structural properties of human cognition and assumes the partition of cognitive phenomena into conscious and 'nonconscious'. The language is treated as a set of semiotic symbols and is used in semantic communication. Semiotic symbols are related to the internal content of empirical knowledge bases in which they are grounded. This relation is given by the socalled epistemic satisfaction relations defining situations in which semiotic symbols are adequate (grounded) representations of...

Klaus Glashoff; Kleiner Kielort
ABSTRACT: In 1679, Leibniz wrote nine manuscripts on three different arithmetical models of Aristotelian logic. This was a part of his project of a “calculus universalis”. First we show the precise relations of these three models to each other by presenting three criteria which serve the purpose of classifiying models of Aristotelian logic. This facilitates the understanding of Leibniz ’ constructions. Our method is of special value for the sophisticated third model, the domain of which consists of pairs of natural numbers. We present a simple approach to Leibniz ’ definitions which on first sight appear complicated. We show that...

The aim of this paper is to describe a simple extension of semantic nets. In this formulation we have labelled nodes with directed arcs, but the directed arcs can lead to other arcs as well as nodes. In this model contexts are not differentiated as special objects, but rather that some nodes to a greater or lesser extent have roles as encoders of contextual information. This formulation is shown to be expressive enough to capture several aspects of context, namely: contextdependent inference, context specific learning, the selection of a relevant context and the generalisation of knowledge. Its strengths are its...

David S. Kung
In this paper, we discuss timing closure for high performance microprocessor designs. Aggressive cycle time and deep submicron technology scaling introduce a myriad of problems that are not present in the ASIC domain. The impact of these problems on floorplanning, placement, clocking and logic synthesis is described. We present ideas and potential solutions for tackling these problems.

Robert Demolombe; Pilar Pozos Parra
Abstract. Deontic logic is appropriate to model a wide variety of legal arguments, however this logic suffers form certain paradoxes of which the socalled Chisholm is one of the most notorious. We propose a formalisation of the Chisholm set in the framework of the situation calculus. We utilise this alternative to modal logic for formalising the obligations of the agent and avoiding the Chisholm paradox. This new approach makes use of the notion of obligation fluents together with their associated successor state axioms. Furthermore, some results about automated reasoning in the situation calculus can be applied in order to consider...

Alan Rector; Jeremy Rogers
GALEN seeks to provide reusable terminology resources for clinical systems. The heart of GALEN is the Common Reference Model (CRM) formulated in a specialised description logic. The CRM is based on a set of principles that have evolved over the period of the project and illustrate key issues to be addressed by any large medical ontology. The principles on which the CRM is based are discussed followed by a more detailed look at the actual mechanisms employed. Finally the structure is compared with other biomedical ontologies in use or proposed.

David Gray; Geoff Hamilton; David Sinclair; Paul Gibson; James Power
The Internet Protocol (IP) is the protocol used to provide connectionless communication between hosts connected to the Internet. It provides a basic internetworking service to transport protocols such as Transmission Control Protocol (TCP) and User Datagram Protocol (UDP). These in turn provide both connectionoriented and connectionless services to applications such as file transfer (FTP) and WWW browsing. In this paper we present four separate specifications of the interface to the internetworking layer implemented by IP using four types of logic: classical, constructive, temporal and linear logic. 1

Makoto Kanazawa
I present a new syntactical method for proving the Interpolation Theorem for the implicational fragment of intuitionistic logic and its substructural subsystems. This method, like Prawitz’s, works on natural deductions rather than sequent derivations, and, unlike existing methods, always finds a ‘strongest ’ interpolant under a certain restricted but reasonable notion of what counts as an ‘interpolant’.

An expressive firstorder temporal logic using the method of temporal arguments is developed and provided with a nonstandard semantics that explicates its underlying temporal structure. Objections from the AI literature against the adequacy of temporal argument theories are answered in the course of discussing representational issues for the developed logic. This logic "accords a special status to time,' ' distinguishes the temporal features of event occurrences from ordinary facts, and supports changing ontologies. We conclude that the method of temporal arguments remains a viable candidate for temporal reasoning in Al. I

Alexander Saldanha; Heather Harkness; Patrick C. Mcgeer; Robert K. Brayton; Alberto L. Sangiovannivincentelli
A common approach to performance optimization of circuits focuses on resynthesis to reduce the length of all paths greater than the desired delay. We describe a new delay optimization procedure that optimizes only sensitizable paths greater than. Unlike previous methods that use topological analysis only, this method accounts for both functional and topological interactions in the circuit. Comprehensive experimental results comparing the proposed technique to a stateoftheart performance optimization procedure are presented for combinational and sequential logic circuits. 1

Wolfgang Faber; Tu Wien; Nicola Leone; Gerald Pfeifer
Disjunctive Logic Programming (DLP) is a very expressive formalism: it allows to express every property of finite structures that is decidable in the complexity class E ^ (NP NH). Despite the high expressiveness of DLP, there are some simple properties, often arising in realworld applications, which cannot be encoded in a simple and natural manner. Among these, properties requiring to apply some arithmetic operators (like sum, times, count) on a set of elements satisfying some conditions, cannot be naturally expressed in DLP. To overcome this deficiency, in this paper we extend DLP by aggregate functions. We formally define the semantics...

Departamento De Lenguajes Y; Ciencias De; La Computación; Universidad De; M Álaga; Informe T Écnico; Sonia Estévezmartín; Antonio J. Fernández; F. Sáenzpérez; S. Estévezmartín A; A. J. Fernández B; F. Sáenzpérez A
This paper describes implementation issues of the constraint functional logic system T OY, which has recently incorporated new features such as solver cooperation. The formal framework introduced in [14] is the basis for this implementation, allowing the cooperation of three constraint solvers over different domains: the Herbrand domain, the finite domain, and the real numbers domain. The system offers both binding and propagation as mechanisms for the cooperation. The paper describes the implementation of the system and, in particular, regarding solver cooperation, presents a new function that serves as a bridge among the solvers involved in the cooperation. The new...

Paul Gibson (nui Maynooth
The feature interaction problem is prominent in telephone service development. Through a number of case studies, we have discovered that no single semantic framework is suitable for the synthesis and analysis of formal feature requirements models, and the choice of modelling language has certain knockon effects on the transformational design steps which lead to implementation. We initially describe a mixed semantic model approach whilst acknowledging that integration is a major concern. Our method incorporates operational state transition models, temporal logic formulae and object oriented structuring mechanisms. Each of these approaches gives rise to certain advantages and disadvantages, and we propose...

Omar Ochoa; Irbis Gallegos; Steve Roach; Ann Gates
In this paper, we describe an Aspect Oriented extension to the verification tool Java Monitoring and Checking (JavaMaC) [1]. This approach generates AspectJ aspects from JavaMaC specifications. We then use these aspects to monitor the program during execution [2]. To demonstrate the described approach, we apply it to a “benchmark ” from formal methods research [3], a safetycritical railroad crossing system composed of a train, a gate and a controller. In this system, the gate must be down while the train is crossing and up when no train is crossing. The JavaMaC framework allows users to specify system states to...

Nuno Roma; Tiago Dias; Leonel Sousa
Abstract. This paper proposes new corebased architectures for motion estimation that are customisable for different coding parameters and hardware resources. These new cores are derived from an efficient and fully parameterisable 2D single array systolic structure for fullsearch blockmatching motion estimation and inherit its configurability properties in what concerns the macroblock dimension, the search area and parallelism level. The proposed architectures require significantly fewer hardware resources, by reducing the spatial and pixel resolutions rather than restricting the set of considered candidate motion vectors. Lowcost and lowpower regular architectures suitable for field programmable logic implementation are obtained without compromising the quality...

Universidade De Lisboa; Faculdade De; Ci Ências; Manuel A. Martins; Doutoramento Em; Matem Ática; Faculdade De; Ci Ências; Manuel A. Martins; Doutoramento Em; Matem Ática; Lógica E Fundamentos
to my Family