We propose techniques to provide calculi based on the connection method with a possibility to preclude infinite loops. We extend previous work — proposed in the field of Logic Programming — concerning the detection of infinite loops during the proof of Horn formulas. On the one hand, we present a technique to be integrated into connection calculi for full first-order logic. On the other hand, we show how dependencies between goals can be used to yield stronger pruning techniques.

We propose an approach to approximate classical reasoning via well-known theorem-proving techniques. Unlike other approaches, our approach takes into acconnt the interplay of knowledge bases and queries and thus allows for query-sensitive approximate reasoning. We demonstrate that our approach deals extremely well with the examples found in the literature. This reveals that conventional theorem-proving techniques can account for approximate reasoning.

In this paper we present a method to detect non-provable goals. The general idea, adopted from cycle unification, is to determine in advance how terms may be modified during a derivation. Since a complete predetermination is obviously not possible, we analyze how terms may be changed by, roughly speaking, adding and deleting function symbols. Such changes of a term are encoded by an efficiently decidable clause set. The satisfiability of such a set ensures that the goal containing the term under consideration cannot contribute to a successful derivation.

XRay is a theorem prover for default logics. Its deductive power is primarily due to our approach of integrating default reasoning into existing model elimination based provers using the well-known PTTP approach. We conceived and integrated a number of enhancements, such as lemma handling, regularity-based truncations of underlying search spaces and a model-based approach to consistency checking.

We propose a model-based approach to incremental consistency checking in default theorem proving. We show that the crucial task of consistency checking can benefit from keeping models in order to restrict the attention to ultimately necessary consistency checks. This is supported by the concept of default lemmata that allow for an additional avoidance of redundancy.

An important advantage of deductive approaches for solving planning problems is the possibility to exploit powerful proof methods and techniques to reduce the search space developed in the field of automated deduction. The aim of this paper is to adapt such techniques to build efficient resource-oriented planning systems.

For many reasoning tasks in Artificial Intelligence, it is much simpler (or even essential) to deal with ground inferences rather than with inferences comprising variables. The usual approach to guarantee ground inferences is to introduce means for enumerating the underlying Herbrand-universe so that during subsequent inferences variables become bound in turn to the respective Herbrand-terms. The inherent problem with such an approach is that it may cause a tremendous number of unnecessary backtracking steps due to heaps of incorrect variable instantiations. In this paper, we propose a new concept that refrains from backtracking by appeal to novel inference rules that allow for correcting previous variable bindings. We show that our approach is not only beneficial for classical proof systems but it is also well-suited for tasks in knowledge representation and reasoning. The major contribution of this paper lies actually in an application of our approach to a calculi conceived for reasoning with default logic.

In a previous paper we proposed an approach to exploit literal equivalences in connection tableau based calculi. There we showed that making equivalences explicit offers new possibilities for search space reduction by applying literal demodulation for simplification and by strengthening the well-known regularity refinement. In this paper we generalize this approach to handle conditional equivalences. The generalization is mainly motivated by the circumstance that nonconditional equivalences, if not present at the beginning of a deduction, are much harder to generate than conditional ones.

The Model Elimination (ME) calculus is a refutationally complete,goal-oriented calculus for first-order clause logic. In this article, weintroduce a new variant called disjunctive positive ME (DPME); it improveson Plaisted’s positive refinement of ME in that reduction steps areallowed only with positive literals stemming from clauses having at leasttwo positive literals (so-called disjunctive clauses). DPME is motivated byits application to various kinds of subsumption deletion: in order to applysubsumption deletion in ME equally successful as in resolution, it iscrucial to employ a version of ME that minimizes ancestor context (i.e., thenecessary A-literals to find a refutation). DPME meets this demand. Wedescribe several variants of ME with subsumption, the most important onesbeing ME with backward and forward subsumption and theT*-Context Check. We compare their pruning power, also takinginto consideration the well-known regularity restriction. All proofs aresupplied. The practicability of our approach is demonstrated with experiments.

To model in a formal system the remarkable ability of human agents to reason about situations, actions, and causality has always been a major research goal in Intellectics. Most of the work towards this goal is based on the situation calculus which, however, has the disadvantage that it requires either to state frame axioms or to use non-monotonic logic and a commonsense law of inertia. A deductive approach which does not show this disadvantage is the linear connection method whose key idea is to treat facts about a situation as resources which can be consumed and produced by actions. It was shown that this approach properly handles planning problems which only allow deterministic actions, i.e. actions which are not allowed to have several alternative effects. In this paper we extend and revise the linear connection method to overcome this restriction.