Fixed Point vs. First-Order Logic on Finite Ordered Structures with Unary Relations

We prove that first order logic is strictly weaker than fixed point logic over every infinite classes of finite ordered structures with unary relations: Over these classes there is always an inductive unary relation which cannot be defined by a first-order formula, even when every inductive sentence (i.e., closed formula) can be expressed in first-order over this particular class. Our proof first establishes a property valid for every unary relation definable by first-order logic over these classes which is peculiar to classes of ordered structures with unary relations. In a second step we show that this property itself can be expressed in fixed point logic and can be used to construct a non-elementary unary relation.

A Theological Challenge: Coordinating Biological, Social, and Religious Visions of Humanity

This paper attempts two tasks. First, it sketches how the natural sciences (including especially the biological sciences), the social sciences, and the scientific study of religion can be understood to furnish complementary, consonant perspectives on human beings and human groups. This suggests that it is possible to speak of a modern secular interpretation of humanity (MSIH) to which these perspectives contribute (though not without tensions). MSIH is not a comprehensive interpretation of human beings, if only because it adopts a posture of neutrality with regard to the reality of religious objects and the truth of theological claims about them. MSIH is certainly an impressively forceful interpretation, however, and it needs to be reckoned with by any perspective on human life that seeks to insert its truth claims into the arena of public debate. Second, the paper considers two challenges that MSIH poses to specifically theological interpretations of human beings. On the one hand, in spite of its posture of religious neutrality, MSIH is a key element in a class of wider, seemingly antireligious interpretations of humanity, including especially projectionist and illusionist critiques of religion. It is consonance with MSIH that makes these critiques such formidable competitors for traditional theological interpretations of human beings. On the other hand, and taking the religiously neutral posture of MSIH at face value, theological accounts of humanity that seek to coordinate the insights of MSIH with positive religious visions of human life must find ways to overcome or manage such dissonance as arises. The goal of synthesis is defended as important, and strategies for managing these challenges, especially in light of the pluralism of extant philosophical and theological interpretations of human beings, are advocated.

Load Profiling for Efficient Route Selection in Multi-Class Networks

High-speed networks, such as ATM networks, are expected to support diverse Quality of Service (QoS) constraints, including real-time QoS guarantees. Real-time QoS is required by many applications such as those that involve voice and video communication. To support such services, routing algorithms that allow applications to reserve the needed bandwidth over a Virtual Circuit (VC) have been proposed. Commonly, these bandwidth-reservation algorithms assign VCs to routes using the least-loaded concept, and thus result in balancing the load over the set of all candidate routes. In this paper, we show that for such reservation-based protocols|which allow for the exclusive use of a preset fraction of a resource's bandwidth for an extended period of time-load balancing is not desirable as it results in resource fragmentation, which adversely affects the likelihood of accepting new reservations. In particular, we show that load-balancing VC routing algorithms are not appropriate when the main objective of the routing protocol is to increase the probability of finding routes that satisfy incoming VC requests, as opposed to equalizing the bandwidth utilization along the various routes. We present an on-line VC routing scheme that is based on the concept of "load profiling", which allows a distribution of "available" bandwidth across a set of candidate routes to match the characteristics of incoming VC QoS requests. We show the effectiveness of our load-profiling approach when compared to traditional load-balancing and load-packing VC routing schemes.

On Class-based Isolation of UDP, Short-lived and Long-lived TCP Flows

The congestion control mechanisms of TCP make it vulnerable in an environment where flows with different congestion-sensitivity compete for scarce resources. With the increasing amount of unresponsive UDP traffic in today's Internet, new mechanisms are needed to enforce fairness in the core of the network. We propose a scalable Diffserv-like architecture, where flows with different characteristics are classified into separate service queues at the routers. Such class-based isolation provides protection so that flows with different characteristics do not negatively impact one another. In this study, we examine different aspects of UDP and TCP interaction and possible gains from segregating UDP and TCP into different classes. We also investigate the utility of further segregating TCP flows into two classes, which are class of short and class of long flows. Results are obtained analytically for both Tail-drop and Random Early Drop (RED) routers. Class-based isolation have the following salient features: (1) better fairness, (2) improved predictability for all kinds of flows, (3) lower transmission delay for delay-sensitive flows, and (4) better control over Quality of Service (QoS) of a particular traffic type.

Efficient Support for Common Relations in Lightweight Formal Reasoning Systems

In work that involves mathematical rigor, there are numerous benefits to adopting a representation of models and arguments that can be supplied to a formal reasoning or verification system: reusability, automatic evaluation of examples, and verification of consistency and correctness. However, accessibility has not been a priority in the design of formal verification tools that can provide these benefits. In earlier work [Lap09a], we attempt to address this broad problem by proposing several specific design criteria organized around the notion of a natural context: the sphere of awareness a working human user maintains of the relevant constructs, arguments, experiences, and background materials necessary to accomplish the task at hand. This work expands one aspect of the earlier work by considering more extensively an essential capability for any formal reasoning system whose design is oriented around simulating the natural context: native support for a collection of mathematical relations that deal with common constructs in arithmetic and set theory. We provide a formal definition for a context of relations that can be used to both validate and assist formal reasoning activities. We provide a proof that any algorithm that implements this formal structure faithfully will necessary converge. Finally, we consider the efficiency of an implementation of this formal structure that leverages modular implementations of well-known data structures: balanced search trees and transitive closures of hypergraphs.

A Memory Model for Concept Hierarchy Representation and Commonsense Reasoning

Most associative memory models perform one level mapping between predefined sets of input and output patterns1 and are unable to represent hierarchical knowledge. Complex AI systems allow hierarchical representation of concepts, but generally do not have learning capabilities. In this paper, a memory model is proposed which forms concept hierarchy by learning sample relations between concepts. All concepts are represented in a concept layer. Relations between a concept and its defining lower level concepts, are chunked as cognitive codes represented in a coding layer. By updating memory contents in the concept layer through code firing in the coding layer, the system is able to perform an important class of commonsense reasoning, namely recognition and inheritance.