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 Σ_{2}-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. |