This article is concerned with automated complexity analysis of term rewrite systems. Since these systems underlie much of declarative programming, time complexity of functions defined by rewrite systems is of particular interest. Among other results, we present a variant of the dependency pair method for analysing runtime complexities of term rewrite systems automatically. The established results significantly extent previously known techniques: we give examples of rewrite systems subject to our methods that could previously not been analysed automatically. Furthermore, the techniques have been implemented in the Tyrolean Complexity Tool. We provide ample numerical data for assessing the viability of the method.

Without these assumptions the sequences of operations that achieve the goals depend on the initial state and the outcomes of nondeterministic changes in the system. This setting raises the questions of how to represent the plans and how to perform plan search. The answers are quite dierent from those in the simpler classical framework. In this paper, we approach conditional planning from a new viewpoint that is motivated by the use of satisability algorithms in classical planning. Translating conditional planning to formulae in the propositional logic is not feasible because of inherent computational limitations. Instead, we translate conditional planning to quantied Boolean formulae. We discuss three formalizations of conditional planning as quantied Boolean formulae, and present experimental results obtained with a theorem-prover. Plans consist of operators that make a set of facts true whenever their preconditions are fullled. The most basic { and the most common in earlier research { form of plans is sequence of operators that are executed unconditionally in the specied order. Plans of this form are sucient only if the world where a plan is carried out is completely predictable and known, and the execution of the plan always starts in the same state. When not all changes in the world can be predicted or not all facts aecting plan execution are known in advance, the structure of plans has to be more general. If the task is to move object A, that is in room 1 or in room 2, to a trash can, the operations that achieve the goal depend on the initial location of A. There is no single sequence of operations that achieves the goal in both cases.

It is common to view programs as a combination of logic and control: the logic part defines what the program must do, the control part -- how to do it. The Logic Programming paradigm was developed with the intention of separating the logic from the control. Recently, extensive research has been conducted on automatic generation of control for logic programs. Only a few of these works considered the issue of automatic generation of control for improving the efficiency of logic programs. In this paper we present a novel algorithm for automatic finding of lowest-cost subgoal orderings. The algorithm works using the divide-and-conquer strategy. The given set of subgoals is partitioned into smaller sets, based on co-occurrence of free variables. The subsets are ordered recursively and merged, yielding a provably optimal order. We experimentally demonstrate the utility of the algorithm by testing it in several domains, and discuss the possibilities of its cooperation with other existing methods.

We study the problem of probabilistic deduction with conditional constraints over basic events. We show that globally complete probabilistic deduction with conditional constraints over basic events is NP-hard. We then concentrate on the special case of probabilistic deduction in conditional constraint trees. We elaborate very efficient techniques for globally complete probabilistic deduction. In detail, for conditional constraint trees with point probabilities, we present a local approach to globally complete probabilistic deduction, which runs in linear time in the size of the conditional constraint trees. For conditional constraint trees with interval probabilities, we show that globally complete probabilistic deduction can be done in a global approach by solving nonlinear programs. We show how these nonlinear programs can be transformed into equivalent linear programs, which are solvable in polynomial time in the size of the conditional constraint trees.

In default reasoning, usually not all possible ways of resolving conflicts between default rules are acceptable. Criteria expressing acceptable ways of resolving the conflicts may be hardwired in the inference mechanism, for example specificity in inheritance reasoning can be handled this way, or they may be given abstractly as an ordering on the default rules. In this article we investigate formalizations of the latter approach in Reiter's default logic. Our goal is to analyze and compare the computational properties of three such formalizations in terms of their computational complexity: the prioritized default logics of Baader and Hollunder, and Brewka, and a prioritized default logic that is based on lexicographic comparison. The analysis locates the propositional variants of these logics on the second and third levels of the polynomial hierarchy, and identifies the boundary between tractable and intractable inference for restricted classes of prioritized default theories.

A class of interval-based temporal languages for uniformly representing and reasoning about actions and plans is presented. Actions are represented by describing what is true while the action itself is occurring, and plans are constructed by temporally relating actions and world states. The temporal languages are members of the family of Description Logics, which are characterized by high expressivity combined with good computational properties. The subsumption problem for a class of temporal Description Logics is investigated and sound and complete decision procedures are given. The basic language TL-F is considered first: it is the composition of a temporal logic TL -- able to express interval temporal networks -- together with the non-temporal logic F -- a Feature Description Logic. It is proven that subsumption in this language is an NP-complete problem. Then it is shown how to reason with the more expressive languages TLU-FU and TL-ALCF. The former adds disjunction both at the temporal and non-temporal sides of the language, the latter extends the non-temporal side with set-valued features (i.e., roles) and a propositionally complete language.

Bottom-up pro v ers prot from strong redundan y on trol but suer from the la k of goal-orien tation, whereas top-do wn pro v ers are goal-orien ted but often ha v ew eak al uli when their pro of lengths are onsidered. In order to in tegrate b oth approa hes, w e try to a hiev e o op eration b et w een a top-do wn and a b ottom-up pro v er in t w o dieren tw a ys: The rst te hnique aims at supp orting a b ottom-up with a top-do wn pro v er. A top-do wn pro v er generates subgoal lauses, they are then pro essed b y a b ottom-up pro v er. The se ond te hnique deals with the use of b ottom-up generated lemmas in a top-do wn pro v er.W e apply our on ept to the areas of mo del elimination and sup erp osition. W e dis uss the abilit y of our te hniques to shorten pro ofs as w ell as to reorder the sear h spa e in anappropriate manner. In tro du tion Automated dedu tion is at its lo w est lev el a sear h problem that spans h uge sear h spa es. In the past man y dieren t al uli ha v e b een dev elop ed in order to op e with problems from the area of automated theorem pro ving. Essen tially, for rst-order theorem pro ving t w o main paradigms for al uli are in use: T op-down al uli lik e mo del elimination (ME, Lo v eland, 1968, 1978) attempt to re ursiv ely break do wn and transform a goal in to subgoals that an nally b e pro v en immediately with the axioms or with assumptions madeduring the pro of. When omparing results of v arious pro v ers (e.g., Sut lie & Suttner, 1997) it is ob vious that pro v ers based on dieren t paradigms often b eha v e quite dieren tly . There are problems where b ottom-up theorem pro v ers p erform onsiderably w ell, but top-do wn pro v ers p o orly,and vi e v ersa. The main reason for this is that b ottom-up pro v ers often suer from the la k of goal-orien tation of their sear h, but prot from their strong redundan y on trol me hanisms. Therefore, a topi that has ome in to the fo us of resear h is the in tegration of b oth approa hes. It is also p ossible to mo dify al uli or pro v ers whi h w ork a ording to one paradigm so as to in tro du e asp e ts of the other paradigm in to it. This, ho w ev er, requires a lot of implemen tational eort to mo dify the pro v ers, whereas our approa h do es not require hanges of the pro v ers but only hanges of their input. Information that is w ell-suited for impro ving the p erforman e of top-do wn pro v ers are lemmas dedu ed b y b ottom-up pro v ers. These lemmas are added to the input of a top-do wn pro v er and an help to shorten the pro of length b y immediately solving subgoals. Normally, the emplo y ed pro of pro edures an signi an tly prot from the pro of length redu tion obtained. This means that an un b ounded use of b ottom-up generated lemmas without using te hniques for ho osing only r elevant lemmas (i.e.

A knowledge system S describing a part of real world does in general not contain complete information. Reasoning with incomplete information is prone to errors since any belief derived from S may be false in the present state of the world. A false belief may suggest wrong decisions and lead to harmful actions. So an important goal is to make false beliefs as unlikely as possible. This work introduces the notions of "typical atoms" and "typical models", and shows that reasoning with typical models minimizes the expected number of false beliefs over all ways of using incomplete information. Various properties of typical models are studied, in particular, correctness and stability of beliefs suggested by typical models, and their connection to oblivious reasoning.

In computer science, ontology is a model of a domain in the form of classes and of relationships between these classes. Classes are organized in a graph the arrows of which are semantic relations. Ontology is static because the class hierarchy is fixed. In paleontology, systematic (i.e., the class hierarchies and the class relationships) is complicated by the time variable. Morphological changes over time yield, by natural selection, the emergence of new forms (taxa) differing from the ancestral morph and contemporaneous taxa of the same class hierarchy. Discovering new taxa implies, therefore, the rearrangement of the class hierarchy or the definition of new classes, based on the degree of atypicality of the new morph. Note that this phenomenon occurs in many domains such as physics, biology, linguistics, for example.

Logic programming has developed as a rich field, built over a logical substratum whose main constituent is a nonclassical form of negation, sometimes coexisting with classical negation. The field has seen the advent of a number of alternative semantics, with Kripke-Kleene semantics, the well-founded semantics, the stable model semantics, and the answer-set semantics standing out as the most successful. We show that all aforementioned semantics are particular cases of a generic semantics, in a framework where classical negation is the unique form of negation and where the literals in the bodies of the rules can be `marked' to indicate that they can be the targets of hypotheses. A particular semantics then amounts to choosing a particular marking scheme and choosing a particular set of hypotheses. When a literal belongs to the chosen set of hypotheses, all marked occurrences of that literal in the body of a rule are assumed to be true, whereas the occurrences of that literal that have not been marked in the body of the rule are to be derived in order to contribute to the firing of the rule. Hence the notion of hypothetical reasoning that is presented in this framework is not based on making global assumptions, but more subtly on making local, contextual assumptions, taking effect as indicated by the chosen marking scheme on the basis of the chosen set of hypotheses. Our approach offers a unified view on the various semantics proposed in logic programming, classical in that only classical negation is used, and links the semantics of logic programs to mechanisms that endow rule-based systems with the power to harness hypothetical reasoning.