Summary of Problems

1Which rewrite systems can be directly defined in lambda calculus?
2Investigate 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?
8Is the decidability of strong sequentiality for orthogonal term rewriting systems NP-complete?
9Is left-sequentiality a decidable property of orthogonal systems?
10Has 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.
14Which conditional rewrite systems are subcommutative?
15Is the extension of Combinatory Logic by Boolean constants confluent?
16Under what conditions does confluence of a normal semi-equational conditional term rewriting system imply confluence of the associated oriented system?
17Is 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?
24Is satisfiability of lpo or rpo ordering constraints decidable in case of non-total precedences?
25[Solved] Is the Σ2-fragment of the first-order theory of ground terms modulo AC decidable?
26Is 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?
27How can the notion of well-rewrite-ordering be used to as the basis for some new kind of “recursive path ordering”?
28Develop 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?
30What are the complexities of various term ordering decision problems?
31Is there a decidable uniform word problem for which there is no variant on the rewriting theme that can decide it—without adding new symbols?
32Is 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?
36Find 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?
39Can the application condition on the Merge rule in the computation of dag-solved forms of unification problems be improved?
40Does 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?
43Design a framework for combining constraint solving algorithms.
44How to compute finite and complete sets of unifiers for any finitary unification problem of a syntactic equational theory.
45Which ordinals correspond to reduction graphs in the λ-calculus?
46For 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?
49Can completion always be made terminating when limiting the depth of occurrences of critical pairs?
50Investigate 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)?
53Are there hyper-recurrent combinators?
54In combinatory logic, is there a uniform universal generator?
55In the λ-calculus, which sets have the form {M | Q* PM}?
56Does the Church-Rosser property of abstract reduction systems imply decreasing Church-Rosser?
57Does there exist a semigroup theory for which there is a reduced canonical term-rewriting system that is not length decreasing?
58Is any “strongly” non-overlapping right-linear term-rewriting system confluent?
59What 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?
64Is confluence of ordered rewriting decidable when the (existential fragment of the) ordering is?
65Is 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?
67Investigate 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?
69What is the syntactic type of (mid-, three-way) distributivity?
70Design a notion of automata for graphs.
71Design 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?
82Is there a convergent extended rewrite system for ternary boolean algebra, in which certain equations hold?
83Extend combination results on rewrite orderings to systems involving βη reductions.
84Is 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?
88Is there a calculus of explicit substitution that is confluent on open terms, simulates one-step beta-reduction and preserves beta-strong normalization?
89Is 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?
90Are context unification and linear second order unification decidable?
91Does 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?
92What is the exact complexity of word unification?
93Are the existential fragment or the positive fragment of the theory of one-step rewriting decidable?
94Is higher-order matching decidable?
95 Is there a one-rule string rewriting system that is non-terminating but also non-looping?
96Is the word problem for all proper combinators of order smaller than 3 decidable?
97Is the word problem for the S-combinator decidable?
98Is unification modulo the theory of allegories decidable?
99[Solved] Is the first-order theory of any Knuth-Bendix ordering decidable?
100Design new termination methods based on the gap-embedding theorems of Friedman and Kriz.
101Are 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]