Summary of Problems

1 Which rewrite systems can be directly defined in lambda calculus?
2 Investigate the properties of spectri for special classes of rewrite systems.
3 [Solved] What is the complexity of deciding ground-reducibility?
4 [Solved] Is it decidable whether a term is is typable in the second-order λ 2 calculus?
5 Does surjective pairing conservatively extend λβη-conversion?
6 [Solved] Is unicity of normal forms with respect to reduction a modular property of left-linear term-rewriting systems?
7 [Solved] Is it possible to decide whether the set of ground normal forms with respect to a given (finite) term-rewriting system is a regular tree language?
8 Is the decidability of strong sequentiality for orthogonal term rewriting systems NP-complete?
9 Is left-sequentiality a decidable property of orthogonal systems?
10 Has any full, finitely-generated and Church-Rosser term-rewriting system (or system with bound variables) a recursive, one-step, normalizing reduction strategy?
11 [Solved] Is unicity of normal forms a modular property of standard conditional systems?
12 [Solved] What is the complexity of the decision problem for the confluence of ground term-rewriting systems?
13 Give decidable criteria for left-linear rewriting systems to be Church-Rosser.
14 Which conditional rewrite systems are subcommutative?
15 Is the extension of Combinatory Logic by Boolean constants confluent?
16 Under what conditions does confluence of a normal semi-equational conditional term rewriting system imply confluence of the associated oriented system?
17 Is a certain conditional rewrite system, which is a linearization of Combinatory Logic extended with surjective pairing, confluent?
18 [Solved] Does “almost-confluence” hold for convergent infinite reduction sequences?
19 Can strong normalization of the typed lambda calculus be proved by a reasonably straightforward mapping from typed terms to a well-founded ordering?
20 [Solved] What is the best bound on the length of a derivation for a one-rule length-preserving string-rewriting system?
21 Is termination of one linear rule decidable?
22 [Solved] Devise practical methods for proving termination of conditional rewriting systems.
23 [Solved] Must any termination ordering used for proving termination of the Battle of Hydra and Hercules-system have the Howard ordinal as its order type?
24 Is satisfiability of lpo or rpo ordering constraints decidable in case of non-total precedences?
25 [Solved] Is the Σ₂-fragment of the first-order theory of ground terms modulo AC decidable?
26 Is it true for non-orthogonal systems that decreasing redexes implies termination? If not, can some decent subclasses be delineated for which the implication does hold?
27 How can the notion of well-rewrite-ordering be used to as the basis for some new kind of “recursive path ordering”?
28 Develop effective methods to decide whether a system decreases with respect to some exponential interpretation.
29 Which is the coarsest relation such that its union with any rewrite relation preserves termination?
30 What are the complexities of various term ordering decision problems?
31 Is there a decidable uniform word problem for which there is no variant on the rewriting theme that can decide it—without adding new symbols?
32 Is there a finite term-rewriting system of some kind for free lattices?
33 [Solved] How can completion modulo ACUI be made effective?
34 [Solved] Is there a set of inference rules that always succeeds in computing a convergent set of rewrite rules for a given set of equations and an ordering, provided that it exists?
35 [Solved] Can completion be incomplete when the ordering is changed en route?
36 Find more restrictive strategies in Boolean-ring based methods for resolution-like first-order theorem proving.
37 Is there a notion of “complete theory” for which contextual deduction is complete for refutation of ground clauses?
38 [Solved] Is unification modulo distributivity decidable?
39 Can the application condition on the Merge rule in the computation of dag-solved forms of unification problems be improved?
40 Does AC unification terminate under more flexible control?
41 [Solved] What is the complexity of the first-order theory of trees?
42 [Solved] Can negations be effectivly eliminated from first-order formulas over trees, where equality is the only predicate?
43 Design a framework for combining constraint solving algorithms.
44 How to compute finite and complete sets of unifiers for any finitary unification problem of a syntactic equational theory.
45 Which ordinals correspond to reduction graphs in the λ-calculus?
46 For which equational theories is ground reducibility of extended rewriting decidable?
47 [Solved] Prove a Parallel Moves Lemma for reductions of infinite length.
48 [Solved] Is embedding a well-quasi-ordering on strings?
49 Can completion always be made terminating when limiting the depth of occurrences of critical pairs?
50 Investigate confluence and termination of combinations of typed lambda-calculi with term rewriting systems.
51 [Solved] Is the first order theory of one-step rewriting decidable?
52 [Solved] Is there a fixed point combinator Y for which Y ↔^* Y(SI)?
53 Are there hyper-recurrent combinators?
54 In combinatory logic, is there a uniform universal generator?
55 In the λ-calculus, which sets have the form {M | Q →^* PM}?
56 Does the Church-Rosser property of abstract reduction systems imply decreasing Church-Rosser?
57 Does there exist a semigroup theory for which there is a reduced canonical term-rewriting system that is not length decreasing?
58 Is any “strongly” non-overlapping right-linear term-rewriting system confluent?
59 What are sufficient condition for the modularity of confluence?
60 [Solved] Does termination of a many-sorted rewrite system reduce to the one-sorted case in case all variables are of the same sort?
61 [Solved] Are weakly orthogonal higher-order rewrite systems confluent?
62 [Solved] Is the union of two left-linear, confluent combinatory reduction systems over the same alphabet, where the rules of the first system do not overlap the rules of the second, confluent?
63 [Solved] Is confluence of right-ground term-rewriting systems decidable?
64 Is confluence of ordered rewriting decidable when the (existential fragment of the) ordering is?
65 Is the system of Cohen and Watson for arithmetic terminating?
66 [Solved] Is there an equational theory for which unification with constants is decidable, but general unification is undecidable?
67 Investigate the exact difference between linear constant restrictions and arbitrary constant restrictions in unification problems.
68 [Solved] Is satisfiability of set constraints with projection and boolean operators decidable?
69 What is the syntactic type of (mid-, three-way) distributivity?
70 Design a notion of automata for graphs.
71 Design pattern-matching algorithms for graphs.
72 Give a definition of graph transduction that extends rational word transductions.
73 Find an embedding theorem for directed graphs.
74 How can termination orderings for term rewriting be adapted to cover those cases in which graph rewriting is terminating although term rewriting is not?
75 What sufficient conditions make confluence of general (hyper-)graph rewriting decidable?
76 [Solved] Is cycle unification decidable?
77 [Solved] Is there a finite, normal form, associative-commutative term-rewriting system for lattices?
78 [Solved] Is there a calculus of explicit substitution that is both confluent and preserves termination?
79 Does a system that is nonoverlapping under unification with infinite terms have unique normal forms?
80 Is strong sequentiality decidable for arbitrary rewrite systems?
81 [Solved] Is it possible to bound the derivation lengths of simply terminating rewrite systems by a multiply recursive function?
82 Is there a convergent extended rewrite system for ternary boolean algebra, in which certain equations hold?
83 Extend combination results on rewrite orderings to systems involving βη reductions.
84 Is unification of patterns modulo any set of variable-preserving equations decidable?
85 [Solved] Can the restrictions on orderings for the use in ordered theorem proving strategies be relaxed?
86 Is the union of two totally terminating rewrite systems, which do not share any symbols, totally terminating?
87 [Solved] Is it decidable whether a single term rewrite rule can be proved terminating by a monotonic ordering that is total on ground terms?
88 Is there a calculus of explicit substitution that is confluent on open terms, simulates one-step beta-reduction and preserves beta-strong normalization?
89 Is the satisfiablity of ordering constraints (lpo) in conjunction with predicates like irreducibility by a fixed rewrite system or membership in a regular tree language decidable?
90 Are context unification and linear second order unification decidable?
91 Does every automatic group have a presentation through some finite convergent string-rewriting system? Does every automatic monoid have an automatic structure such that the set of representatives is a prefix-closed cross-section?
92 What is the exact complexity of word unification?
93 Are the existential fragment or the positive fragment of the theory of one-step rewriting decidable?
94 Is higher-order matching decidable?
95 Is there a one-rule string rewriting system that is non-terminating but also non-looping?
96 Is the word problem for all proper combinators of order smaller than 3 decidable?
97 Is the word problem for the S-combinator decidable?
98 Is unification modulo the theory of allegories decidable?
99 [Solved] Is the first-order theory of any Knuth-Bendix ordering decidable?
100 Design new termination methods based on the gap-embedding theorems of Friedman and Kriz.
101 Are universality and inclusion of AC-recognizable languages decidable?
102 Investigate normalization by a canonical term rewrite system in the setting of second-order monadic logic
103 Equational axiomatization of graph operations
104 [Solved] Termination of replacing two successive occurrences of the same symbol in a string
105 [Solved] Derivational complexity of replacing two successive occurrences of the same symbol in a string
106 Can we use the dependency pair method to prove relative termination?
107 Give a complete (resource free) characterisation of rewrite systems with polynomial derivational complexity.

[RTALooP home]

1	Which rewrite systems can be directly defined in lambda calculus?
2	Investigate the properties of spectri for special classes of rewrite systems.
3	[Solved] What is the complexity of deciding ground-reducibility?
4	[Solved] Is it decidable whether a term is is typable in the second-order λ 2 calculus?
5	Does surjective pairing conservatively extend λβη-conversion?
6	[Solved] Is unicity of normal forms with respect to reduction a modular property of left-linear term-rewriting systems?
7	[Solved] Is it possible to decide whether the set of ground normal forms with respect to a given (finite) term-rewriting system is a regular tree language?
8	Is the decidability of strong sequentiality for orthogonal term rewriting systems NP-complete?
9	Is left-sequentiality a decidable property of orthogonal systems?
10	Has any full, finitely-generated and Church-Rosser term-rewriting system (or system with bound variables) a recursive, one-step, normalizing reduction strategy?
11	[Solved] Is unicity of normal forms a modular property of standard conditional systems?
12	[Solved] What is the complexity of the decision problem for the confluence of ground term-rewriting systems?
13	Give decidable criteria for left-linear rewriting systems to be Church-Rosser.
14	Which conditional rewrite systems are subcommutative?
15	Is the extension of Combinatory Logic by Boolean constants confluent?
16	Under what conditions does confluence of a normal semi-equational conditional term rewriting system imply confluence of the associated oriented system?
17	Is a certain conditional rewrite system, which is a linearization of Combinatory Logic extended with surjective pairing, confluent?
18	[Solved] Does “almost-confluence” hold for convergent infinite reduction sequences?
19	Can strong normalization of the typed lambda calculus be proved by a reasonably straightforward mapping from typed terms to a well-founded ordering?
20	[Solved] What is the best bound on the length of a derivation for a one-rule length-preserving string-rewriting system?
21	Is termination of one linear rule decidable?
22	[Solved] Devise practical methods for proving termination of conditional rewriting systems.
23	[Solved] Must any termination ordering used for proving termination of the Battle of Hydra and Hercules-system have the Howard ordinal as its order type?
24	Is satisfiability of lpo or rpo ordering constraints decidable in case of non-total precedences?
25	[Solved] Is the Σ₂-fragment of the first-order theory of ground terms modulo AC decidable?
26	Is it true for non-orthogonal systems that decreasing redexes implies termination? If not, can some decent subclasses be delineated for which the implication does hold?
27	How can the notion of well-rewrite-ordering be used to as the basis for some new kind of “recursive path ordering”?
28	Develop effective methods to decide whether a system decreases with respect to some exponential interpretation.
29	Which is the coarsest relation such that its union with any rewrite relation preserves termination?
30	What are the complexities of various term ordering decision problems?
31	Is there a decidable uniform word problem for which there is no variant on the rewriting theme that can decide it—without adding new symbols?
32	Is there a finite term-rewriting system of some kind for free lattices?
33	[Solved] How can completion modulo ACUI be made effective?
34	[Solved] Is there a set of inference rules that always succeeds in computing a convergent set of rewrite rules for a given set of equations and an ordering, provided that it exists?
35	[Solved] Can completion be incomplete when the ordering is changed en route?
36	Find more restrictive strategies in Boolean-ring based methods for resolution-like first-order theorem proving.
37	Is there a notion of “complete theory” for which contextual deduction is complete for refutation of ground clauses?
38	[Solved] Is unification modulo distributivity decidable?
39	Can the application condition on the Merge rule in the computation of dag-solved forms of unification problems be improved?
40	Does AC unification terminate under more flexible control?
41	[Solved] What is the complexity of the first-order theory of trees?
42	[Solved] Can negations be effectivly eliminated from first-order formulas over trees, where equality is the only predicate?
43	Design a framework for combining constraint solving algorithms.
44	How to compute finite and complete sets of unifiers for any finitary unification problem of a syntactic equational theory.
45	Which ordinals correspond to reduction graphs in the λ-calculus?
46	For which equational theories is ground reducibility of extended rewriting decidable?
47	[Solved] Prove a Parallel Moves Lemma for reductions of infinite length.
48	[Solved] Is embedding a well-quasi-ordering on strings?
49	Can completion always be made terminating when limiting the depth of occurrences of critical pairs?
50	Investigate confluence and termination of combinations of typed lambda-calculi with term rewriting systems.
51	[Solved] Is the first order theory of one-step rewriting decidable?
52	[Solved] Is there a fixed point combinator Y for which Y ↔^* Y(SI)?
53	Are there hyper-recurrent combinators?
54	In combinatory logic, is there a uniform universal generator?
55	In the λ-calculus, which sets have the form {M \| Q →^* PM}?
56	Does the Church-Rosser property of abstract reduction systems imply decreasing Church-Rosser?
57	Does there exist a semigroup theory for which there is a reduced canonical term-rewriting system that is not length decreasing?
58	Is any “strongly” non-overlapping right-linear term-rewriting system confluent?
59	What are sufficient condition for the modularity of confluence?
60	[Solved] Does termination of a many-sorted rewrite system reduce to the one-sorted case in case all variables are of the same sort?
61	[Solved] Are weakly orthogonal higher-order rewrite systems confluent?
62	[Solved] Is the union of two left-linear, confluent combinatory reduction systems over the same alphabet, where the rules of the first system do not overlap the rules of the second, confluent?
63	[Solved] Is confluence of right-ground term-rewriting systems decidable?
64	Is confluence of ordered rewriting decidable when the (existential fragment of the) ordering is?
65	Is the system of Cohen and Watson for arithmetic terminating?
66	[Solved] Is there an equational theory for which unification with constants is decidable, but general unification is undecidable?
67	Investigate the exact difference between linear constant restrictions and arbitrary constant restrictions in unification problems.
68	[Solved] Is satisfiability of set constraints with projection and boolean operators decidable?
69	What is the syntactic type of (mid-, three-way) distributivity?
70	Design a notion of automata for graphs.
71	Design pattern-matching algorithms for graphs.
72	Give a definition of graph transduction that extends rational word transductions.
73	Find an embedding theorem for directed graphs.
74	How can termination orderings for term rewriting be adapted to cover those cases in which graph rewriting is terminating although term rewriting is not?
75	What sufficient conditions make confluence of general (hyper-)graph rewriting decidable?
76	[Solved] Is cycle unification decidable?
77	[Solved] Is there a finite, normal form, associative-commutative term-rewriting system for lattices?
78	[Solved] Is there a calculus of explicit substitution that is both confluent and preserves termination?
79	Does a system that is nonoverlapping under unification with infinite terms have unique normal forms?
80	Is strong sequentiality decidable for arbitrary rewrite systems?
81	[Solved] Is it possible to bound the derivation lengths of simply terminating rewrite systems by a multiply recursive function?
82	Is there a convergent extended rewrite system for ternary boolean algebra, in which certain equations hold?
83	Extend combination results on rewrite orderings to systems involving βη reductions.
84	Is unification of patterns modulo any set of variable-preserving equations decidable?
85	[Solved] Can the restrictions on orderings for the use in ordered theorem proving strategies be relaxed?
86	Is the union of two totally terminating rewrite systems, which do not share any symbols, totally terminating?
87	[Solved] Is it decidable whether a single term rewrite rule can be proved terminating by a monotonic ordering that is total on ground terms?
88	Is there a calculus of explicit substitution that is confluent on open terms, simulates one-step beta-reduction and preserves beta-strong normalization?
89	Is the satisfiablity of ordering constraints (lpo) in conjunction with predicates like irreducibility by a fixed rewrite system or membership in a regular tree language decidable?
90	Are context unification and linear second order unification decidable?
91	Does every automatic group have a presentation through some finite convergent string-rewriting system? Does every automatic monoid have an automatic structure such that the set of representatives is a prefix-closed cross-section?
92	What is the exact complexity of word unification?
93	Are the existential fragment or the positive fragment of the theory of one-step rewriting decidable?
94	Is higher-order matching decidable?
95	Is there a one-rule string rewriting system that is non-terminating but also non-looping?
96	Is the word problem for all proper combinators of order smaller than 3 decidable?
97	Is the word problem for the S-combinator decidable?
98	Is unification modulo the theory of allegories decidable?
99	[Solved] Is the first-order theory of any Knuth-Bendix ordering decidable?
100	Design new termination methods based on the gap-embedding theorems of Friedman and Kriz.
101	Are universality and inclusion of AC-recognizable languages decidable?
102	Investigate normalization by a canonical term rewrite system in the setting of second-order monadic logic
103	Equational axiomatization of graph operations
104	[Solved] Termination of replacing two successive occurrences of the same symbol in a string
105	[Solved] Derivational complexity of replacing two successive occurrences of the same symbol in a string
106	Can we use the dependency pair method to prove relative termination?
107	Give a complete (resource free) characterisation of rewrite systems with polynomial derivational complexity.