
In this paper, we present a new coordination model and a small set of programming notations for distributed programming that can be integrated in very different programming languages (imperative, declarative or object oriented). Both together, allow the development of distributed programs in a compositional way, by assembling different independent pieces of (possibly preexisting and heterogeneous) code. This approach is in the spirit of many other similar proposals as Linda, PCN, CC++, etc., but it allows multiparadigm and multilingual integration and provides a powerful set of concurrent programming techniques, inherited from Concurrent Logic Languages (CLLs), that can be efficiently implemented in...

The Proceedings of the Society for Medieval Logic and Metaphysics (P.S.M.L.M.) is the publication of the Society for Medieval Logic and Metaphysics, collecting original materials presented at sessions sponsored by the Society. Publication in the Proceedings constitutes prepublication, leaving the authors ’ right to publish (a possibly modified version of) their materials elsewhere unaffected. The Society for Medieval Logic and Metaphysics (S.M.L.M.) is a network of scholars founded with the aim of fostering collaboration and research based on the recognition that � recovering the profound metaphysical insights of medieval thinkers for our own philosophical thought is highly desirable, and, despite...

Abstract — We study and implement concrete methods for the verification of both imperative as well as functional programs in the frame of the Theorema system. The distinctive features of our approach consist in the automatic generation of loop invariants (by using combinatorial and algebraic techniques), and the generation of verification conditions as first–order logical formulae which do not refer to a specific model of computation. I.

Luca Cardelli; Giorgio Ghelli
Abstract. The ambient logic is a modal logic proposed to describe the structural and computational properties of distributed and mobile computation. The structural part of the ambient logic is, essentially, a logic of labeled trees, hence it turns out to be a good foundation for query languages for semistructured data, much in the same way as rstorder logic is a tting foundation for relational query languages. We de ne here a query language for semistructured data that is based on the ambient logic, and we outline an execution model for this language. The language turns out to be quite expressive....

C. Joseph Vanderwaart; Robert Haper; Peter Lee
Explicit or implicit, enforced or not, safety policies are ubiquitous in software systems. In the many settings where thirdparty software is executed in the context of a larger client program, the supervisor usually enforces a safety policy that prevents the foreign code from behaving in ways that would disrupt the client, corrupt data or destabilize the system. Certified code provides a static means for controlling the behavior of untrusted programs or components by bringing the power of type systems and formal logic to bear on the problem. Code certification systems that prevent bad memory accesses and enforce the abstractions provided...

Mark Colyvan
In this paper I discuss an argument that purports to prove that probability theory is the only sensible means of dealing with uncertainty. I show that this argument can succeed only if some rather controversial assumptions about the nature of uncertainty are accepted. I discuss these assumptions and provide reasons for rejecting them. I also present examples of what I take to be nonprobabilistic uncertainty. Key Words: Cox’s Theorem, NonClassical Logic, Probability, Uncertainty, Vagueness Uncertainties are ubiquitous in risk analysis and on the face of it, we must contend with a number of quite distinct sorts of uncertainty. There are,...

James J. Lu; Neil V. Murray; Erik Rosenthal
The inference rule!resolution was introduced in [27] as a technique for developing an SLDstyle query answering procedure for the logic programming subset of annotated logic. The inference rule requires that the lattice of truth values be ordinary. In this paper, it is proved that all complete distributive lattices are ordinary. Properties of!resolution in the general theorem proving setting are explored, including the completeness of a variety of restrictions. It is shown that the pruning effects of classical restriction strategies (for example, ordering and the linear restriction) can be enhanced with the!operator. Two macro inference rules, annotated hyperresolution and annotated hypertableaux,...

V. Kheterpal; V. Rovner; T. G. Hersan; D. Motiani; Y. Takegawa; A. J. Strojwas; L. Pileggi
Implementing logic blocks in an integrated circuit in terms of repeating or regular geometry patterns [6,7] can provide significant advantages in terms of manufacturability and design cost [2]. Various forms of gate and logic arrays have been recently proposed that can offer such pattern regularity to reduce design risk and costs [2,4,9,11,12]. In this paper, we propose a fullmaskset design methodology which provides the same physical design coherence as a configurable array, but with area and other design benefits comparable to standard cell ASICs. This methodology is based on a set of simple logic primitives that are mapped to a...

Zhongzhi Shi; Wenpin Jiao; Qiujian Sheng
Abstract: In this paper, a methodology for agentoriented software analysis and design is proposed, which starts from a system’s organizational structure and its work mode. The main tasks of analysis are to build the models for a system’s organization structure and its work mode.to capture how roles construct the system, which problems the system is desired to solve, and which relationships are among those problems. The main tasks of design are to model agents who will play the roles and to model interactions to show how agents realize the existing work mode and solve problems. To ensure the consistency between...

Andreas Podelski; Andrey Rybalchenko
Abstract. Software model checking with abstraction refinement is emerging as a practical approach to verify industrial software systems. Its distinguishing characteristics lie in the way it applies logical reasoning to deal with abstraction. It is therefore natural to investigate whether and how the use of a constraintbased programming language may lead to an elegant and concise implementation of a practical tool. In this paper we describe the outcome of our investigation. Using a Prolog system together with Constraint Logic Programming extensions as the implementation platform of our choice we have built such a tool, called ARMC (for Abstraction Refinement Model...

Franz Baader; Jan Hladik; Rafael Peñaloza
Abstract. In Description Logics (DLs), both tableaubased and automatabased algorithms are frequently used to show decidability and complexity results for basic inference problems such as satisfiability of concepts. Whereas tableaubased algorithms usually yield worstcase optimal algorithms in the case of PSpacecomplete logics, it is often very hard to design optimal tableaubased algorithms for ExpTimecomplete DLs. In contrast, the automatabased approach is usually wellsuited to prove ExpTime upperbounds, but its direct application will usually also yield an ExpTimealgorithm for a PSpacecomplete logic since the (tree) automaton constructed for a given concept is usually exponentially large. In the present paper, we formulate...

Visvesh S. Sathe; Conrad H. Ziesler; Marios C. Papaefthymiou
In this paper, we propose Boost Logic, a logic family which relies on voltage scaling, gate overdrive and energy recovery techniques to achieve high energy efficiency at frequencies in the GHz range. The key feature of our design is the use of an energy recovering “boost ” stage to provide an efficient gate overdrive to a highly voltage scaled logic at near threshold supply voltage. We have evaluated our logic family using postlayout simulation of an 8bit pipelined array multiplier in a ¢¤£¦¥¨§� © m CMOS process with ���� � =340mV. At 1.6GHz and a 1.3V supply voltage, the Boost...

Simona Colucci; Tommaso Di Noia; Eugenio Di Sciascio; Francesco M. Donini; Azzurra Ragone
Abstract: A logicbased approach to the semanticbased composition of task oriented teams using candidates profiles and task description is presented, in the framework of a skill management system. The selection process exploits Concept Covering, carried out using nonstandard inference services in Description Logics. The approach is motivated andcomparedwithothersemanticorientedproposals.

Dan Moldovan; Marius Pas Ca; Sanda Harabagiu; Mihai Surdeanu
Language Computer Corporation This paper presents an indepth analysis of a stateoftheart Question Answering system. Several scenarios are examined: (1) the performance of each module in a serial baseline system, (2) the impact of feedbacks and the insertion of a logic prover, and (3) the impact of various retrieval strategies and lexical resources. The main conclusion is that the overall performance depends on the depth of natural language processing resources and the tools used for answer finding. Categories and Subject Descriptors: H.5.2 [Information Interfaces and Presentation]: User

Harald Zankl; Aart Middeldorp
Abstract This note presents an approach to prove termination of term rewrite systems (TRSs) with the KnuthBendix order efficiently. The constraints for the weight function as well as for the precedence are encoded in propositional logic and the resulting formula is tested for satisfiability. Any satisfying assignment represents a weight function and a precedence such the induced KnuthBendix order orients the rules of the encoded TRS from left to right. 1.1

Ananta K. Majhi; James Jacob; Lalit M. Patnaik; Vishwani D. Agrawal
We propose a coverage metric and a twopass test generation method for path delay faults in combinational logic circuits. The coverage is measured for each line with a rising and a falling transition. However, the test criterion is diflerent from that of the slowtorise and slowtofall transition faults. The test, called “line delay test”, is a path delay test for the longest sensitizable path producing a given transition on the target line. The maximum number of tests (and faults) is limited to twice the number of lines. However, the line delay test criterion resembles path delay test and not the...

Zuzana Haniková
Contents i Acknowledgments iv

Future manycore architectures are likely to have heterogeneous computing resources which will include conventional CPUs as well as variants of today’s GPUs and reconfigurable logic like FPGAs. Many of the techniques that the reconfigurable computing community has championed will find new applications in mainstream applications. One challenge posed by such manycore architectures is the requirement to target multiple parallel computing resources from a single description (or code). This paper proposes a design methodology for the specification and implementation of data parallel computations that can be mapped to either circuits on FPGAs or pixelshader code on GPUs from exactly the same...

Thomas Lukasiewicz; Jörg Schellhase; Fachgebiet Wirtschaftsinformatik; Universität Kassel
Abstract. In previous work, we have introduced variablestrength conditional preferences for ranking objects in ontologies. In this paper, we continue this line of research. We propose a new ranking of objects, which integrates this userdefined preference ranking of objects with Google’s importance ranking (called PageRank) based on the link structure between the objects. We also propose to use probabilistic description logics based on Bayesian networks and the description logic DLLite to compute the ranking of incompletely specified objects. 1

Abbas K. Zaidi; Er H. Levis
Abstract—This paper is an extension of an earlier work on a methodology for modeling temporal aspects of discreteevent systems. The methodology incorporates point and interval descriptions of time, and offers both qualitative and quantitative calculus for time. A graphbased temporal programmer (TEMPER) is shown to implement the axiomatic system of the temporal formalism. The approach transforms the system specifications given by temporal statements into a graph structure, identifies errors (if present) in the system, infers new temporal relations among system intervals, and calculates delays among time points and their actual time of occurrence. Index Terms—Discrete event systems, Petri nets, point...