Author name cluster

Andrea Sattler-Klein

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

3 papers

2 author rows

TCS Journal 2010 Journal Article

Some complexity results for prefix Gröbner bases in free monoid rings

Andrea Sattler-Klein

We establish the following complexity results for prefix Gröbner bases in free monoid rings: 1. | R | ⋅ s i z e ( p ) reduction steps are sufficient to normalize a given polynomial p w. r. t. a given right-normalized system R of prefix rules compatible with some total admissible well-founded ordering >. 2. O ( | R | ⋅ s i z e ( R ) ) basic steps are sufficient to transform a given terminating system R of prefix rules into an equivalent right-normalized system. 3. O ( | R | 2 ⋅ s i z e ( R ) ) basic steps are sufficient to decide whether or not a given terminating system R of prefix rules is a prefix Gröbner basis. The latter result answers an open question posed by Zeckzer (2000) [9].

Details DOI

I&C Journal 1996 Journal Article

Proof Lengths for Equational Completion

David A. Plaisted
Andrea Sattler-Klein

We first show that ground term-rewriting systems can be completed in a polynomial number of rewriting steps, if the appropriate data structure for terms is used. We then apply this result to study the lengths of critical pair proofs in non-ground systems, and obtain bounds on the lengths of critical pair proofs in the non-ground case. We show how these bounds depend on the types of inference steps that are allowed in the proofs.

Details DOI

LPAR Conference 1992 Conference Paper

Infinite, Canonical String Rewriting Systems Generated by Completion

Andrea Sattler-Klein

Abstract Most versions of the Knuth-Bendix completion ’procedure’ are designed to compute when possible a canonical rewriting system. We show that even for string rewriting systems ( SRSs ) canonical systems may be generated by completion which are not recursively enumerable. This may happen also if the SRS has decidable word problem. We analyze how this phenomenon depends on the ordering used for completion. It turns out that in general if a SRS is completed with respect to a length-lexicographic ordering divergence sequences encoding the input/output behaviour of any primitive recursive function as well as any recursively enumerable set and some non recursively enumerable sets may be generated. But, if a SRS with decidable word problem is completed with such an ordering, then the generated canonical system will be recursive.

Details