Catálogo de publicaciones - libros

At the time Alan Turing was engaged in deciphering the code of the Enigma in Bletchley Park and Konrad Zuse applied his patent for the first electronic computer called “Rechenvorrichtung” in Berlin, Jörg was born into the rural capital of the smallest Fürstentum of Germany, called Schaumburg-Lippe, a name even well educated Germans have probably never heard of. Jörg grew up as the oldest son of a family whose male providers had been joiners and curlers for centuries. There has never been a question that one day he would inherit the small family owned curler and joiners workshop.

But things turned out otherwise: Schaumburg-Lippe never became an independent Land again and the once respectable Siekmann family of joiners, curlers and church leaders was on the decline: mass furniture production became a highly capital intensive, fully automated business, where a certain Swedish company set the pace. In that process, almost all of the family-owned small and medium sized woodworking companies vanished and the once proud Schaumburg Lippesche Handwerkskammer dating back far into medieval times became obsolete.

But Jörg did not quite fit particularly well anyway: when he could not decide whether he wanted to be an artist or a scientist – an idea so inconceivable that his father threatened to cut off all his family ties – he took his juvenile poems and drawings to a family friend who looked at his paintings and poems with a stern expression and suggested: “Son, you better learn the trade of your fathers!”

Some general reflections on proof transformations lead to the abstract concept of a quintessential proof of a theorem. A quintessential proof embodies the essential features of many intertranslatable proofs of the theorem. While reasonable candidates for quintessential proofs for normal proofs have been developed, more work is needed with regard to non-normal proofs. Work on proof transformations seems likely to lead to important progress in understanding proofs.

The lack of automated support is probably the main obstacle to the application of formal method techniques in the industrial setting. A possible solution to this problem is to combine the expressiveness of general purpose reasoners (such as theorem provers) with the efficiency of specialized ones (such as decision procedures). This is witnessed by the fact that many theorem provers developed for verification purposes (such as Acl2 [11], PVS [17], Simplify [9], STeP [14], and Tecton [10]) have integrated procedures for ubiquitous theories such as the theory of equality, decidable fragments of arithmetics, lists, and arrays. Unfortunately, designing an effective integration is far from being a trivial task and the solutions available in the verification systems listed above are not completely satisfactory for two main reasons. First, the schemes designed to incorporate decision procedure in larger systems are not flexible enough to allow developers to easily incorporate new procedures. Second, only a tiny portion of the proof obligations arising in many practical applications falls exactly into the domain the specialized reasoners are designed to solve. Thus, in many cases, available decision procedures are of little help if they are not combined with mechanisms for widening their scope.

Propositional reasoning (SAT) is an essential part of many reasoning tasks. Many problems in computer science can be compiled to SAT and then effectively decided using state-of-the-art solvers. Alternatively, if reduction to SAT is not feasible, the ideas and technology of state-of-the-art SAT solvers can be useful in deciding the propositional component of the reasoning task being considered. This last approach has been used in different contexts by different authors, many times by authors of this paper. Because of the essential role played by the SAT solver, these decision procedures have been called “SAT-based”. SAT-based decision procedures have been proposed for various logics, but also in other areas such as planning. In this paper we present a unifying perspective on the various SAT-based approaches to these different reasoning tasks.

This is the first of a new series of papers on the temporal dynamics of Support and Attack networks. These are graphs with a basic situation described in Figure 5 below. We have nodes ,..., connected by arrows to a node . The nodes have some values attached to them and these values are transmitted by the arrows, and revise the value at . This series of papers studies the temporal dynamics of such networks. The topic, in this generality, has emerged from our previous research into argumentation frameworks (Gabbay and Woods [14,13,10,12] and Woods [21]). Our starting point is therefore a generalisation of abstract argumentation networks.

Probabilistic conditionals are a powerful means of representing commonsense and expert knowledge. By viewing probabilistic conditionals as an institution, we obtain a formalization of probabilistic conditionals as a logical system. Using the framework of institutions, we phrase a general representation problem that is closely related to the selection of preferred models. The problem of discovering probabilistic conditionals from data can be seen as an instance of the inverse representation problem, thereby considering knowledge discovery as an operation inverse to inductive knowledge representation. These concepts are illustrated using the well-known probabilistic principle of maximum entropy for which we sketch an approach to solve the inverse representation problem.

Today it is commonplace to talk about the revolution going on in our society, driven by information technology. Through talking about the ongoing changes people seem to compensate their uneasiness with the restlessness in this world. Few of those heralding the future developments are actually looking further ahead than perhaps five or ten years. And even fewer still are pondering about the consequences the coming technological changes will have for society and prepare for actions to be planned for coping with these changes.

First-order constraints over arbitrary theories or structures can be formalised as the formula instantiation problem as defined in [11]. Several re- sults have been previously obtained for the formula instantiation problem in the case of quantifier-free formulas of first-order logic. In this paper we prove the first general result on formula instantiation for quantified formulas, namely that formula instantiation is decidable for the monadic class without equality.

Around 1990 the work on the first-order theorem prover MKRP stopped after a development going on for more than a decade. Instead a new system has been developed since then, the mathematical assistant Ω. In this contribution I try to summarise some of the discussions and decisions that led to this shift in focus and to the development of the Ω system, and I attempt in retrospect to give a tentative evaluation of some of the decisions.

Though higher-order unification is in general undecidable, there are expressive and decidable variants. Several interesting special cases and variants stem from restricting algorithms to search only unifiers where the number of bound variables is restricted. The intention of this paper is to summarize results in this area and to shed some light on the connections between context unification, decidable variants of higher-order, second order unification and string unification. Since this paper is intended to appear in a volume in celebrating Jörg Siekmann’s 60th birthday, we will take the opportunity to give hints on how the motivating power of Jörg Siekmann has contributed to and put forward the research in unification.