Abstracts of papers (co-)authored/edited by Bernhard Gramlich

• International Conference and Workshop Papers
• Journal Papers
• Books, Book Chapters and(Co-)Edited Works
• Theses
• National Conference and Workshop Papers
• Technical Reports

International Conference and Workshop Papers

• Karl Gmeiner, Bernhard Gramlich and Felix Schernhammer
  On Soundness Conditions for Unraveling Deterministic Conditional Rewrite Systems
  Proc. 23rd International Conference on Rewriting Techniques and Applications (RTA 2012), Nagoya, Japan, May 28 - June 2, 2012, Ashish Tiwari, ed., LIPIcs (Leibniz International Proceedings in Informatics), 2012, to appear.
  
  Abstract We study (un)soundness of transformations of conditional term rewriting systems (CTRSs) into unconditional term rewriting systems (TRSs). The focus here is on analyzing (un)soundness of so-called unravelings, the most basic and natural class of such transformations. We extend our previous analysis from normal 1-CTRSs to the more general class of deterministic CTRSs (DCTRSs) where extra variables in right-hand sides of rules are allowed to a certain extent. We prove that the previous soundness results based on weak left-linearity and on right-linearity can be extended from normal 1-CTRSs to DCTRSs. Counterexamples show that such an extension to DCTRSs does not work for the previous criteria which were based on confluence and on non-erasingness, not even for right-stable systems. Yet, we prove weaker versions of soundness criteria based on confluence and on non-erasingness. Finally, we compare our approach and results with other recently established soundness criteria for unraveling DCTRSs.
  
  
• Eugen Jiresch and Bernhard Gramlich
  Realizing Monads in Interaction Nets via Generic Typed Rules
  Proc. 9th Annual conference on Theory and Applications of Models of Computation (TAMC 2012), Beijing, China, May 16-21, 2012, Springer LNCS, Manindra Agrawal, S. Barry Cooper and Angsheng Li, eds., 2012, to appear.
  
  Abstract The modularity of termination and confluence properties of term rewriting systems has been extensively studied, for disjoint unions and other more types of combinations. However, for rewriting under strategies the theory is less well explored. Here we extend the modularity analysis of termination properties systematically to (variants of) innermost and outermost rewriting. It turns out --- as expected --- that in essence innermost rewriting behaves nicely w.r.t. modularity of termination properties, whereas this is not at all the case for outermost rewriting, at least not without further assumptions.
  
  
• Bernhard Gramlich and Klaus Györgyfalvay
  On Modularity of Termination Properties of Rewriting under Strategies
  Proc. 12th International Workshop on Termination (Extended Abstracts) (WST 2012) Obergurgl, Austria, February 19-23, 2012, Georg Moser, ed., pp. 59-63, 2012.
  
  Abstract The modularity of termination and confluence properties of term rewriting systems has been extensively studied, for disjoint unions and other more types of combinations. However, for rewriting under strategies the theory is less well explored. Here we extend the modularity analysis of termination properties systematically to (variants of) innermost and outermost rewriting. It turns out --- as expected --- that in essence innermost rewriting behaves nicely w.r.t. modularity of termination properties, whereas this is not at all the case for outermost rewriting, at least not without further assumptions.
  
  
• Karl Gmeiner, Bernhard Gramlich and Felix Schernhammer
  On (Un)Soundness of Unravelings
  Proc. 21st International Conference on Rewriting Techniques and Applications (RTA 2010), Edinburgh, Scotland, UK, July 11-13, 2010, Christopher Lynch, ed., LIPIcs (Leibniz International Proceedings in Informatics) volume, 2010.
  
  Abstract We revisit (un)soundness of transformations of conditional into unconditional rewrite systems. The focus here is on so-called unravelings, the most simple and natural kind of such transformations, for the class of normal conditional systems without extra variables. By a systematic and thorough study of existing counterexamples and of the potential sources of unsoundness we obtain several new positive and negative results. In particular, we prove the following new results: Confluence, non-erasingness and weak left-linearity (of a given conditional system) each guarantee soundness of the unraveled version w.r.t. the original one. The latter result substantially extends the only known sufficient criterion for soundness, namely left-linearity. Furthermore, by means of counterexamples we refute various other tempting conjectures about sufficient conditions for soundness.
  
  
• Bernhard Gramlich and Felix Schernhammer
  Outermost Termination via Contextual Dependency Pairs
  Proc. 11th International Workshop on Termination (WST 2010), Edinburgh, Scotland, UK, July 14-15, 2010, Peter Schneider-Kamp, ed., 2010.
  
  Abstract Recently, the problem of proving outermost termination has been addressed mainly by methods relying on transformations. Here we describe a more direct approach inspired by the dependency pair (DP) framework of [Giesl et al., JAR 2006]. The basic idea is to enrich dependency pairs by an additional component, namely the calling context of the corresponding recursive function call. Then one can use the additional contextual information to model DP chains adhering to certain strategies (e.g. the outermost strategy). Additionally, existing methods of the ordinary DP approach can partly be reused.
  
  
• Bernhard Gramlich and Felix Schernhammer
  Termination of Rewriting with - and Automated Synthesis of - Forbidden Patterns
  Prelim. Proc. 1st International Workshop on Strategies in Rewriting, Proving, and Programming (IWS 2010), Edinburgh, Scotland, UK, July 9, 2010, pp. 13-17, Hélène Kirchner and César Muñoz, eds., 2010.
  
  
• Felix Schernhammer and Bernhard Gramlich
  VMTL - A Modular Termination Laboratory
  Proc. 20th International Conference on Rewriting Techniques and Applications (RTA 2009), Brasilia, Brazil, Jne 29 - July 1, 2009, Ralf Treinen, ed., LNCS 5595, pp. 285-294, Springer-Verlag, 2009.
  
  Abstract The automated analysis of termination of term rewriting systems (TRSs) has drawn a lot of attention in the scientific community during the last decades and many different methods and approaches have been developed for this purpose. We present VMTL (Vienna Modular Termination Laboratory), a tool implementing some of the most recent and powerful algorithms for termination analysis of TRSs, while providing an open interface that allows users to easily plug in new algorithms in a modular fashion according to the widely adopted dependency pair framework. Apart from modular extensibility, VMTL focuses on analyzing the termination behaviour of conditional term rewriting systems (CTRSs). Using one of the latest transformational techniques, the resulting restricted termination problems (for unconditional context-sensitive TRSs) are processed with dedicated algorithms.
  
  
• Bernhard Gramlich and Felix Schernhammer
  Extending Context-Sensitivity in Term Rewriting
  Prelim. Proc. 9th International Workshop on Reduction Strategies in Rewriting and Programming (RTA 2009), Brasilia, Brazil, June 28, 2009, Maribel Fernandez, ed., pp. 25-29, June 2009.
  
  Abstract Context-sensitive rewriting as pioneered by [Lucas 1995] has turned out to be a remarkably fruitful concept in many respects. Still, various examples and problems cannot be treated in a satisfactory way within this framework, because the underlying notion of context-sensitivity is too rigid and specialized. From a systematic point of view, it is only a very special case of a more general concept of context-sensitivity. In this contribution we will discuss more general versions of context-sensitivity, the relationships among them and the commonly used notion of context-sensitivity, as well as their feasibility from a computational point of view. In particular, we will present first steps towards an extended approach for context-sensitivity that is based on the notion of "forbidden patterns" which appears to be a reasonable compromise between expressive power and practical feasibility. The basic idea here is that a rewrite step should be forbidden if the redex to be contracted has a certain shape and appears in a certain context.
  
  
• Felix Schernhammer and Bernhard Gramlich
  On Some Implementation Aspects of VMTL
  Proc. 10th International Workshop on Termination (WST 2009), Leipzig, Germany, June 3-5, 2009, Alfons Geser and Johannes Waldmann, ed., pp. 72-75, 2009.
  
  Abstract VMTL (Vienna Modular Termination Laboratory) is a program designed to (semi-) automatically prove termination of various classes of term rewriting systems, including conditional and context-sensitive ones. VMTL is extensible in that it provides easy to use, public interfaces for the addition of new dependency pair processors and transformations. Moreover, VMTL provides implementations of several standard processors and transformations out of the box. In this work we describe and discuss implementation details of several DP processors currently available in VMTL. In particular the dependency graph, subterm principle, narrowing and instantiation processors are described and several non-standard modifications and generalizations of these processors are proposed.
  
  
• Karl Gmeiner and Bernhard Gramlich
  Transformations of Conditional Rewrite Systems Revisited
  Recent Trends in Algebraic Development Techniques (WADT 2008) - Revised Selected Papers, Andrea Corradini and Ugo Montanari, eds., LNCS 5486, pp. 166-186, Springer, 2009.
  
  Abstract We revisit known transformations of conditional rewrite systems to unconditional ones in a systematic way. We present a unified framework for describing, analyzing and classifying such transformations, discuss the major problems arising, and finally present a new transformation which has some advantages as compared to the approach of [Serbanuta/Rosu-RTA'06]. The key feature of our new approach (for left-linear confluent normal 1-CTRSs) is that it is backtracking-free due to an appropriate encoding of the conditions.
  
  
• Felix Schernhammer and Bernhard Gramlich
  On Operational Termination of Deterministic Conditional Rewrite Systems
  Proc. 20th Nordic Workshop on Programming Theory (Extended Abstracts) (NWPT 2008), Tarmo Uustalu, Jüri Vain and Juhan Emits, eds., pp. 84-86, Tallinn, Estonia, November 19-21, 2008.
  
  Abstract We characterize the practically important notion of operational termination of deterministic conditional term rewriting systems (DCTRSs) by context-sensitive termination of a transformed TRS on original terms. Experimental evaluations show that this new approach yields more power when verifying operational termination than existing ones. Moreover, it allows us to disprove operational termination of DCTRSs.
  
  
• Karl Gmeiner and Bernhard Gramlich
  Transformations of Conditional Rewrite Systems Revisited
  Prelim. Proc. 19th International Workshop on Algebraic Development Techniques (WADT 2008), Andrea Corradini and Fabio Gadducci, eds., pp. 64-66, Pisa, Italy, June 13-16, 2008.
  
  Abstract We revisit known transformations of conditional rewrite systems to unconditional ones in a systematic way. We present a unified framework for describing and classifying such transformations, discuss the major problems arising, provide simplified (old) and new counterexamples to certain (desirable) properties of specific transformations, and finally present a new transformation which has some advantages as compared to a quite recent approach, namely the one of [Serbanuta/Rosu-RTA'06].
  
  
• Felix Schernhammer and Bernhard Gramlich
  On Proving and Characterizing Operational Termination of Deterministic Conditional Rewrite Systems
  Proc. 9th International Workshop on Termination - Extended Abstracts (WST 2007, held as part of RDP 2007, 4th Federated Conference on Rewriting, Deduction, and Programming), pp. 82-85, Dieter Hofbauer and Alexander Serebrenik, eds., Paris, France, June 29, 2007.
  
  Abstract Conditional term rewriting systems (CTRSs) are a natural extension of unconditional such systems (TRSs) allowing rules to be guarded by conditions. Conditional rules tend to be very intuitive and easy to formulate and are therefore used in several programming and specification languages, such as Maude or ELAN. Besides, the particular class of deterministic (oriented) CTRSs (DCTRSs) has been used for instance in proofs of termination of (well-moded) logic programs, [Ganzinger/Waldmann'92]. Recently, the notion of operational termination of DCTRSs was defined in [Lucas/Marché/Meseguer'05], which guarantees finite reductions in existing rewrite engines. In [Ohlebusch'02], based on the idea of unravelings of [Marchiori'96], a transformation from DCTRSs into TRSs was proposed, such that termination of the transformed TRS implies quasi-reductivity of the DCTRS. In this extended abstract we provide an alternative definition of quasi-reductivity, which allows us to prove the property for strictly more DCTRSs than Ohlebusch's transformation was able to handle, while preserving the important implications of quasi-reductivity. The key concept used is context-sensitive rewriting [Lucas'01]. We define a transformation from DCTRSs into context-sen\-sitive (unconditional) TRSs such that termination of the transformed context-sensitive TRS implies context-sensitive quasi-reductivity of the DCTRS. Furthermore we relate the latter notion to other known ones and give equivalent characterizations of operational termination.
  
  
  
• Felix Schernhammer and Bernhard Gramlich
  Termination of Lazy Rewriting Revisited
  Proc. 7th International Workshop on Reduction Strategies in Rewriting and Programming (WRS 2007, held as part of RDP 2007, 4th Federated Conference on Rewriting, Deduction, and Programming), pp. 28-42, Jürgen Giesl, ed., Paris, France, June 25, 2007.
  
  Abstract Lazy rewriting is a proper restriction of term rewriting that dynamically restricts the reduction of certain arguments of functions in order to obtain termination. In contrast to context-sensitive rewriting reductions at such argument positions are not completely forbidden but delayed. Based on the observation that the only existing (non-trivial) approach to prove termination of such lazy rewrite systems is flawed, we develop a modified approach for transforming lazy rewrite systems into context-sensitive ones that is sound and complete with respect to termination.
  
  
• Bernhard Gramlich
  Generalizing Newman's Lemma for Left-Linear Rewrite Systems
  Proc. 17th International Conference on Rewriting Techniques and Applications (RTA 2006), held as part of FLoC 2006 (4th Federated Logic Conference), Seattle, Washington, USA, August 10-22, 2006, Frank Pfenning, ed., LNCS 4098, pp. 66-80, Springer, August 2006.
  
  Abstract Confluence criteria for non-terminating rewrite systems are known to be rare and notoriously difficult to obtain. Here we prove a new result in this direction. Our main result is a generalized version of Newman's Lemma for left-linear term rewriting systems that does not need a full termination assumption. We discuss its relationships to previous confluence criteria, its restrictions, examples of application as well as open problems. The whole approach is developed in the (more general) framework of context-sensitive rewriting which thus turns out to be useful also for ordinary (context-free) rewriting.
  
  
  
• Bernhard Gramlich
  On Strategies for Inductive Theorem Proving [Invited Talk]
  Proc. 5th International Workshop on Strategies in Automated Deduction (STRATEGIES 2004), held in conjunction with IJCAR 2004 (2nd International Joint Conference on Automated Reasoning), Cork, Ireland, July 4, 2004, Maria Paola Bonacina and Thierry Boy de la Tour, eds., pp. 62-63 (abstract), July 2004.
  
  Abstract Inductive Theorem Proving (ITP) is a challenging field in automated reasoning and theorem proving. Typically, Automated Theorem Proving (ATP) refers to methods, techniques and tools for automatically proving general (most often first-order) theorems. Nowadays, the field of ATP has reached a certain degree of maturity and powerful ATP systems are widely available and used. The situation with ITP is strikingly different, in the sense that proving inductive theorems in an essentially automatic way still is a very challenging task, even for the most advanced existing ITP systems. Both in general ATP and in ITP strategies for guiding the proof search process are of fundamental importance, in automated as well as in interactive or mixed settings. In the talk we will try to give a thorough assessment of strategies in ITP and, more generally, of the main structural, conceptual and technical problems and challenges that need to be addressed in order to achieve major progress towards Automated Inductive Theorem Proving (AITP).
  
  
  
• Bernhard Gramlich
  Modularity of Termination of Left-Linear Rewrite Systems Revisited
  Proc. 7th International Workshop on Termination - Extended Abstracts (WST 2004), part of RDP 2004 (2nd Federated Conference on Rewriting, Deduction, and Programming), Aachen, Germany, June 1-2, 2004, Michael Codish and Aart Middeldorp, eds., Technical Report AIB-2004-07, ISSN 0935-3232, RWTH Aachen, June 2004.
  
  Abstract We investigate modularity of termination of left-linear rewrite systems in the constructor sharing case. More precisely, we study cases where both involved system are left-linear, as well as other related cases where the conditions on the involved systems systems (like left-linearity) are not the same. Several tempting approaches to generalize the well-known deep modularity results of \cite{ToKlBa89,ToKlBa95}, \cite{Ma95b,SSMaPa95} are discussed and falsified by counterexamples. By a thorough analysis of the crucial notions of uniquely collapsing and consistency w.r.t. reduction and of the role of left-linearity in collapsing and, more generally, \emph{shared symbol lifting} reductions we finally show how to generalize certain modularity results for termination in the case of disjoint unions to combinations of constructor sharing systems. The problem in the symmetric case (where both systems are left-linear) remains open, whereas we are able to extend a couple of asymmetric modularity results from \cite{Gr98} to combinations of constructor sharing systems.
  
  
  
• Bernhard Gramlich and Salvador Lucas
  Modular Context-Sensitive Algebraic Specifications
  Proc. 17th International Workshop on Algebraic Development Techniques - Extended Abstracts (WADT 2004), Barcelona, Spain, March 27-30, 2004, ed. Peter D. Mosses, pp. 20-22, 2004.
  
  Abstract Context-sensitivity in algebraic specifications is an interesting approach for bridging the gap between the purely logical and semantic nature of such systems and (certain problems in) their operational realization and implementation. Context-sensitive algebraic specifications are obtained by enriching ordinary algebraic specifications with additional syntactical (context) information that turns out to be very useful in transforming these specifications into executable prototypes or implementations satisfying usually desired properties. Here we investigate modular aspects of such context-sensitive algebraic specifications and computations in the framework of context-sensitive equational reasoning and rewriting. In particular, we study the modularity behaviour of context-sensitive term rewriting systems w.r.t confluence and related uniqueness properties. We show how to extend various modularity results known from (unrestricted) term rewriting systems to this more general setting, and how to cope with the additional complications caused by context-sensitivity.
  
  
  
• María Alpuente, Santiago Escobar, Bernhard Gramlich and Salvador Lucas
  Improving On-demand Strategy Annotations
  Proc. 9th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2002), Tbilisi, Georgia, October 14-18, 2002, eds. Mattias Baaz and Andrei Voronkov, LNAI 2514, Springer-Verlag, 2002.
  
  Abstract In functional languages such as OBJ*, CafeOBJ, and Maude, symbols are given strategy annotations which specify (the order in) which subterms are evaluated. Syntactically, they are given either as lists of natural numbers or as lists of integers associated to function symbols whose (absolute) values refer to the arguments of the corresponding symbol. A positive index enables the evaluation of an argument whereas a negative index means "evaluate on-demand". While strategy annotations containing only natural numbers have been implemented and received some recent investigation endeavor (regarding, e.g., termination and completeness), fully general annotations (also called on-demand strategy annotations), which have been proposed to support laziness in OBJ-like languages, are disappointingly under-explored to date. In this paper, we first point out a number of problems of current proposals for handling on-demand strategy annotations. Then, we propose a solution to these problems which is based on a suitable extension of the E-evaluation strategy of OBJ-like languages (that only considers annotations given as natural numbers) to on-demand strategy annotations. Our strategy incorporates a better treatment of demandness and also exhibits good computational properties; in particular, we show how to use it for computing (head-)normal forms. We also introduce a transformation for proving termination of the new evaluation strategy by using standard techniques.
  
  
  
• Bernhard Gramlich and Salvador Lucas
  Modular Termination of Context-Sensitive Rewriting
  Proc. 4th International Conference on Principles and Practice of Declarative Programming (PPDP 2002), Pittsburgh, PA, USA, October 6-8, 2002, ed. Claude Kirchner, ACM Press, 2002.
  
  Abstract Context-sensitive rewriting (CSR) has recently emerged as an interesting and flexible paradigm that provides a bridge between the abstract world of general rewriting and the (more) applied setting of declarative specification and programming languages such as OBJ*, CafeOBJ, ELAN, and Maude. A natural approach to study properties of programs written in these languages is to model them as context-sensitive rewriting systems. Here we are especially interested in proving termination of such systems, and thereby providing methods to establish termination of e.g. OBJ* programs. For proving termination of context-sensitive rewriting, there exist a few transformation methods, that reduce the problem to termination of a transformed ordinary term rewriting system (TRS). These transformations, however, have some serious drawbacks. In particular, most of them do not seem to support a modular analysis of the termination problem. In this paper we will show that a substantial part of the well-known theory of modular term rewriting can be extended to CSR, via a thorough analysis of the additional complications arising from context-sensitivity. More precisely, we will mainly concentrate on termination (properties). The obtained modularity results correspond nicely to the fact that in the above languages the modular design of programs and specifications is explicitly promoted, since it can now also be complemented by modular analysis techniques.
  
  
  
• Bernhard Gramlich and Salvador Lucas
  Simple Termination of Context-Sensitive Rewriting
  Proc. 3rd ACM Sigplan Workshop on Rule-based Programming (RULE 2002), Pittsburgh, PA, USA, October 5, 2002, eds. Bernd Fischer and Eelco Visser, ACM Press, 2002.
  
  Abstract Simple termination (or its algebraic counterpart, the simplification orderings) is the (often indirect) basis of most existing automatic techniques for proving termination of rule-based programs (e.g., Knuth-Bendix, polynomial, or recursive path orderings, but also DP-simple termination, etc.). An interesting framework for such programs is context-sensitive rewriting (CSR) that provides a bridge between the abstract world of general rewriting and the (more) applied setting of declarative specification and programming languages (e.g., OBJ*, CafeOBJ, ELAN, and Maude). In these languages, certain replacement restrictions can be specified in programs by the so-called strategy annotations. They may significantly improve the computational properties of programs, especially regarding their termination behaviour. Context-sensitive rewriting techniques (in particular, the methods for proving termination of CSR) have been proved useful for analyzing the properties of these programs. This entails the need to provide implementable methods for proving termination of CSR. Simplification orderings (corresponding to the notion of simple termination) which are well-known in term rewriting (and have nice properties) are, then, natural candidates for such an attempt. In this paper we introduce and investigate a corresponding notion of simple termination of CSR. We prove that our notion actually provides a unifying framework for proving termination of CSR by using standard simplification orderings via the existing (transformational) methods, and also covers CSRPO, a very recent proposal that extends the recursive path ordering (RPO) (a well-known simplification ordering) to context-sensitive terms. We also introduce polynomial orderings for dealing with (simple) termination of CSR. Finally, we also give criteria for the modularity of simple termination, for the case of disjoint unions as well as for constructor-sharing context-sensitive rewrite systems.
  
  
  
• Bernhard Gramlich and Reinhard Pichler
  Algorithmic Aspects of Herbrand Models Represented by Ground Atoms with Ground Equations
  Proc. 18th Int. Conference on Automated Deduction (CADE 2002), Copenhagen, Denmark, July 2002, LNAI 2392, pp. 241-259, ed. A. Voronkov, Springer-Verlag, 2002.
  
  Abstract Automated model building has evolved as an important subdiscipline of automated deduction over the past decade. One crucial issue in automated model building is the selection of an appropriate (finite) representation of (in general infinite) models. Quite a few such formalisms have been proposed in the literature. In this paper, we concentrate on the representation of Herbrand models by ground atoms with ground equations (GAE-models), introduced recently by Fermüller/Leitsch. For the actual work with any model representation, efficient algorithms for two decision problems are required, namely: The clause evaluation problem (i.e.: Given a clause C and a representation M of a model, does C evaluate to "true" in this model?) and the model equivalence problem (i.e.: Given two representations M1 and M2, do they represent the same model?). Previously published algorithms for these two problems in case of GAE-models require exponential time. We prove that the clause evaluation problem is indeed intractable (that is, coNP-complete), whereas the model equivalence problem can be solved in polynomial time. Moreover, we show how our new algorithm for the model equivalence problem can be used to transform an arbitrary GAE-model into an equivalent one with better computational properties.
  
  
  
• Bernhard Gramlich
  Knowledge Based Simplification of Termination Proofs
  Proc. 5th Int. Workshop on Termination (WST 2001) - Extended Abstracts, Utrecht, The Netherlands, May 2001, ed. N. Dershowitz, pp. 19-21, 2001.
  
  
  
• Bernhard Gramlich
  Simplifying Termination Proofs for Rewrite Systems by Preprocessing
  Proc. 2nd Int. Conf. on Principles and Practice of Declarative Programming (PPDP 2000), Montreal, Canada, September 2000, eds. M. Gabrielli & F. Pfenning, pp. 139-150, ACM press, 2000.
  
  Abstract We prove some new results that simplify termination proofs for non-overlapping term rewriting systems. The first one is a refined modularity result (for not necessarily disjoint systems). The second, more important one, gives conditions under which the simplification of right-hand sides (using rules of the original system) is a sound preprocessing step, in the sense that termination of the original system is equivalent to termination of the simplified system, and that the equational theory is preserved. The proofs are based on some powerful structural properties known for non-overlapping systems. Finally, we show how to extend these results, in particular, to the case of conditional rewrite systems where we additionally treat simplification of conditions of rules. The presented results provide the theoretical basis for sound (and automatic) preprocessing steps when proving termination of (possibly conditional) non-overlapping rewrite systems and and equational programs defined by such systems.
  
  
  
• Bernhard Gramlich
  On the (Non-)Existence of Least Fixed Points in Conditional Equational Logic and Conditional Rewriting
  Proc. 2nd Int. Workshop on Fixed Points in Computer Science (FICS 2000) - Extended Abstracts, Paris, France, July 2000, pp. 38-40, ed. I. Guessarian, July 2000.
  
  Abstract We investigate problems with basic definitions in conditional equational logic and conditional term rewriting that are closely related to (definitions via) least fixed point constructions. In particular, we discuss problems with non-well-defined (equality / rewrite) relations that are due to the non-existence of certain least fixed points, and modified approaches to guarantee the existence of such fixed points.
  
  
  
• Bernhard Gramlich
  Extending First-Order Unification by Tractable Second-Order Features
  Proc. 3rd Int. Workshop on First-Order Theorem Proving (FTP 2000), St Andrews, Scotland, July 2000, pp. 122-133, eds. P. Baumgartner & H. Zhang, Fachbericht Informatik 5/2000, Universität Koblenz, July 2000.
  
  Abstract We present a new approach for solving certain infinite sets of first order unification problems represented by term schemes. Within the framework of second-order equational logic solving such scheme unification problems amounts exactly to solving (variable-)restricted unification problems. Finally, we show how this approach yields a generic solution technique for infinitely many ordinary first-order unification problems.
  
  
  
• Bernhard Gramlich
  Strategic Aspects in Inductive Theorem Proving and Proof Engineering (Extended Abstract)
  Proc. FLoC'99 Workshop on the Automation of Proof by Mathematical Induction (IND-WS'99), Trento, Italy, pp. 25-28, July 1999.
  
  
  
• Bernhard Gramlich
  On Some Abstract Termination Criteria
  Proc. 4th Int. Workshop on Termination (WST'99) - Abstracts, Dagstuhl, Germany, May 1999.
  
  
  
• Bernhard Gramlich
  On (Un)Sound Simplifications of Equational Theories
  Proc. 12th Int. Workshop on Unification (UNIF'98), Rome, Italy, ed. Marisa Venturini Zilli et al., Research Report SI-98/8, June 1998.
  
  
  
• Bernhard Gramlich
  Modular Aspects of Rewrite-Based Specifications
  Proc. 12th Int. Workshop on Algebraic Development Techniques - Selected Papers (WADT'97), Tarquinia, Italy, ed. F. Parisi-Presicce, LNCS 1376, pp.253-268, 1998.
  
  Abstract We investigate modular properties of term rewriting systems, the basic operational formalism for equational specifications. First we study sufficient conditions for the preservation of the termination property under disjoint (and more general) combinations of term rewriting systems. By means of a refined analysis of existing approaches we show how to prove several new asymmetric preservation results. For this purpose we introduce two interesting new properties of term rewriting systems related to collapsing reductions: uniquely collapsing and collapsing confluent. We discuss these properties w.r.t. well-known confluence, consistency and normal form properties, and show that they are modular for left-linear systems, but not in general.
  
  
  
• Bernhard Gramlich
  Design Issues for Inductive Theorem Proving Systems
  CADE-14 Workshop on Automated Induction Theorem Proving (IND-WS'97), Townsville, North Queensland, Australia, July 1997.
  
  
  
• Bernhard Gramlich
  A Refined Analysis for Termination of Combined Rewrite Systems
  Proc. 3rd Int. Workshop on Termination (IWT'97) - Extended Abstracts, Utrecht The Netherlands,
  pp. 4-5, May 1997.
  
  
  
• Bernhard Gramlich
  On Proving Termination by Innermost Termination
  Proc. 7th Int. Conf. on Rewriting Techniques and Applications (RTA'96), New Brunswick, NJ, USA,
  ed. H. Ganzinger, LNCS 1103, pp. 97-107, 1996.
  
  Abstract We present a new approach for proving termination of rewrite systems by innermost termination. From the resulting abstract criterion we derive concrete conditions, based on critical peak properties, under which innermost termination implies termination (and confluence). Finally, we show how to apply the main results for providing new sufficient conditions for the modularity of termination.
  
  
  
• Bernhard Gramlich and Claus-Peter Wirth
  Confluence of Terminating Conditional Rewrite Systems Revisited
  Proc. 7th Int. Conf. on Rewriting Techniques and Applications (RTA'96), New Brunswick, NJ, USA,
  ed. H. Ganzinger, LNCS 1103, pp. 245-259, 1996.
  
  Abstract We present a new and powerful criterion for confluence of terminating (terms in) join conditional term rewriting systems. This criterion is based on a certain joinability property for shared parallel critical peaks and does neither require the systems to be decreasing nor left-linear nor normal, but only terminating.
  
  
  
• Bernhard Gramlich
  Confluence without Termination via Parallel Critical Pairs
  Proc. 21st Int. Coll. on Trees in Algebra and Programming (CAAP'96), Linköping, Sweden,
  ed. H. Kirchner, LNCS 1059, pp. 211-225, 1996.
  
  Abstract We present a new criterion for confluence of (possibly) non-terminating left-linear term rewriting systems. The criterion is based on certain strong joinability properties of parallel critical pairs. We show how this criterion relates to other well-known results, consider some special cases and discuss some possible extensions.
  
  
  
• Bernhard Gramlich
  Conditional Rewrite Systems under Signature Extensions: Some Counterexamples
  Proc. 10th Int. Workshop on Unification (UNIF'96), Herrsching (Munich), Germany,
  eds. K.U. Schulz & S. Kepser, CIS-Report 96-91, pp. 45-50, 1996.
  
  Abstract Here we are interested in the question whether certain weak and strong termination and confluence properties of conditional term rewriting systems (CTRSs) are preserved under signature extensions.
  
  
  
• Bernhard Gramlich
  On Evaluation Criteria for Inductive Theorem Proving Systems
  Proc. 4th Int. Workshop on the Automation of Proof by Mathematical Induction (IND-WS'95), Dagstuhl-Seminar-Report, Dagstuhl, Germany, July 1995.
  ed. Alan Bundy, pp. 14-15, June 1992.
  
  
  
• Bernhard Gramlich
  Termination by Divide and Conquer: Some New Preservation Results
  Proc. 2nd Int. Workshop on Termination (IWT'95) - Extended Abstracts, La Bresse, France
  pp. 4-5, May 1995.
  
  
  
• Bernhard Gramlich
  On Termination and Confluence of Conditional Rewrite Systems
  Proc. 4th Int. Workshop on Conditional and Typed Rewriting Systems (CTRS'94), Jerusalem, Israel,
  eds. N. Dershowitz & N. Lindenstrauss, LNCS 968, pp. 166-185, 1995.
  
  Abstract We consider the problem of verifying confluence and termination of conditional term rewriting systems. Recently we have obtained some interesting results for unconditional term rewriting systems (TRSs) which are non-overlapping or, more generally, locally confluent overlay systems. These results provide sufficient criteria for termination plus confluence in terms of restricted termination and confluence properties (Gramlich \cite{Gr94e}). Here we generalize our approach to the conditional case and show how to solve the additional complications due to the presence of conditions in the rules. Our main result can be stated as follows: Any conditional TRS (CTRS) which is an innermost terminating overlay system such that all (conditional) critical pairs are joinable is complete, i.e., terminating and confluent.
  
  
  
• Bernhard Gramlich
  On Modularity of Termination and Confluence Properties of Conditional Rewrite Systems
  Proc. 4th Int. Conf. on Algebraic and Logic Programming (ALP'94), Madrid, Spain,
  eds. G. Levi & M. Rodrigíguez-Artalejo, LNCS 850, pp. 186-203, 1994.
  
  Abstract We investigate the modularity behaviour of termination and confluence properties of conditional term rewriting systems. In particular, we show how to obtain sufficient conditions for the modularity of weak termination, weak innermost termination, (strong) innermost termination, (strong) termination, confluence and completeness of conditional rewrite systems.
  
  
  
• Claus-Peter Wirth and Bernhard Gramlich
  On Notions of Inductive Validity for First-Order Equational Clauses
  Proc. 12th Int. Conf. on Automated Deduction (CADE'94), Nancy, France,
  ed. A. Bundy, LNAI 814, pp. 162-176, 1994.
  
  Abstract We define and discuss various conceivable notions of inductive validity for first-order equational clauses. This is done within the framework of constructor-based positive/negative conditional equational specifications which permits to treat negation and incomplete function definitions in an adequate and natural fashion. Moreover, we show that under some reasonable assumptions all these notions are monotonic \wrt\ consistent extension, in contrast to the case of inductive validity for initial semantics (of unconditional or positive conditional equations). In particular from a practical point of view, this monotonicity property is crucial since it allows for an incremental construction process of complex specifications where consistent extensions of specifications cannot destroy the validity of (already proved) inductive properties. Finally we show how various notions of inductive validity in the literature fit in or are related to our classification.
  
  
  
• Bernhard Gramlich
  Experiences with the Development, Maintenance and Enhancement of UNICOM
  Proc. CADE-12 Workshop on Correctness and Metatheoretic Extensibility of Automated Reasoning Systems, Nancy, France,
  eds. D. Basin, F. Giunchiglia and M. Kaufmann, pp. 42-43, 1994.
  
  
  
• Aart Middeldorp and Bernhard Gramlich
  Simple Termination is Difficult
  Proc. 5th Int. Conf. on Rewriting Techniques and Applications (RTA'93), Montreal, Canada,
  ed. C. Kirchner, LNCS 690, pp. 228-242, 1993.
  
  Abstract A terminating term rewriting system is called simply terminating if its termination can be shown by means of a simplification ordering, an ordering with the property that a term is always bigger than its proper subterms. Almost all methods for proving termination yield, when applicable, simple termination. We show that simple termination is an undecidable property, even for one-rule systems. This contradicts a result by Jouannaud and Kirchner. The proof is based on the ingenious construction of Dauchet who showed the undecidability of termination for one-rule systems.
  
  
  
• Bernhard Gramlich
  Termination Properties of Non-Orthogonal Term Rewriting Systems
  Proc. 1st Int. Workshop on Termination (IWT'93) - Abstracts, St. Andrews, Scotland, May 1993.
  
  
  
• Bernhard Gramlich
  Sufficient Conditions for Modular Termination of Conditional Term Rewriting Systems
  Proc. 3rd Int. Workshop on Conditional Term rewriting Systems (CTRS'92), Pont-à-Mousson, France,
  eds. M. Rusinowitch & J.-L. Rémy, LNCS 656, pp. 128-142, 1993.
  
  Abstract Recently we have shown the following abstract result for unconditional term rewriting systems (TRSs). Whenever the disjoint union $\dsum$ of two (finite) terminating TRSs $\reins$, $\rzwei$ is non-terminating, then one of the systems, say $\reins$, enjoys an interesting property, namely it is not termination preserving under non-deterministic collapses, i.e. \mbox{$\reins \oplus \{ G(x,y) \ra x, G(x,y) \ra y \}$} is non-terminating, and the other system $\rzwei$ is collapsing, i.e. contains a rule with a variable right hand side. This result generalizes known sufficient syntactical criteria for modular termination of rewriting. Here we extend this result and derived sufficient criteria for modularity of termination to the case of conditional term rewriting systems (CTRSs). Moreover we relate various definitions of notions related to termination of CTRSs to each other and discuss some subtleties and problems concerning extra variables in the rules.
  
  
  
• Claus-Peter Wirth and Bernhard Gramlich
  A Constructor-Based Approach for Positive/Negative Conditional Equational Specifications
  Proc. 3rd Int. Workshop on Conditional Term rewriting Systems (CTRS'92), Pont-à-Mousson, France,
  eds. M. Rusinowitch & J.-L. Rémy, LNCS 656, pp. 198-212, 1993.
  
  Abstract We present a constructor-based approach for assigning appropriate semantics to algebraic specifications given by finite sets of positive/negative-conditional equations. Under the assumption of confluence of the reduction relation we define, the factor algebra of the ground term algebra modulo the congruence of this reduction relation is a minimal model which is (beyond that) the minimum of all models that do not identify more constructor ground terms than necessary.
  
  
  
• Bernhard Gramlich
  Generalized Sufficient Conditions for Modular Termination of Rewriting
  Proc. 3rd Int. Conf. on Algebraic and Logic Programming (ALP'92), Volterra, Italy,
  eds. H. Kirchner & G. Levi, LNCS 632, pp. 53-68, 1992.
  
  Abstract Modular properties of term rewriting systems, i.e. properties which are preserved under disjoint unions, have attracted an increasing attention within the last few years. Whereas confluence is modular this does not hold true in general for termination. By means of a careful analysis of potential counterexamples we prove the following abstract result. Whenever the disjoint union $\dsum$ of two (finite) terminating term rewriting systems $\reins$, $\rzwei$ is non-terminating, then one of the systems, say $\reins$, enjoys an interesting (undecidable) property, namely it is not termination preserving under non-deterministic collapses, i.e. \mbox{$\reins \oplus \{ G(x,y) \ra x, G(x,y) \ra y \}$} is non-terminating, and the other system $\rzwei$ is collapsing, i.e. contains a rule with a variable right hand side. This result generalizes known sufficient syntactical criteria for modular termination of rewriting and provides the basis for a couple of derived modularity results. Furthermore, we prove that the minimal rank of potential counterexamples in disjoint unions may be arbitrarily high which shows that interaction of systems in such disjoint unions may be very subtle. Finally, extensions and generalizations of our main results in various directions are discussed and sketched.
  
  
  
• Bernhard Gramlich
  Relating Innermost, Weak, Uniform and Modular Termination of Term Rewriting Systems
  Proc. 3rd Int. Conf. on Logic Programming and Automated Reasoning (LPAR'92), St. Petersburg, Russia,
  ed. A. Voronkov, LNAI 624, pp. 285-296, 1992.
  
  Abstract Term rewriting systems play an important role in various areas, e.g. in abstract data type specifications, for automated theorem proving and as a basic computation model for functional programming languages. In theory and practice, one of the most important properties of term rewriting systems is the strong normalization or (finite or uniform) termination property which is undecidable in general. For ensuring this property many sufficient criteria and methods based on well-founded term orderings have been developed. In this paper we follow another line of research and study restricted termination properties of term rewriting systems, in particular weak termination and innermost termination, and their interrelation. New criteria are provided which are sufficient for the equivalence of innermost/weak termination and uniform termination of term rewriting systems. Using these basic results we are also able to prove some new results about modular termination of rewriting. In particular, we show that termination is modular for locally confluent overlay systems. As an easy consequence this result also entails a simplified proof of the fact that completeness is a decomposable property of so-called constructor systems. Interestingly, these modularity results are obtained by means of a proof technique which itself constitutes a {\em modular} approach.
  
  
  
• Bernhard Gramlich
  Inductive Theorem Proving Based on Rewriting and Completion Techniques
  Proc. 1st Int. Workshop On the Automation of Inductive Proof (IND-WS'92) - Abstracts, held in conjunction with CADE-11, Saratoga Springs, NY, USA
  ed. Alan Bundy, pp. 14-15, June 1992.
  
  
  
• Bernhard Gramlich
  Completion Based Inductive Theorem Proving: An Abstract Framework and its Applications
  Proc. 9th European Conf. on Artificial Intelligence (ECAI'90), Stockholm, Sweden,
  ed. L.C. Aiello, Pitman Publishing, London, pp. 314-319, 1990.
  
  Abstract We present an abstract framework for completion based inductive theorem proving in equational theories and show how the problem of proving inductive validity of equational conjectures can be considered from a "positive" or "negative" point of view. The general framework leads to a better understanding of completion based inductive theorem proving and enables us to obtain generalized characterizations of inductive validity. Within the "positive" approach we demonstrate how to prove inductive theorems for the case that the base system is terminating but not necessarily ground confluent. Moreover, we classify and discuss possible refinements and optimizations of completion based inductive theorem proving. This yields a good basis for incorporating AI techniques into the method. Finally we summarize encouraging experiments performed with an implementation of the method.
  
  
  
• Bernhard Gramlich
  UNICOM: A Refined Completion Based Inductive Theorem Prover
  Proc. 10th Int. Conf. on Automated Deduction (CADE'90), Kaiserslautern, Germany,
  ed. M.E. Stickel, LNAI 449, pp. 655-656, 1990.
  
  Abstract UNICOM (UNfailing Inductive COMletion) is a toolbox for investigating equationally defined hierarchically structured many-sorted algebraic specifications. We summarize its main components, theoretical foundations, characteristic features and experiences with the system.
  
  
  
• Bernhard Gramlich
  Unification of Term Schemes
  Proc. 2nd Int. Workshop on Unification - Extended Abstracts (UNIF'89), Lambrecht, Germany,
  eds. H.-J. Bürckert & W. Nutt, 1989.
  
  Abstract see SR-88-18
  
  
  
• Bernhard Gramlich
  Efficient AC-Matching using Constraint Propagation
  Proc. 2nd Int. Workshop on Unification - Abstracts (UNIF'88), Val d'Ajol, France,
  eds. C. Kirchner & G. Smolka, Rapport Interne No. 89-R-38, CRIN, 1988.
  
  Abstract see SR-88-15
  
  
  
• Jürgen Avenhaus, Richard Göbel, Bernhard Gramlich, Klaus Madlener and Joachim Steinbach
  TRSPEC: A Term Rewriting Based System for Algebraic Specifications
  Proc. 1st Int. Workshop on Conditional Term Rewriting Systems (CTRS'97), Orsay, France,
  eds. S. Kaplan & J.-P. Jouannaud, LNCS 308, pp. 245-248, 1988.
  
  Abstract Term rewriting systems and methods can be used for functional programming and as a technology for program verification using the same formalism in both cases. The TRSPEC system provides tools for specifying functions by term rewriting systems and for proving (equational) properties of these functions in the corresponding initial algebra by a specialized Knuth-Bendix completion procedure. Various checks of abstract specifications as well as rapid prototyping by means of a compilation into executable specifications are possible. One of the main goals of the system is to provide a suitable basis for performing experiments in order to validate new theoretical results and approaches and to identify the main problems and limits of rewriting techniques for program verification from a practical point of view.
  
  

Journal Papers

• Bernhard Gramlich and Felix Schernhammer
  Termination of Rewriting with and Automated Synthesis of Forbidden Patterns
  Final Proc. 1st International Workshop on Strategies in Rewriting, Proving, and Programming (IWS 2010), Electronic Proceedings in Theoretical Computer Science, Volume 44, pp. 35-50, Hélène Kirchner and César Muñoz, eds., December 2010.
  abstract, bibtex, pdf
  
  Abstract We introduce a modified version of the well-known dependency pair framework that is suitable for the termination analysis of rewriting under forbidden pattern restrictions. By attaching contexts to dependency pairs that represent the calling contexts of the corresponding recursive function calls, it is possible to incorporate the forbidden pattern restrictions in the (adapted) notion of dependency pair chains, thus yielding a sound and complete approach to termination analysis. Building upon this contextual dependency pair framework we introduce a DP processor that simplifies problems by analyzing the contextual information of the dependency pairs. Moreover, we show how this processor can be used to synthesize forbidden patterns suitable for a given TRS on-the-fly during the termination analysis.
  
  
• Bernhard Gramlich and Felix Schernhammer
  Extending Context-Sensitivity in Term Rewriting
  Final Proc. 9th International Workshop on Reduction Strategies in Rewriting and Programming (WRS 2009), Electronic Proceedings in Theoretical Computer Science, Volume 15, Maribel Fernandez, ed., pp. 56-68, January 26, 2010.
  
  Abstract We propose a generalized version of context-sensitivity in term rewriting based on the notion of "forbidden patterns". The basic idea is that a rewrite step should be forbidden if the redex to be contracted has a certain shape and appears in a certain context. This shape and context is expressed through forbidden patterns. In particular we analyze the relationships among this novel approach and the commonly used notion of context-sensitivity in term rewriting, as well as the feasibility of rewriting with forbidden patterns from a computational point of view. The latter feasibility is characterized by demanding that restricting a rewrite relation yields an improved termination behaviour while still being powerful enough to compute meaningful results. Sufficient criteria for both kinds of properties in certain classes of rewrite systems with forbidden patterns are presented.
  
  
• María Alpuente, Santiago Escobar, Bernhard Gramlich and Salvador Lucas
  On-demand Strategy Annotations Revisited: An Improved On-Demand Evaluation Strategy
  Theoretical Computer Science, Volume 411, Issue 2, Pages 504-541, 2 January 2010.
  
  Abstract In functional languages such as OBJ*, CafeOBJ, and Maude, symbols are given strategy annotations that specify (the order in) which subterms are evaluated. Syntactically, strategy annotations are given either as lists of natural numbers or as lists of integers associated to function symbols whose (absolute) values refer to the arguments of the corresponding symbol. A positive index prescribes the evaluation of an argument whereas a negative index means ``evaluation on-demand''. These on-demand indices have been proposed to support laziness in OBJ-like languages. While strategy annotations containing only natural numbers have been implemented and investigated to some extent (regarding, e.g., termination, confluence, and completeness), fully general annotations (including positive and negative indices) are disappointingly under-explored to date. In this paper, we first point out a number of problems of current proposals for handling on-demand strategy annotations. Then, we propose a solution to these problems by keeping an accurate track of annotations along the evaluation sequences. We formalize this solution as a suitable extension of the evaluation strategy of OBJ-like languages (which only consider annotations given as natural numbers) to on-demand strategy annotations. Our on-demand evaluation strategy (ode) overcomes the drawbacks of previous proposals and also has better computational properties. For instance, we show how to use this strategy for computing (head-)normal forms. We also introduce a transformation which allows us to prove termination of the new evaluation strategy by using standard rewriting techniques. Finally, we present two interpreters of the new strategy together with some encouraging experiments which demonstrate the usefulness of our approach.
  
  
  
• Felix Schernhammer and Bernhard Gramlich
  Characterizing and Proving Operational Termination of Deterministic Conditional Term Rewriting Systems
  Journal of Logic and Algebraic Programming, Volume 79, Issue 7, Pages 659-688, Revised selected papers of NWPT 2008, Tarmo Uustalu and Jüri Vain, editors, October 2010.
  
  Abstract We investigate the practically crucial property of operational termination of deterministic conditional term rewriting systems (DCTRSs), an important declarative programming paradigm. We show that operational termination can be equivalently characterized by the newly introduced notion of context-sensitive quasi-reductivity. Based on this characterization and an unraveling transformation of DCTRSs into context-sensitive (unconditional) rewrite systems (CSRSs), context-sensitive quasi-reductivity of a DCTRS is shown to be equivalent to termination of the resulting CSRS on original terms. This result enables both proving and disproving operational termination of given DCTRSs via transformation into CSRSs. A concrete procedure for this restricted termination analysis (on original terms) is proposed and encouraging benchmarks obtained by the termination tool VMTL, that utilizes this approach, are presented. Finally, we show that the context-sensitive unraveling transformation is sound and complete for collapse-extended termination, thus solving an open problem of [Duran et al. 2008].
  
  
  
• Felix Schernhammer and Bernhard Gramlich
  Termination of Lazy Rewriting Revisited
  Electronic Notes in Theoretical Computer Science (ENTCS), Volume 204, Final Proc. of WRS 2007 - 7th International Workshop on Reduction Strategies in Rewriting and Programming, Jürgen Giesl, ed., pages 35-51, April 2008.
  
  Abstract Lazy rewriting is a proper restriction of term rewriting that dynamically restricts the reduction of certain arguments of functions in order to obtain termination. In contrast to context-sensitive rewriting reductions at such argument positions are not completely forbidden but delayed. Based on the observation that the only existing (non-trivial) approach to prove termination of such lazy rewrite systems is flawed, we develop a modified approach for transforming lazy rewrite systems into context-sensitive ones that is sound and complete with respect to termination. First experimental results with this transformation based technique are encouraging.
  
  
  
• María Alpuente, Bernhard Gramlich and Alicia Villanueva
  A Framework for Timed Concurrent Constraint Programming with External Functions
  Electronic Notes in Theoretical Computer Science, Volume 188 (Pages 1-156), Proc. 6th Spanish Conference on Programming and Languages (PROLE 2006), Sitges, Barcelona, Spain, Paqui Lucio and Fernando Orejas, eds., pages 143-155, July 2007.
  
  Abstract The timed concurrent constraint programming language (tccp in short) was introduced for modeling reactive systems. This language allows one to model in a very intuitive way typical ingredients of these systems such as timeouts, preemptions, etc. However, there is no natural way for modeling other desirable features such as functional computations, for example for calculating arithmetic results. In fact, although it is certainly possible to implement such kind of operations, each single step of the computation takes time in tccp, and avoiding interferences with the intended overall behavior of the (reactive) system is quite involved. In this paper, we propose an extension of tccp for modeling instantaneous computations which improves the expressiveness of the language, in the sense that operations that are cumbersome to implement in pure tccp, are executed by calling an efficient, external functional engine, while the tccp programmer can focus on the pure, and usually more complex, reactive part of the system. We also describe a case study which motivates the work, and discuss how the new capability presented here can also be used as a new tool for developers from the verification point of view.

  Keywords: Timed Concurrent Constraint language; Functional features; Case study

  
  
• Bernhard Gramlich
  Strategic Issues, Problems and Challenges in Inductive Theorem Proving
  Electronic Notes in Theoretical Computer Science, Volume 125, Issue 2 (Proc. 5th International Workshop on Strategies in Automated Deduction, Strategies 2004 - Selected Papers, M.P. Bonacina and T. Boy de la Tour, eds.), Elsevier, pp. 5-43, March 2005.
  
  Abstract (Automated) Inductive Theorem Proving (ITP) is a challenging field in automated reasoning and theorem proving. Typically, (Automated) Theorem Proving (TP) refers to methods, techniques and tools for automatically proving \emph{general} (most often first-order) theorems. Nowadays, the field of TP has reached a certain degree of maturity and powerful TP systems are widely available and used. The situation with ITP is strikingly different, in the sense that proving inductive theorems in an essentially automatic way still is a very challenging task, even for the most advanced existing ITP systems. Both in general TP and in ITP, strategies for guiding the proof search process are of fundamental importance, in automated as well as in interactive or mixed settings. In the paper we will analyze and discuss the most important strategic and proof search issues in ITP, compare ITP with TP, and argue why ITP is in a sense much more challenging. More generally, we will systematically isolate, investigate and classify the main problems and challenges in ITP w.r.t. automation, on different levels and from different points of views. Finally, based on this analysis we will present some theses about the state of the art in the field, possible criteria for what could be considered as substantial progress, and promising lines of research for the future, towards (more) automated ITP.
  
  
  
• Bernhard Gramlich
  On Interreduction of Semi-Complete Term Rewriting Systems
  Theoretical Computer Science 258(1-2), pp. 435-451, April 2001.
  
  Abstract For a complete, i.e., confluent and terminating term rewriting system (TRS) it is well-known that simplification (also called interreduction) into an equivalent canonical, i.e., complete and interreduced TRS is easily possible. This can be achieved by first normalizing all right-hand sides of the TRS and then deleting all rules with a reducible left-hand side. Here we investigate the logical and operational preservation properties of the same simplification operations for semi-complete, i.e., confluent and weakly terminating TRSs. Surprisingly, it turns out that for semi-complete TRSs these simplifications are neither operationally harmless nor logically correct: Semi-completeness may get lost and the induced equational theory need not be preserved. We also provide sufficient criteria for the preservation of semi-completeness and of the induced equational theory. In particular, we show that orthogonal TRSs enjoy all these preservation properties. In the general case, for a given semi-complete TRS an equivalent semi-canonical, i.e., semi-complete and interreduced system need not even exist.
  
  
  
• Bernhard Gramlich
  On Termination and Confluence Properties of Disjoint and Constructor-Sharing Conditional Rewrite Systems
  Theoretical Computer Science 165(1), pp. 97-131, 1996.
  
  Abstract We investigate the modularity behaviour of termination and confluence properties of (join) conditional term rewriting systems. We give counterexamples showing that the properties weak termination, weak innermost termination and (strong) innermost termination are not preserved in general under signature extensions. Then we develop sufficient conditions for the preservation of these properties under signature extensions, and more generally, for their modularity in the disjoint union case. This leads to new criteria for modularity of termination and completeness generalizing known results for unconditional systems. Finally, combining our analysis with recent related results on the preservation of semi-completeness, we show how to cover the (non-disjoint) case of combined conditional rewrite systems with shared constructors, too.
  
  
  
• Bernhard Gramlich
  Abstract Relations between Restricted Termination and Confluence Properties of Rewrite Systems
  Fundamentae Informaticae 24 (special issue on term rewriting systems), pp. 3-23, 1995.
  
  Abstract We investigate restricted termination and confluence properties of term rewriting systems, in particular weak termination, weak innermost termination, (strong) innermost termination, (strong) termination, and their interrelations. New criteria are provided which are sufficient for the equivalence of these properties. These criteria provide interesting possibilities to infer completeness, i.e. termination plus confluence, from restricted termination and confluence properties. Our main result states that any (strongly) innermost terminating, locally confluent overlay system is terminating, and hence confluent and complete. Using these basic results we are also able to prove some new results about modular termination of rewriting. In particular, we show that termination is modular for some classes of innermost terminating and locally confluent term rewriting systems, namely for non-overlapping and even for overlay systems. As an easy consequence this latter result also entails a simplified proof of the fact that completeness is a decomposable property of constructor systems. Similarly, a combined overlay system with shared constructors is complete if and only if its component sytems are complete overlay systems. Interestingly, these modularity results are obtained by means of a proof technique which itself constitutes a {\em modular} approach.
  
  
  
• Aart Middeldorp and Bernhard Gramlich
  Simple Termination is Difficult
  Applicable Algebra in Engineering, Communication and Computing, Volume 6, Number 2, pp. 115-128, March 1995.
  
  Abstract A terminating term rewriting system is called simply terminating if its termination can be shown by means of a simplification ordering, an ordering with the property that a term is always bigger than its proper subterms. Almost all methods for proving termination yield, when applicable, simple termination. We show that simple termination is an undecidable property, even for one-rule systems. This contradicts a result by Jouannaud and Kirchner. The proof is based on the ingenious construction of Dauchet who showed the undecidability of termination for one-rule systems. Our results may be summarized as follows: being simply terminating, (non-)self-embedding, and (non-)looping are undecidable properties of orthogonal, variable preserving, one-rule constructor systems.
  
  
  
• Bernhard Gramlich
  Generalized Sufficient Conditions for Modular Termination of Rewriting
  Applicable Algebra in Engineering, Communication and Computing, Volume 5, Numbers 3-4, pp. 131-158, May 1994.
  
  Abstract Modular properties of term rewriting systems, i.e. properties which are preserved under disjoint unions, have attracted an increasing attention within the last few years. Whereas confluence is modular this does not hold true in general for termination. By means of a careful analysis of potential counterexamples we prove the following abstract result. Whenever the disjoint union $\dsum$ of two (finitely branching) terminating term rewriting systems $\reins$, $\rzwei$ is non-terminating, then one of the systems, say $\reins$, enjoys an interesting (undecidable) property, namely it is not termination preserving under non-deterministic collapses, i.e. \mbox{$\reins \oplus \{ G(x,y) \ra x, G(x,y) \ra y \}$} is non-terminating, and the other system $\rzwei$ is collapsing, i.e. contains a rule with a variable right hand side. This result generalizes known sufficient criteria for modular termination of rewriting and provides the basis for a couple of derived modularity results. Furthermore, we prove that the minimal rank of potential counterexamples in disjoint unions may be arbitrarily high which shows that interaction of systems in such disjoint unions may be very subtle. Finally, extensions and generalizations of our main results in various directions are discussed. In particular, we show how to generalize the main results to some restricted form of non-disjoint combinations of term rewriting systems, namely for `combined systems with shared constructors'.
  
  
  
• Claus-Peter Wirth and Bernhard Gramlich
  A Constructor-Based Approach for Positive/Negative Conditional Equational Specifications
  Journal of Symbolic Computation 17, pp. 51-90, 1994.
  
  Abstract We study algebraic specifications given by finite sets \R\ of positive/negative-conditional equations (\ie\ universally quantified first-order implications with a single equation in the succedent and a conjunction of positive and negative (\ie\ negated) equations in the antecedent). The class of models of such a specification \R\ does not contain in general a minimum model in the sense that it can be mapped to any other model by some homomorphism. We present a constructor-based approach for assigning appropriate semantics to such specifications. We introduce two restrictions: firstly, for a condition to be fulfilled we require the evaluation values of the terms of the negative equations to be in the constructor sub-universe which contains the evaluation values of all constructor ground terms; secondly, we restrict the constructor equations to have ``Horn''-form and to be ``constructor-preserving''. A reduction relation for \R\ is defined, which allows to generalize the fundamental results for positive-conditional rewrite systems. This reduction relation is monotonic \wrt\ consistent extension of the specification, which is of practical importance as it allows for an incremental construction process of complex specifications without destroying reduction steps which were possible before. Under the assumption of confluence, the factor algebra of the term algebra modulo the congruence of the reduction relation is a minimal model which is (beyond that) the minimum of all models that do not identify more objects of the constructor sub-universe than necessary. We define several kinds of compatibility of \R\ with a reduction ordering for achieving decidability of reducibility, and present several criteria for the confluence of our reduction relation.
  
  
  
• Bernhard Gramlich
  A Note on a Parameterized Version of the Well-Founded Induction Principle
  Bulletin of the EATCS 52, pp. 274-278, 1994.
  
  Abstract The well-known and powerful proof principle by well-founded induction says that for verifying $\forall x: P(x)$ for some property $P$ it suffices to show $\forall x: [ [ \forall y < x : P(y) ] \imp P(x) ]$, provided $<$ is a well-founded partial ordering on the domain of interest. Here we investigate a more general formulation of this proof principle which allows for a kind of parameterized partial orderings $<_x$ which naturally arises in some cases. More precisely, we develop conditions under which the parameterized proof principle $\forall x: [ [ \forall y <_x x : P(y) ] \imp P(x) ]$ is sound in the sense that $\forall x: [ [ \forall y <_x x : P(y) ] \imp P(x) ] \imp \forall x: P(x)$ holds, and give counterexamples demonstrating that these conditions are indeed essential.
  
  

Books, Book Chapters and(Co-)Edited Works

• Bernhard Gramlich, ed.
  Frontiers of Combining Systems 5th International Workshop, FroCoS 2005, Vienna, Austria, September 19-21, 2005, Proceedings
  (Springer web page on LNAI 3717, Springer online web page for LNAI 3717)
  Lecture Notes in Computer Science, Vol. 3717, Springer, September 2005.
  
  Contents Final versions of all invited and regular contributions to FroCoS 2005.
  
  
• Bernhard Gramlich and Salvador Lucas, eds.
  Journal of Symbol Computation - Special issue on Reduction Strategies in Rewriting and Programming,
  Volume 40, Issue 1, pp. 745-903, Elsevier Science Publishers, July 2005.
  
  Contents Selected revised and extended papers from WRS 2001 and WRS 2002.
  
  
• Bernhard Gramlich and Salvador Lucas, eds.
  3rd International Workshop on Reduction Strategies in Rewriting and Programming (WRS 2003) -- Final Proceedings
  Electronic Notes in Theoretical Computer Science (ENTCS), Volume 86, Issue 4, Elsevier Science Publishers, 2003.
  
  Contents Final Proceedings of WRS 2003.
  
  
• Bernhard Gramlich and Salvador Lucas, eds.
  Proc. 3rd International Workshop on Reduction Strategies in Rewriting and Programming (WRS 2003)
  Valenica, Spain, June 8, 2003, Technical Report DSIC-II/14/03, Departamento de Sistemas Informáticos y Computación, Universidad Polit{\'e}cnica de Valencia, 2003.
  
  Contents Preliminary Proceedings of WRS 2003.
  
  
• Bernhard Gramlich and Salvador Lucas, eds.
  2nd International Workshop on Reduction Strategies in Rewriting and Programming (WRS 2002) -- Final Proceedings
  Electronic Notes in Theoretical Computer Science (ENTCS), Volume 70, Issue 6, Elsevier Science Publishers, 2002.
  
  Contents Final Proceedings of WRS 2002.
  
  
• Bernhard Gramlich and Salvador Lucas, eds.
  Proc. 2nd International Workshop on Reduction Strategies in Rewriting and Programming (WRS 2002)
  Copenhagen, Denmark, July 2002, Technical Report E1852-2002-02, Institut für Computersprachen, TU Wien, Austria, Verlag Berger, July 2002.
  
  Contents Preliminary Proceedings of WRS 2002.
  
  
• Maria Paola Bonacina and Bernhard Gramlich, eds.
  4th International Workshop on Strategies in Automated Deduction (STRATEGIES 2001) - Selected Papers
  Electronic Notes in Theoretical Computer Science (ENTCS), Volume 58, Issue 2, Elsevier Science Publishers, 2001.
  
  Contents Selected revised papers from STRATEGIES 2001.
  
  
• Bernhard Gramlich and Salvador Lucas, eds.
  1st International Workshop on Reduction Strategies in Rewriting and Programming (WRS 2001)
  Electronic Notes in Theoretical Computer Science (ENTCS), Volume 57, Elsevier Science Publishers, 2001.
  
  Contents ENTCS proceedings of WRS 2001.
  
  
• Maria Paola Bonacina and Bernhard Gramlich, eds.
  Proceedings 4th International Workshop on Strategies in Automated Deduction (STRATEGIES'01)
  118 pp., Siena, Italy, June 2001.
  
  Contents Workshop description, invited and accepted workshop papers.
  
  
• Bernhard Gramlich and Salvador Lucas, eds.
  Proceedings International Workshop on Reduction Strategies in Rewriting and Programming (WRS'01)
  Utrecht, The Netherlands, Technial Report SPUPV 2359, Servicio de Publicaciones - Universidad Politécnica de Valencia, 187 pp., May 2001.
  
  Contents Workshop description, invited and accepted workshop papers.
  
  
• Bernhard Gramlich, Hélène Kirchner and Frank Pfenning, eds.
  Strategies in Automated Deduction
  special issue of Annals of Mathematics and Artificial Intelligence, Volume 29, Issue 1/4, 257 pp., 2000, published in February 2001.
  
  Contents Selected papers on Strategies in Automated Deduction covering a variety of different topics.
  
  
• Bernhard Gramlich, Hélène Kirchner and Frank Pfenning, eds.
  Proceedings of FLoC'99 Workshop on Strategies in Automated Deduction (STRATEGIES'99)
  92 pp., Trento, Italy, July 1999.
  
  Contents Workshop description, workshop programme, abstracts of invited talks (with one full version) and extended versions of all regular contributions.
  
  
• Bernhard Gramlich and Frank Pfenning, eds.
  Proceedings of CADE-15 Workshop on Strategies in Automated Deduction
  74 pp., Trento, Italy, July 1998.
  
  Contents Workshop description, workshop programme, extended versions of all invited talks and regular contributions.
  
  
• Bernhard Gramlich and Hélène Kirchner, eds.
  Proceedings of CADE-14 Workshop on Strategies in Automated Deduction
  70 pp., Townsville, North Queensland, Australia, July 1997.
  
  Contents Workshop description, workshop programme, extended versions of all presented contributions, list of participants.
  
  
• Bernhard Gramlich and Jürgen Avenhaus
  Formal Specification and Verification of Equationally Defined Functional Programs with UNICOM
  in: Sichere Software, ed. H. Kersten, Hüthig Verlag, pp. 150-171, 1990.
  
  Abstract Functional programs can be specified by systems of equations in a very abstract and elegant fashion. The same holds for correctness properties which are needed for a formal verification of such programs. For an algorithmic treatment of equationally defined systems and problems powerful and theoretically well-established methods and tools are available, in particular term rewriting and completion techniques. In this paper we present a refined specialized adaptation of these techniques for dealing with verification problems. The practical realization of the corresponding theoretical results has lead to UNICOM, a software environment for (equation based) formal specification, verification and implementation of functional programs. The essential methodological foundations of UNICOM, its system structure and functionality are briefly surveyed. Furthermore experiences gained from numerous practical experiments are summarized. An extended non-trivial example is included for illustrating thhe kind of intelligent proof engineering which is required for the whole specification and verification process. Finally open problems and perspectives for future work are discussed, in particular concerning practical applicability of the underlying approach.
  
  

Theses

• Bernhard Gramlich
  Towards a Structure Theory of Term Rewriting
  Habilitation Thesis, 135 pp., Technische Universität Wien, September 1999.
  
  
• Bernhard Gramlich
  Termination and Confluence Properties of Structured Rewrite Systems
  PhD Thesis, 217 pp., Fachbereich Informatik, Universität Kaiserslautern, Germany, January 1996.
  
  Abstract Termination and confluence properties of term rewriting systems are of fundamental importance, both from a theoretical point of view and also concerning many practical applications in computer science and mathematics. We study structural aspects of termination and confluence properties of unconditional and conditional term rewriting systems. Two types of structural aspects are considered.
  First we investigate single rewrite systems. In a systematic manner we analyze how restricted versions of termination and confluence relate to each other and to general termination and confluence. In particular we focus on innermost rewriting and its properties. Various structural syntactic and semantic conditions are isolated which guarantee equivalence of general termination (and confluence) and weakened versions of these properties.
  In a second major part we consider structural aspects of combining systems. Here we investigate modularity and preservation properties of rewrite systems under various types of combinations. We survey known results in a unifying framework and develop new approaches, in particular for ensuring the preservation of termination under various types of combinations. The abstract results obtained provide a deeper insight into the striking phenomena that rewriting in combined systems may exhibit, and entail various interesting positive consequences.
  
  
  

National Conferences and Workshops

• María Alpuente, Bernhard Gramlich and Alicia Villanueva
  Timed Concurrent Constraint Programming with Instantaneous Computations
  Proc. 6th Spanish Conference on Programming and Computer Languages (PROLE 2006), Sitges, Spain,
  ed. Paqui Lucio, pp. 221-230, October 2006.
  
  Abstract The timed concurrent constraint programming language (tccp in short) was introduced for modeling reactive systems. This language allows one to model in a very intuitive way typical ingredients of these systems such as timeouts, preemptions, etc. However, there is no natural way for modeling other desirable features such as functional computations, for example for calculating arithmetic results. In fact, although it is certainly possible to implement such kind of operations, each single step takes time in tccp, and avoiding interferences with the intended overall behavior of the system is quite involved.
  In this paper, we propose an extension of tccp for modeling instantaneous computations which improves the expressiveness of the language, in the sense that operations that are cumbersome to implement in pure tccp, are executed by calling an efficient, external functional engine, while the tccp programmer can focus in the pure, and usually more complex, reactive part of the system. We also describe a case study which motivates the work, and discuss how the new capability presented here can also be used as a new tool for developers from the verification point of view.
  
  
  

Technical Reports

• Bernhard Gramlich and Klaus Györgyfalvay
  On Modularity of Termination Properties of Rewriting under Position-Based Strategies
  Technical Report, Theory and Logic Group, Institute of Computer Languages, TU Wien, Austria, 2012, forthcoming.
  
  
• Bernhard Gramlich and Klaus Györgyfalvay
  A Note on Minimal Counterexamples to Modularity of Termination
  Technical Report E1852-2012-02, Theory and Logic Group, Institute of Computer Languages, TU Wien, Austria, August 2012.
  
  
• Karl Gmeiner, Bernhard Gramlich and Felix Schernhammer
  On Soundness Conditions for Unraveling Deterministic Conditional Rewrite Systems
  Technical Report E1852-2012-01, Theory and Logic Group, Institute of Computer Languages, TU Wien, Austria, April 2012.
  
  Abstract We study (un)soundness of transformations of conditional term rewriting systems (CTRSs) into unconditional term rewriting systems (TRSs). The focus here is on analyzing (un)soundness of so-called unravelings, the most basic and natural class of such transformations. We extend our previous analysis from normal 1-CTRSs to the more general class of deterministic CTRSs (DCTRSs) where extra variables in right-hand sides of rules are allowed to a certain extent. We prove that the previous soundness results based on weak left-linearity and on right-linearity can be extended from normal 1-CTRSs to DCTRSs. Counterexamples show that such an extension to DCTRSs does not work for the previous criteria which were based on confluence and on non-erasingness, not even for right-stable systems. Yet, we prove weaker versions of soundness criteria based on confluence and on non-erasingness. Finally, we compare our approach and results with other recently established soundness criteria for unraveling DCTRSs.
  
  
• Eugen Jiresch and Bernhard Gramlich
  Realizing Monads in Interaction Nets via Generic Typed Rules
  Technical Report E1852-2011-01, Theory and Logic Group, Institute of Computer Languages, TU Wien, Austria, June 2011.
  
  Abstract Interaction net systems are a model of computation based on graph rewriting. They enjoy various nice properties which make them a promising basis for a functional programming language. However, mechanisms to model impure functions are indispensable for a practical language. A natural approach to achieve this goal is the systematic use of monads. Yet, specifying the appropriate monads for impure language features is hard, due to the very restricted form of basic interaction rules. What is missing in particular, are appropriate means to specify higher-order functions and some typing mechanism that restricts computations to reasonable settings. In this paper, we propose two extensions of interaction nets which solve these problems. First we extend interaction rules with generic rules, thus adding a form of higher-order functions. Moreover, we define constraints on these rules to ensure the preservation of uniform confluence. In addition, we propose a simple type system in order to appropriately restrict the matching of generic rules. Finally, we show how the combination of these features, i.e., generic typed rules, can indeed be employed to model impure functions in interaction nets via monads in an intuitive and simple manner.
  
  
• Karl Gmeiner, Bernhard Gramlich and Felix Schernhammer
  On (Un)Soundness of Unravelings
  Technical Report E1852-2010-01, Theory and Logic Group, Institute of Computer Languages, TU Wien, Austria, April 2010.
  
  Abstract We revisit (un)soundness of transformations of conditional into unconditional rewrite systems. The focus here is on so-called unravelings, the most simple and natural kind of such transformations, for the class of normal conditional systems without extra variables. By a systematic and thorough study of existing counterexamples and of the potential sources of unsoundness we obtain several new positive and negative results. In particular, we prove the following new results: Confluence, non-erasingness and weak left-linearity (of a given conditional system) each guarantee soundness of the unraveled version w.r.t. the original one. The latter result substantially extends the only known sufficient criterion for soundness, namely left-linearity. Furthermore, by means of counterexamples we refute various other tempting conjectures about sufficient conditions for soundness.
  
  
• Bernhard Gramlich and Felix Schernhammer
  Extending Context-Sensitivity in Term Rewriting
  Technical Report E1852-2009-02, Theory and Logic Group, Institute of Computer Languages, TU Wien, Austria, December 2009.
  
  Abstract We propose a generalized version of context-sensitivity in term rewriting based on the notion of "forbidden patterns". The basic idea is that a rewrite step should be forbidden if the redex to be contracted has a certain shape and appears in a certain context. This shape and context is expressed through forbidden patterns. In particular we analyze the relationships among this novel approach and the commonly used notion of context-sensitivity in term rewriting, as well as the feasibility of rewriting with forbidden patterns from a computational point of view. The latter feasibility is characterized by demanding that restricting a rewrite relation yields an improved termination behaviour while still being powerful enough to compute meaningful results. Sufficient criteria for both kinds of properties in certain classes of rewrite systems with forbidden patterns are presented.
  
  
• Felix Schernhammer and Bernhard Gramlich
  Characterizing and Proving Operational Termination of Deterministic Conditional Term Rewriting Systems
  Technical Report E1852-2009-01 (revised and extended version of WST 2007 and NWPT 2008 contributions), Theory and Logic Group, Institute of Computer Languages, TU Wien, Austria, September 2009 (revised version).
  
  Abstract We investigate the practically crucial property of operational termination of deterministic conditional term rewriting systems (DCTRSs), an important declarative programming paradigm. We show that operational termination can be equivalently characterized by the newly introduced notion of context-sensitive quasi-reductivity. Based on this characterization and an unraveling transformation of DCTRSs into context-sensitive (unconditional) rewrite systems (CSRSs), context-sensitive quasi-reductivity of a DCTRS is shown to be equivalent to termination of the resulting CSRS on original terms. This result enables both proving and disproving operational termination of given DCTRSs via transformation into CSRSs. A concrete procedure for this restricted termination analysis (on original terms) is proposed and encouraging benchmarks obtained by the termination tool VMTL, that utilizes this approach, are presented. Finally, we show that the context-sensitive unraveling transformation is sound and complete for collapse-extended termination, thus solving an open problem of [Duran et al. 2008].
  
  
• Felix Schernhammer and Bernhard Gramlich
  Termination of Lazy Rewriting Revisited
  Technical Report E1852-2007-01 (full version of WRS 2007 paper, 30 pages), Theory and Logic Group, Institute of Computer Languages, TU Wien, Austria, November 2007.
  
  Abstract Lazy rewriting is a proper restriction of term rewriting that dynamically restricts the reduction of certain arguments of functions in order to obtain termination. In contrast to context-sensitive rewriting reductions at such argument positions are not completely forbidden but delayed. Based on the observation that the only existing (non-trivial) approach to prove termination of such lazy rewrite systems is flawed, we develop a modified approach for transforming lazy rewrite systems into context-sensitive ones that is sound and complete with respect to termination. First experimental results with this transformation based technique are encouraging.
  
  
• María Alpuente, Bernhard Gramlich and Alicia Villanueva
  A Framework for Timed Concurrent Constraint Programming with External Functions
  Technical Report DSIC-II/13/06, 16 pages, Departamento de Sistemas Informáticos y Computación, UPV, Valencia, Spain, December 2006.
  
  Abstract The timed concurrent constraint programming language (tccp in short) was introduced for modeling reactive systems. This language allows one to model in a very intuitive way typical ingredients of these systems such as timeouts, preemptions, etc. However, there is no natural way for modeling other desirable features such as functional computations, for example for calculating arithmetic results. In fact, although it is certainly possible to implement such kind of operations, each single step of the computation takes time in tccp, and avoiding interferences with the intended overall behavior of the (reactive) system is quite involved. In this paper, we propose an extension of tccp for modeling instantaneous computations which improves the expressiveness of the language, in the sense that operations that are cumbersome to implement in pure tccp, are executed by calling an efficient, external functional engine, while the tccp programmer can focus on the pure, and usually more complex, reactive part of the system. We also describe a case study which motivates the work, and discuss how the new capability presented here can also be used as a new tool for developers from the verification point of view.

  Keywords: Timed Concurrent Constraint language; Functional features; Case study

  
  
  
• María Alpuente, Santiago Escobar, Bernhard Gramlich and Salvador Lucas
  On-Demand Strategy Annotations Revisited
  Technical Report DSIC-II/18/03, 51 pages, Departamento de Sistemas Informáticos y Computación, UPV, Valencia, Spain, July 2003.
  
  Abstract In functional languages such as OBJ*, CafeOBJ, and Maude, symbols are given strategy annotations that specify (the order in) which subterms are evaluated. Syntactically, strategy annotations are given either as lists of natural numbers or as lists of integers associated to function symbols whose (absolute) values refer to the arguments of the corresponding symbol. A positive index prescribes the evaluation of an argument whereas a negative index means "evaluate on-demand". While strategy annotations containing only natural numbers have been implemented and investigated to some extent (regarding, e.g., termination and completeness), fully general annotations (also called on-demand strategy annotations), which have been proposed to support laziness in OBJ-like languages, are disappointingly under-explored to date. In this paper, we first point out a number of problems of current proposals for handling on-demand strategy annotations, such as undecidability of the reduction relation or inadequacy of the model. Then, we propose a solution to these problems by keeping an accurate track of annotations along evaluation sequences. This solution is defined as a suitable extension of the $E$-evaluation strategy of OBJ-like languages (which only considers annotations given as natural numbers) to on-demand strategy annotations. Our strategy overcomes the drawbacks of these previous proposals and also exhibits better computational properties. For instance, we show how to use it for computing (head-)normal forms. We also introduce a transformation for proving termination of the new evaluation strategy by using standard techniques. Finally, we present an interpreter of the new strategy together with some encouraging experiments.
  
  
  
• Bernhard Gramlich
  On Interreduction of Semi-Complete Term Rewriting Systems
  Technical Report E1852-BG-99-01, Technische Universität Wien, September 1999.
  
  Abstract For a complete, i.e., confluent and terminating term rewriting system (TRS) it is well-known that simplification (also called interreduction) into an equivalent canonical, i.e., complete and interreduced TRS is easily possible. This can be achieved by first normalizing all right-hand sides of the TRS and then deleting all rules with a reducible left-hand side. Here we investigate the logical and operational preservation properties of the same simplification operations for semi-complete, i.e., confluent and weakly terminating TRSs. Surprisingly, it turns out that for semi-complete TRSs these simplifications are neither operationally harmless nor logically correct: Semi-completeness may get lost and the induced equational theory need not be preserved. We also provide sufficient criteria for the preservation of semi-completeness and of the induced equational theory. In particular, we show that orthogonal TRSs enjoy all these preservation properties. In the general case, for a given semi-complete TRS an equivalent semi-canonical, i.e., semi-complete and interreduced system need not even exist.
  
  
  
• Bernhard Gramlich
  Modular Aspects of Rewrite-Based Specifications
  Research Report RR-3330, INRIA Lorraine, Nancy, France, 1997.
  
  Abstract We investigate modular properties of term rewriting systems, the basic operational formalism for equational specifications. First we study sufficient conditions for the preservation of the termination property under disjoint (and more general) combinations of term rewriting systems. By means of a refined analysis of existing approaches we show how to prove several new asymmetric preservation results. For this purpose we introduce two interesting new properties of term rewriting systems related to collapsing reductions: uniquely collapsing and collapsing confluent. We discuss these properties w.r.t. well-known confluence, consistency and normal form properties, and show that they are modular for left-linear systems, but not in general.
  
  
  
• Bernhard Gramlich
  On Semi-Completeness of Term Rewriting Systems
  Research Report RR-3327, INRIA Lorraine, Nancy, France, 1997.
  
  Abstract We investigate the question whether semi-completeness, i.e., weak termination plus confluence, of term rewriting systems is preserved under the normalization of right-hand sides. We give a simple counterexample showing that in general this transformation neither preserves weak termination nor (local) confluence. Moreover we present two conditions which are sufficient for the preservation of semi-completeness. In particular, we show that (almost) orthogonal systems enjoy this preservation property.
  
  
  
• Bernhard Gramlich
  Confluence without Termination via Parallel Critical Pairs
  SEKI-Report SR-95-13, Fachbereich Informatik, Universität Kaiserslautern, 1995.
  
  Abstract We present a new criterion for confluence of (possibly) non-terminating left-linear term rewriting systems. The criterion is based on certain strong joinability properties of parallel critical pairs. We show how this criterion relates to other well-known results, consider some special cases and discuss some possible extensions.
  
  
  
• Bernhard Gramlich
  A Note on a Parameterized Version of the Well-Founded Induction Principle
  SEKI-Report SR-95-08, Fachbereich Informatik, Universität Kaiserslautern, 1995.
  
  Abstract The well-known and powerful proof principle by well-founded induction says that for verifying $\forall x: P(x)$ for some property $P$ it suffices to show $\forall x: [ [ \forall y < x : P(y) ] \imp P(x) ]$, provided $<$ is a well-founded partial ordering on the domain of interest. Here we investigate a more general formulation of this proof principle which allows for a kind of parameterized partial orderings $<_x$ which naturally arises in some cases. More precisely, we develop conditions under which the parameterized proof principle $\forall x: [ [ \forall y <_x x : P(y) ] \imp P(x) ]$ is sound in the sense that $\forall x: [ [ \forall y <_x x : P(y) ] \imp P(x) ] \imp \forall x: P(x)$ holds, and give counterexamples demonstrating that these conditions are indeed essential.
  
  
  
• Bernhard Gramlich
  New Abstract Criteria for Termination and Confluence of Conditional Rewrite Systems
  SEKI-Report SR-93-17, Fachbereich Informatik, Universität Kaiserslautern, 1993.
  
  Abstract We consider the problem of verifying confluence and termination of conditional term rewriting systems (TRSs). For unconditional TRSs the critical pair lemma holds which enables a finite test for confluence of (finite) terminating systems. And for ensuring termination of unconditional TRSs a couple of methods for constructing appropiate well-founded term orderings are known. If however termination is not guaranteed then proving confluence is much more difficult. Recently we have obtained some interesting results for unconditional TRSs which provide sufficient criteria for termination plus confluence in terms of restricted termination and confluence properties. In particular, we have shown that any innermost terminating and locally confluent overlay system is complete, i.e. terminating and confluent. Here we generalize our approach to the conditional case and show how to solve the additional complications due to the presence of conditions in the rules. Our main result can be stated as follows: Any conditional TRS which is an innermost terminating semantical overlay system such that all (conditional) critical pairs are joinable is complete.
  
  
  
• Bernhard Gramlich
  Relating Innermost, Weak, Uniform and Modular Termination of Term Rewriting Systems
  SEKI-Report SR-93-09, Fachbereich Informatik, Universität Kaiserslautern, 1993.
  
  Abstract We investigate restricted termination and confluence properties of term rewriting systems, in particular weak termination and innermost termination, and their interrelation. New criteria are provided which are sufficient for the equivalence of innermost / weak termination and uniform termination of term rewriting systems. These criteria provide interesting possibilities to infer completeness, i.e. termination plus confluence, from restricted termination and confluence properties. Using these basic results we are also able to prove some new results about modular termination of rewriting. In particular, we show that termination is modular for some classes of innermost terminating and locally confluent term rewriting systems, namely for non-overlapping and even for overlay systems. As an easy consequence this latter result also entails a simplified proof of the fact that completeness is a decomposable property of so-called constructor systems. Furthermore we show how to obtain similar results for even more general cases of (non-disjoint) combined systems with shared constructors and of certain hierarchical combinations of systems with constructors. Interestingly, these modularity results are obtained by means of a proof technique which itself constitutes a modular approach.
  
  
  
• Claus-Peter Wirth, Bernhard Gramlich, Ulrich Kühler and Horst Prote
  Constructor-Based Inductive Validity in Positive/Negative Conditional Relating Innermost, Weak, Uniform and Modular
  SEKI-Report SR-93-05, Fachbereich Informatik, Universität Kaiserslautern, 1993.
  
  Abstract We study algebraic specifications given by finite sets R of positive/negative-conditional equations (i.e. universally quantified first-order implications with a single equation in the succedent and a conjunction of positive and negative (i.e. negated) equations in the antecedent). The class of models of such a specification R does not contain in general a minimum model in the sense that it can be mapped to any other model by some homomorphism. We present a constructor-based approach for assigning appropriate semantics to such specifications. We introduce two syntactic restrictions: firstly, for a condition to be fulfilled we require the evaluation values of the terms of the negative equations to be in the constructor sub-universe which contains the set of evaluation values of all constructor ground terms; secondly, we restrict the constructor equations to have "Horn"-form and to be "constructor-preserving". A reduction relation for R is defined, which allows to generalize the fundamental results for positive-conditional rewrite systems, which does not need to be noetherian or restricted to ground terms, and which is monotonic w.r.t. consistent extension of the specification. Under the assumption of confluence, the factor algebra of the term algebra modulo the congruence of the reduction relation is a minimal model which is (beyond that) the minimum of all models that do not identify more objects of the constructor sub-universe than necessary and which establishes one of the four notions of inductive validity of Gentzen clauses we discuss. To achieve decidability of reducibility we define several kinds of compatibility of R with a reduction ordering and present a complete critical-pair test for the confluence of the reduction relation.
  
  
  
• Claus-Peter Wirth and Bernhard Gramlich
  A Constructor-Based Approach for Positive/Negative-Conditional Equational Specifications
  SEKI-Report SR-92-10, Fachbereich Informatik, Universität Kaiserslautern, 1992.
  
  Abstract We study algebraic specifications given by finite sets R of positive/negative-conditional equations (i.e. universally quantified first-order implications with a single equation in the succedent and a conjunction of positive and negative (i.e. negated) equations in the antecedent). The class of models of such a specification R does not contain in general a minimum model in the sense that it can be mapped to any other model by some homomorphism. We present a constructor-based approach for assigning appropriate semantics to such specifications. We introduce two syntactic restrictions: firstly, for a condition to be fulfilled we require the evaluation values of the terms of the negative equations to be in the set of evaluation values of constructor ground terms; secondly, we restrict the constructor rules to have "Horn"- form and to be "constructor-preserving". A reduction relation for R is defined, which allows to generalize the fundamental results for positive-conditional rewrite systems, which does not need to be noetherian or restricted to ground terms, and which is monotonic w.r.t. the extension of the specification. Under the assumption of confluence, the factor algebra of the ground term algebra modulo the congruence of our reduction relation is a minimal model which is (beyond that) the minimum of all models that do not identify more constructor ground terms than necessary. To achieve decidability of reducibility we define several kinds of compatibility of R with a reduction ordering and present a complete critical-pair test à la Knuth-Bendix for the confluence of our reduction relation.
  
  
  
• Bernhard Gramlich
  Towards Intelligent Inductive Proof Engineering
  SEKI-Report SR-92-01, Fachbereich Informatik, Universität Kaiserslautern, 1992.
  
  Abstract This paper deals with inductive theorem proving in equational theories using the well-developed framework of completion and rewriting techniques for systems of term equations and rewrite rules. The theoretical foundations are briefly reviewed focussing on the central ideas as well as on important operationalization issues. Moreover a brief comparison of different inductive proof techniques is included. Concerning practical applications we discuss and isolate crucial aspects of the whole specification and proof engineering process. The necessity of linking together this whole process of formalizing, modelling and structuring abstract (equational) specifications of algorithms and corresponding (inductive) properties to be verified is pointed out and exemplified by means of an extended non-trivial example. Crucial conceptual as well as proof-technical aspects are presented and discussed. They constitute the basis for an adequate integration and combintion of intelligent user-guided and machine-supported automated reasoning. Finally the main theoretical and practical problems as well as promising perspectives for future work are sketched, in particular concerning architectural and design principles for future generation inductive theorem provers.
  
  
  
• Bernhard Gramlich and Wolfgang Lindner
  A Guide to UNICOM, an Inductive Theorem Prover Based on Rewriting and Completion Techniques
  SEKI-Report SR-91-17, Fachbereich Informatik, Universität Kaiserslautern, 1991.
  
  Abstract We provide an overview of UNICOM, an inductive theorem prover for equational logic which is based on refined rewriting and completion techniques. The architecture of the system as well as its functionality are described. Moreover, an insight into the most important aspects of the internal proof process is provided. This knowledge about how the central inductive proof component of the system essentially works is crucial for human users who want to solve non-trivial proof tasks with UNICOM and thoroughly analyse potential failures. The presentation is focussed on practical aspects of understanding and using UNICOM. A brief but complete description of the command interface, an installation guide, an example session, a detailed extended example illustrating various special features and a collection of successfully handled examples are also included.
  
  
  
• Bernhard Gramlich
  A Structural Analysis of Modular Termination of Term Rewriting Systems
  SEKI-Report SR-91-15, Fachbereich Informatik, Universität Kaiserslautern, 1991.
  
  Abstract Modular properties of term rewriting systems, i.e. properties which are preserved under disjoint unions, have attracted an increasing attention within the last few years. Whereas confluence is modular this does not hold true in general for termination. By means of a careful analysis of potential counterexamples we prove the following abstract result. Whenever the disjoint union $\dsum$ of two (finite) terminating term rewriting systems $\reins$, $\rzwei$ is non-terminating, then one of the systems, say $\reins$, enjoys an interesting (undecidable) property, namely it is not termination preserving under non-deterministic collapses, i.e. \mbox{$\reins \oplus \{ G(x,y) \ra x, G(x,y) \ra y \}$} is non-terminating, and the other system $\rzwei$ is collapsing, i.e. contains a rule with a variable right hand side. This result generalizes known sufficient syntactical criteria for modular termination of rewriting. Then we develop a specialized version of the `increasing interpretation method' for proving termination of combinations of term rewriting systems. This method is applied to establish modularity of termination for certain classes of term rewriting systems. In particular, termination turns out to be modular for the class of systems, for which termination can be shown by simplification orderings (this result has recently been obtained by Kurihara \& Ohuchi by a similar, but less general proof technique). Moreover, we show that the weaker property of being non-self-embedding which also implies termination is not modular. We prove that the finiteness restrictions in our main results concerning the term rewriting systems involved can be considerably weakened. Furthermore, we prove that the minimal rank of potential counterexamples in disjoint unions may be arbitrarily high. Hence, a general analysis of arbitrarily complicated `mixed' term seems to be necessary when modularity of termination is investigated. Finally, we show that generalizations of our main results are possible for the cases of conditional term rewriting systems as well as for some restricted form of non-disjoint combinations of term rewriting systems involving common constructors.
  
  
  
• Bernhard Gramlich
  Completion Based Inductive Theorem Proving: A Case Study in Verifying Sorting Algorithms
  SEKI-Report SR-90-04, Fachbereich Informatik, Universität Kaiserslautern, 1990.
  
  Abstract The focus of this paper lies on practical aspects of completion based inductive theorem proving in equational theories. As domain of interest we concentrate on the mechanically supported verification of a couple of sorting algorithms. The experiments have been performed with UNICOM, an inductive theorem prover based on refined unfailing completion techniques. We summarize these experiments, point out important technical and conceptual aspects, and illustrate them by numerous examples. In particular, we discuss and exemplify the kind of intelligent proof engineering required for succeeding in non-trivial verification problems.
  
  
  
• Bernhard Gramlich
  Inductive Theorem Proving Using Refined Unfailing Completion Techniques
  SEKI-Report SR-89-14, Fachbereich Informatik, Universität Kaiserslautern, 1989.
  
  Abstract We present a brief overview on completion based inductive theorem proving techniques, point out the key concepts for the underlying "proof by consistency" paradigm and isolate an abstrcat description of what is necessary for an an algorithmic realization of such methods. In particular, we give several versions of proof orderings, which - under certain conditions - are well-suited for that purpose. Together with corresponding notions of (positve and negative) covering sets we get abstract "positive" and "negative" characterizations of inductive validity. As a consequencewe can generlize known criteria for inductive validity, even for the cases where some of the conjectures may not be orientable or where the base system is terminating but not necessarily ground confluent.
  Furthermore we consider several refinements and optimizations of completion based inductive theorem proving techniques. In particular, sufficient criteria for for being a covering set including restrictions of critical pairs (and the usage of non-equational inductive knowledge) are discussed. Moreover, a couple of lemma generation methods are briefly summarized and classified. A new technique of save generalization is particularly interesting, since it provides means for syntactic generalizations, i.e. simplifications, without loosing semantic equivalence. Finally, we present the main features and characteristics of UNICOM, an inductive theorem prover with refined unfailing completion techniques and built on top of TRSPEC, a term rewriting based system for investigating algebraic specifications.
  
  
  
• Bernhard Gramlich
  Unification of Term Schemes - Theory and Applications
  SEKI-Report SR-88-18, Fachbereich Informatik, Universität Kaiserslautern, 1988.
  
  Abstract We present a new approach for solving certain infinite sets of first order unification problems represented by term schemes. Withion the framework of second-order equational logic solving such scheme unification problems amounts exactly to solving (variable-)restricted unification problems. A method known for solving first-order restricted unification problems is generalized to the second-order case. Essentially this is achieved by transforming a restricted unification problem into an unrestricted one, solving the latter and retransforming the solutions obtained. The results on restricted second-order unification are then used to solve the original problem, namely to decide the solvability of scheme unification problems and - in the positive case - to compute the corresponding most general unifiers. Finally the results obtained are applied to provide sufficient conditions for a property of "repeated" unifiability which in turn is crucial for the analysis of divergence of completion procedures for term rewriting systems. Although the study of divergent completion behavior was the starting point of the work presented, the results obtained are not only applicable to divergnece analysis, but may be useful for other applications, too.
  
  
  
• Bernhard Gramlich and Jörg Denzinger
  Efficient AC-matching Using Constraint Propagation
  SEKI-Report SR-88-15, Fachbereich Informatik, Universität Kaiserslautern, 1988.
  
  Abstract We present a new approach to associative-commutative (AC-)pattern matching using a technique of global constraint propagation which in many cases enables us to drastically cut down the search space for solutions. Given a conjunction of simplified non-trivial AC-matching problems the main idea of our method consists in deducing and propagating constraints for possible variable assignments from all problems instead of choosing only one problem for processing next. Thus many failure branches of the search tree for solutions can be cut down without expanding them. The control strategy for branching is designed such that nodes with a small branching degree are preferred. Incorporating some additional optimizations we get a new AC-matching algorithm which is especially well-suited for certain non-linear patterns and for a systematic early detection of unsolvability. Moreover we point out the advantages of using unique ordered normal forms for AC-equivalent terms based on a special class of orderings on the function symbols and the variables. Finally we sketch how our constraint propagation approach for AC-matching can be generalized to other kinds of E-matching and E-unification problems.
  
  

Bernhard Gramlich