The Objective Conception of Context and Its Logic

In this paper, an objective conception of contexts based loosely upon situation theory is developed and formalized. Unlike subjective conceptions, which take contexts to be something like sets of beliefs, contexts on the objective conception are taken to be complex, structured pieces of the world that (in general) contain individuals, other contexts, and propositions about them. An extended first-order language for this account is developed. The language contains complex terms for propositions, and the standard predicate ist that expresses the relation that holds between a context and a proposition just in case the latter is true in the former. The logic for the objective conception features a global classical predicate calculus, a local logic for reasoning within contexts, and axioms for propositions. The specter of paradox is banished from the logic by allowing ist to be nonbivalent in problematic cases: it is not in general the case, for any context c and proposition p, that either ist(c,p) or ist(c, ¬ p). An important representational capability of the logic is illustrated by proving an appropriately modified version of an illustrative theorem from McCarthy's classic Blocks World example.     

Continuous reductions among combinatorial optimization problems

Summary Many reductions among combinatorial problems are known in the context of NP-completeness. These reductions preserve the optimality of solutions. However, they may change the relative error of approximative solutions dramatically. In this paper, we apply a new type of reductions, called continuous reductions. When one problem is continuously reduced to another, any approximation algorithm for the latter problem can be transformed into an approximation algorithm for the former. Moreover, the performance ratio is preserved up to a constant factor. We relate the problem Minimum Number of Inverters in CMOS-Circuits, which arises in the context of logic synthesis, to several classical combinatorial problems such as Maximum Independent Set and Deletion of a Minimum Number of Vertices (Edges) in Order to Obtain a Bipartite (Partial) Subgraph.     

Sometime = always + recursion ≡ always on the equivalence of the intermittent and invariant assertions methods for proving inevitability properties of programs

Summary We propose and compare two induction principles called always and sometime for proving inevitability properties of programs. They are respective formalizations and generalizations of Floyd invariant assertions and Burstall intermittent assertions methods for proving total correctness of sequential programs whose methodological advantages or disadvantages have been discussed in a number of previous papers. Both principles are formalized in the abstract setting of arbitrary nondeterministic transition systems and illustrated by appropriate examples. The sometime method is interpreted as a recursive application of the always method. Hence always can be considered as a special case of sometime. These proof methods are strongly equivalent in the sense that a proof by one induction principle can be rewritten into a proof by the other one. The first two theorems of the paper show that an invariant for the always method can be translated into an invariant for the sometime method even if every recursive application of the later is required to be of finite length. The third and main theorem of the paper shows how to translate an invariant for the sometime method into an invariant for the always method. It is emphasized that this translation technique follows the idea of transforming recursive programs into iterative ones. Of course, a general translation technique does not imply that the original sometime invariant and the resulting always invariant are equally understandable. This is illustrated by an example.     

Real-time model based geometric reasoning for vision-guided navigation

This paper describes results of a real-time model based geometric reasoning module for autonomous vision-guided road following. Vision-guided road following requires extracting road boundaries from images in real time to guide the navigation of autonomous vehicles on a roadway. The detected road region boundary is error prone due to imperfect image segmentation. To achieve robust system performance, a geometric reasoning module that uses spatial and temporal constraints to perform model based reasoning is used. Local geometric supports for each road edge segment are collected and recorded and a global consistency checking is performed to obtain a consistent interpretation of the raw data. Cases involving incomplete sensor data, curved roads where only one side of the road is visible, and incorrect segmentation due to shadows, road patches, or unusual road conditions, can usually be detected and corrected. The image segmentation results are what the vision system sees. The geometric reasoning results are what the vision system perceives. This reasoning module has been integrated into a road following system which is capable of supporting autonomous robot road following at 24 km/hr.     

Characterization of desirable properties of general database decompositions

The classical theory of acyclicity of universal relational schemata identifies a set of desirable properties of such schemata, and then shows that all of these properties are equivalent to one another, and in turn equivalent to certain acyclicity characterizations of a hypergraph underlying the schema. The desirable properties include the simplicity of constraints, the correctness of certain efficient query evaluation algorithms, and the complexity of maintaining the integrity of a decomposed database. The principal result of this paper is to show that the essence of this result may be extended to a much more general setting; namely, that in which database schemata are just sets and database mappings just functions. Rather than identifying a single desirability class, our work shows that there are several, all of which collapse to a common group when restricted to the universal relational setting. Particularly, the classical notions of pairwise consistency implies global consistency and hypergraph acyclicity are not equivalent in the general case, but rather are independent of each other, and may be considered separately or in combination, to yield varying strengths of desirability.     

Crypt-equivalent algebraic specifications

Summary Equivalence is a fundamental notion for the semantic analysis of algebraic specifications. In this paper the notion of crypt-equivalence is introduced and studied w.r.t. two loose approaches to the semantics of an algebraic specification T: the class of all first-order models of T and the class of all term-generated models of T. Two specifications are called crypt-equivalent if for one specification there exists a predicate logic formula which implicitly defines an expansion (by new functions) of every model of that specification in such a way that the expansion (after forgetting unnecessary functions) is homologous to a model of the other specification, and if vice versa there exists another predicate logic formula with the same properties for the other specification. We speak of first-order crypt-equivalence if this holds for all first-order models, and of inductive crypt-equivalence if this holds for all term-generated models. Characterizations and structural properties of these notions are studied. In particular, it is shown that first order crypt-equivalence is equivalent to the existence of explicit definitions and that in case of positive definability two first-order crypt-equivalent specifications admit the same categories of models and homomorphisms. Similarly, two specifications which are inductively crypt-equivalent via sufficiently complete implicit definitions determine the same associated categories. Moreover, crypt-equivalence is compared with other notions of equivalence for algebraic specifications: in particular, it is shown that first-order cryptequivalence is strictly coarser than abstract semantic equivalence and that inductive crypt-equivalence is strictly finer than inductive simulation equivalence and implementation equivalence.     

Unitary immersions of nonlinear systems

In this paper, we define what we call a unitary immersion of a nonlinear system. We observe that, for classical Hamiltonian systems, this notion contains, in some sense, the concept of quantization. We restrict our attention to degree-zero unitary immersions, where all observation functions must be represented by operators of the type multiplication by a function. We show that the problem of classifying such degree-zero unitary immersions of a given nonlinear system is not obvious. In some cases, we solve this problem.Chargé de Recherche au CNRS.Maître de Conférences.     

Modelling default and likelihood reasoning as probabilistic reasoning

This paper presents a probabilistic analysis of plausible reasoning about defaults and about likelihood. Likely and by default are in fact treated as duals in the same sense as possibility and necessity. To model these four forms probabilistically, a logicQDP and its quantitative counterpartDP are derived that allow qualitative and corresponding quantitative reasoning. Consistency and consequence results for subsets of the logics are given that require at most a quadratic number of satisfiability tests in the underlying prepositional logic. The quantitative logic shows how to track the propagation error inherent in these reasoning forms. The methodology and sound framework of the system highlights their approximate nature, the dualities, and the need for complementary reasoning about relevance.Much of this research was done while at the University of Technology, Sydney, Broadway, NSW, Australia, and some at the Turing Institute, 36 Nth. Hanover Str., Glasgow, Scotland.     

Automated Deduction Techniques for the Management of Personalized Documents

This work is about a real-world application of automated deduction. The application is the management of documents (such as mathematical textbooks) as they occur in a readily available tool. In this Slicing Information Technology tool, documents are decomposed (sliced) into small units. A particular application task is to assemble a new document from such units in a selective way, based on the user's current interest and knowledge. It is argued that this task can be naturally expressed through logic, and that automated deduction technology can be exploited for solving it. More precisely, we rely on first-order clausal logic with some default negation principle, and we propose a model computation theorem prover as a suitable deduction mechanism. Beyond solving the task at hand as such, with this work we contribute to the quest for arguments in favor of automated deduction techniques in the real world. Also, we argue why we think that automated deduction techniques are the best choice here.     

Enhancing the performance of an agent-based manufacturing system through learning and forecasting

Agent-based technology has been identified as an important approach for developing next generation manufacturing systems. One of the key techniques needed for implementing such advanced systems will be learning. This paper first discusses learning issues in agent-based manufacturing systems and reviews related approaches, then describes how to enhance the performance of an agent-based manufacturing system through learning from history (based on distributed case-based learning and reasoning) and learning from the future (through system forecasting simulation). Learning from history is used to enhance coordination capabilities by minimizing communication and processing overheads. Learning from the future is used to adjust promissory schedules through forecasting simulation, by taking into account the shop floor interactions, production and transportation time. Detailed learning and reasoning mechanisms are described and partial experimental results are presented.