We consider the parameterized problems of whether a given set of clauses can be refuted within k resolution steps, and whether a given set of clauses contains an unsatisfiable subset of size at most k. We show that both problems are complete for the class W[1], the first level of the W-hierarchy of fixed-parameter intractable problems. Our results remain true if restricted to 3-SAT instances and/or to various restricted versions of resolution including tree-like resolution, input resolution, and read-once resolution. Applying a metatheorem of Frick and Grohe, we show that, restricted to classes of sets of clauses of locally bounded treewidth, the considered problems are fixed-parameter tractable. For example, the problems are fixed-parameter tractable for planar CNF formulas.

The model presented in this paper provides a formalisation of the concept of money and the mechanics of its circulation in an economy. Any instance of money is modelled as a Money Token. The mechanics of the creation, transfer and redemption of money are modelled using a limited set of four defined Basic Transactions. In this model, money is any contract, which can be represented by a Money Token. This is shown to include, but is not limited to, various types of securities, fiat money, cash, and commodities. The definition of a Money Token builds upon Roy Radner’s (1972) formalisation of securities contracts. The concept of the defined set of Basic Transactions originates in computer based electronic money technology. In both origin and applications the model provides a bridge between theoretical models of economies, the applied economics areas of monetary economics, finance, and banking and computer based systems for storage and circulation of financial instruments. It has been developed as a tool for research or practical implementation. This paper discusses the model, developed as part of a PhD thesis (Furche, 2001), in the context of ongoing research work.

Stored value systems are the most recent form of electronic payment technology. They are meant to coexist with credit and debit technology, by primarily targeting the low value area of the transaction market. Being targeted at low value transactions, they are designed to have very low transaction cost. Stored value systems rely on creating a form of electronic value, on smart cards or as computer files. Such value can be bought (withdrawn) at any one time, and spent in arbitrary fractions at later times. When the technology emerged for its first implementations in the first half of the 1990s, it was much celebrated as a replacement for cash with many benefits over existing payment technologies. Many of these systems have subsequently been set up as trials, and the commercial rollout of some systems has started. However, actual usage of stored value systems is still low, much lower than was expected by the operators of the systems. Several years after the first trials were implemented, it is still unclear whether and when they will play a relevant role in the payments system market. And none of the trials that have been run can be considered a commercial success. This makes it necessary not only to assess the technology, but also the commercial future and user uptake of these systems.

The Internet in a role as ideal infrastructure for a global consumer marketplace has now been discussed for some time. However, actual trading figures on the Internet are today significantly lower than what had been projected three years ago. The main obstacle had already been identified at the time, it was the lack of an efficient payment mechanism on the Internet. Today, we are still facing the same problem. While the technology to make secure payments on an insecure communication infrastructure is available, its implementation on the Internet is taking longer than expected. In this paper, we first discuss the technology for electronic payment systems on the Internet. We then evaluate their current market position, with particular emphasis on the South East Asian region.

The usability of a statistical database is defined to be the ratio of the cardinality of the largest set of queries which can be answered without compromise to the total number of queries. In this paper, we present new results concerning the usability of secure statistical databases for general SUM, COUNT and MEAN queries, as well as for the corresponding range queries. We give the usability of these k-dimensional databases for all k/spl ges/1. The paper concludes with a discussion of the implications of our results.

SubScrip is a protocol that allows the establishment of pay-per-view services on the Internet where every single access has only a very low value. It can eeectively bundle payments to use any existing or proposed In-ternet billing mechanism as a basis, solving the problem of transaction costs being too high to economically support small payments in pay-per-view schemes. The SubScrip protocol is a prepaid anonymous system with no need for user identiication, and in its simple form does not require expensive encryption computations. SubScrip is diierent from other payment mechanisms proposed in that it does not require the setting up of a complete banking and billing hierarchy, but can be implemented based on, and without any modi-cations to, any combination of all currently existing or proposed Internet payment mechanisms.

This article provides an overview of automated reasoning and of the various fields for which it is relevant. It takes the form of a collection of articles, each covering some field and each written by an expert in that field. A field is introduced, its elements reviewed, the current state of the art given, the basic problems discussed, and the various goals listed. Although individually the goals of each field present a wide spectrum, collectively the fields share the interest of automating the process known as reasoning.