Chair for Automata Theory of the Institute for Theoretical Computer Science, Faculty of Computer Science at TU Dresden

Technical Reports

1996

 F. Baader and C. Tinelli. A New Approach for Combining Decision Procedures for the Word Problem, and Its Connection to the Nelson-Oppen Combination Method. LTCS-Report 96-01, LuFg Theoretical Computer Science, RWTH Aachen, 1996. An abridged version has appeared in Proc. CADE'97, Springer LNAI 1249.
Bibtex entry  Paper (PS)

Abstract

The Nelson-Oppen combination method can be used to combine decision procedures for the validity of quantifier-free formulae in first-order theories with disjoint signatures, provided that the theories to be combined are stably infinite. We show that, even though equational theories need not satisfy this property, Nelson and Oppen's method can be applied, after some minor modifications, to combine decision procedures for the validity of quantifier-free formulae in equational theories. Unfortunately, and contrary to a common belief, the method cannot be used to combine decision procedures for the word problem. We present a method that solves this kind of combination problem. Our method is based on transformation rules and also applies to equational theories that share a finite number of constant symbols.

F. Baader and U. Sattler. Number Restrictions on Complex Roles in Description Logics. LTCS-Report 96-02, LuFg Theoretical Computer Science, RWTH Aachen, 1996. An abridged version has appeared in the Proceedings of the Fifth International Conference on Knowledge Representation and Reasoning, 1996, Cambridge, Massachusetts.
Bibtex entry  Paper (PS)

F. Baader and U. Sattler. Description Logics with Symbolic Number Restrictions. LTCS-Report 96-03, LuFg Theoretical Computer Science, RWTH Aachen, 1996. An abridged version has appeared in the Proceedings of the 12th European Conference on Artificial Intelligence, 1996, Budapest, Hungary.
Bibtex entry  Paper (PS)

S. Kepser and J. Richts. Optimisation Techniques for Combining Constraint Solvers. LTCS-Report 96-04, LuFG Theoretical Computer Science, RWTH Aachen, Germany, 1996.
Bibtex entry  Paper (PS)

Abstract

In recent years, techniques that had been developed for the combination of unification algorithms for equational theories were extended to combining constraint solvers. These techniques inherited an old deficit that was already present in the combination of equational theories which makes them rather unsuitable for practical use: The underlying combination algorithms are highly non-deterministic. This paper is concerned with the practical problem of how to optimise the combination method of Baader and Schulz. We present two optimisation methods, called the iterative and the deductive method. The iterative method reorders and localises the non-deterministic decisions. The deductive method uses specific algorithms for the components to reach certain decisions deterministically. Run time tests of our implementation indicate that the optimised combination method yields combined decision procedures that are efficient enough to be used in practice.

F. Baader. Combination of Compatible Reduction Orderings that are Total on Ground Terms. LTCS-Report 96-05, LuFg Theoretical Computer Science, RWTH Aachen, Germany, 1996.
Bibtex entry  Paper (PS)

Abstract

Reduction orderings that are compatible with an equational theory $E$ and total on (the $E$-equivalence classes of) ground terms play an important role in automated deduction. We present a general approach for combining such orderings. To be more precise, we show how $E_1$-compatible reduction orderings total on $\Sigma_1$-ground terms and $E_2$-compatible reduction orderings total on $\Sigma_2$-ground terms can be used to construct an $(E_1\cup E_2)$-compatible reduction ordering total on $(\Sigma_1\cup \Sigma_2)$-ground terms, provided that the signatures are disjoint and some other (rather weak) restrictions are satisfied. This work was motivated by the observation that it is often easier to construct such orderings for ``small'' signatures and theories separately, rather than directly for their union.

There is also a complete overview of our technical reports.
home Back to the homepage of the Chair for Automata Theory.
Generated at Fri Jun 12 11:21:13 CEST 2009.