.A term rewrite system is called simply terminating if its termination can be shown by means of a simplification ordering. According to a result of Weiermann, the derivation length function of any simply terminating finite rewrite system is eventually dominated by a Hardy function of ordinal less than the small Veblen ordinal. This bound had appeared to be of rather theoretical nature, because all known examples had had multiple recursive complexities, until recently Touzet constructed simply terminating examples with complexities beyond (...) multiple recursion. This was established by simulating the Hydra battle for all ordinal segments below the proof-theoretic ordinal of Peano arithmetic. By extending this result to the small Veblen ordinal we prove the huge bound of Weiermann to be sharp. As a spin-off we can show that total termination allows for complexities as high as those of simple termination. (shrink)

Let F be a signature and R a strictly orthogonal rewrite system on ground terms of F . We give an effective proof of a bounding condition for R , based on a detailed analysis of how terms are transformed during the rewrite process, which allows us to give recursive bounds on the derivation lengths of terms. We give a syntactic characterisation of the Grzegorczyk hierarchy and a rewriting schema for calculating its functions. As a consequence of this, using (...) results of Elias Tahhan–Bittar, it can be shown that, for n⩾3 , the derivation length functions for functions in Grzegorczyk class E n belong to Grzegorczyk class E n+1 . We also give recursive bounds for the derivation lengths of functions defined by parameter recursion. (shrink)

Recently, Brass and Dix showed 143–165) that the well founded semantics WFS can be defined as a confluent calculus of transformation rules. This led not only to a simple extension to disjunctive programs 167–213), but also to a new computation of the well-founded semantics which is linear for a broad class of programs. We take this approach as a starting point and generalize it considerably by developing a general theory of Confluent LP-systems CS . Such a system CS is (...) a rewriting system on the set of all logic programs over a fixed signature L and it induces in a natural way a canonical semantics. Moreover, we show four important applications of this theory: most of the well-known semantics are induced by confluent LP-systems , there are many more transformation rules that lead to confluent LP-systems , semantics induced by such systems can be used to model aggregation , the new systems can be used to construct interesting counterexamples to some conjectures about the space of well-behaved semantics. (shrink)

We present a characterization of confluence for term rewriting systems, which is then refined for special classes of rewriting systems. The refined characterization is used to obtain a polynomial time algorithm for deciding the confluence of ground term rewrite systems. The same approach also shows the decidability of confluence for shallow and linear term rewriting systems. The decision procedure has a polynomial time complexity under the assumption that the maximum arity of a function (...) symbol in the signature is a constant. (shrink)

The termination of rewrite systems for parameter recursion, simple nested recursion and unnested multiple recursion is shown by using monotone interpretations both on the ordinals below the first primitive recursively closed ordinal and on the natural numbers. We show that the resulting derivation lengths are primitive recursive. As a corollary we obtain transparent and illuminating proofs of the facts that the schemata of parameter recursion, simple nested recursion and unnested multiple recursion lead from primitive recursive functions to primitive recursive (...) functions. (shrink)

The “official” history of connexive logic was written in 2012 by Storrs McCall who argued that connexive logic was founded by ancient logicians like Aristotle, Chrysippus, and Boethius; that it was further developed by medieval logicians like Abelard, Kilwardby, and Paul of Venice; and that it was rediscovered in the 19th and twentieth century by Lewis Carroll, Hugh MacColl, Frank P. Ramsey, and Everett J. Nelson. From 1960 onwards, connexive logic was finally transformed into non-classical calculi which partly concur with (...) systems of relevance logic and paraconsistent logic. In this paper it will be argued that McCall’s historical analysis is fundamentally mistaken since it doesn’t take into account two versions of connexivism. While “humble” connexivism maintains that connexive properties only apply to “normal” antecedents, “hardcore” connexivism insists that they also hold for “abnormal” propositions. It is shown that the overwhelming majority of the forerunners of connexive logic were only “humble” connexivists. Their ideas concerning connexive implication don’t give rise, however, to anything like a non-classical logic. (shrink)

The main powerful method for establishing termination of term rewriting systems was discovered by Nachum Dershowitz through the introduction of certain natural well founded orderings (lexicographic path orderings). This leads to natural decision problems which may be of the highest computational complexity of any decidable problems appearing in a natural established computer science context.

Inspired by Judith Butler's conceptualization of drag as ‘gender parody’, I develop the conceptual frame of ‘textual drag’ in order to define and examine the relationship between parody, satire and gender. I test this frame by reading two seminal feminist works, Virginia Woolf's Orlando and Monique Wittig's Le Corps lesbien. Both texts lend themselves particularly persuasively to analysis with this frame, as they each use parodic strategies to facilitate proto-queer satirical critiques of reductive gender norms. Orlando deploys an exaggerated nineteenth-century (...) biographical style, which foregrounds the protagonist's gender fluidity and her developing critique of the norms and systems that surround her, while Le Corps lesbien rewrites canonical romance narratives from a lesbian perspective, challenging the heterosexism inherent in these narratives and providing new modes of thinking about gender, desire and sexual interaction. (shrink)

The debate on sustainable globalized development rests on two clearly stated economic assumptions: that "development" proceeds, solely and inevitably, through industrialization and the proliferation of capital intensive high-technology, towards the creation of service sector economies; and that globalization, based on a neoliberal, capitalist, free market ideology, provides the only vehicle for such development. Sustainability, according to the proponents of globalized development, is merely a function of market forces, which will generate the solutions for all problems including the environmental dilemmas that (...) loom over the globe today. The social focus of globalized development is clearly the "individual" and the much-touted goal of development in the context of these debates, is the emancipation of the individual from want. This glorification of the individual, so characteristic of the Enlightenment, has defined all aspects of modernity, leading to approaches that are self-focused and that give little thought to the needs of society or even the social context. The increasing impoverishment of human life and the growing environmental degradation, however, provide a poignant counterpoint to this onrush of capital interests, demanding a reassessment of sustainability separate from the logic of industrialization and globalized development. This paper examines the unfolding of the logic of capitalism, which underlies the structure of the Rostowian model of development and the problems in the assumptions underlying today''s globalized development process. The evident impossibility of sustainability in the current growth-based market system leads to the examination of alternatives including a reflexive understanding of the choices and the inclusion of opportunity costs, related to the social, environmental and economic aspects of decision making. The integration of all factors of production into the logic of development provides a sustainable alternative to the current system. (shrink)

The Turkish translation of the azān, the Muslim call to prayer, in the early Republican era stood as a striking symbol of the drastic changes witnessed in the Turkish state and its people as attempts to secularize the nation and redefine its identity dominated the state’s socio-political agenda. Evaluating this phenomenon from the perspective of Translation Studies can reveal novel insights into why the azān was translated and why it was met with resistance. This case study attempted to rethink the (...) translation of the azān from the perspective of rewriting and to explore its negative reception from the perspective of norms, with particular emphasis placed on the setting and historical context of the translation. Based on the ideological motives portrayed and the other reforms implemented by the state, or in other words, the patron, it is possible to argue that the translation of the azān can be regarded as an act of rewriting. The opposition directed towards it can be accounted for by the norms of the people opposing it. Based on their history with the Islamic belief system, it can be assumed that Islam and its Arabic practices played a big part in the values that make up their norms. (shrink)

In various documents the view emerges that contemporary biotechnosciences are currently experiencing a scientific revolution: a massive increase of pace, scale and scope. A significant part of the research endeavours involved in this scientific upheaval is devoted to understanding and, if possible, ameliorating humankind: from our genomes up to our bodies and brains. New developments in contemporary technosciences, such as synthetic biology and other genomics and “post-genomics” fields, tend to blur the distinctions between prevention, therapy and enhancement. An important dimension (...) of this development is “biomimesis”: i.e. the tendency of novel technologies and materials to mimic or plagiarize nature on a molecular and microscopic level in order to optimise prospects for the embedding of technological artefacts in natural systems such as human bodies and brains. In this paper, these developments are read and assessed from a psychoanalytical perspective. Three key concepts from psychoanalysis are used to come to terms with what is happening in research laboratories today. After assessing the general profile of the current revolution in this manner, I will focus on a particular case study, a line of research that may serve as exemplification of the vicissitudes of contemporary technosciences, namely viral biomaterials. Viral life forms can be genetically modified (their genomes can be rewritten) in such a manner that they may be inserted in human bodies in order to produce substances at specific sites such as hormones (testosterone), neurotransmitters (dopamine), enzymes (insulin) or bone and muscle tissue. Notably, certain target groups such as top athletes, soldiers or patients suffering from degenerative diseases may become the pioneers serving as research subjects for novel applications. The same technologies can be used for various purposes ranging from therapy up to prevention and enhancement. (shrink)

Brown famously held that in the field of public education, segregation has no place. But segregation was undefined. Was segregation constituted by mere racial classification, by the fact that the state had divided children into racial groups? Or did Brown condemn a caste system whose effect was to stigmatize black children. In Parents Involved v. Seattle Justice Roberts says segregation is about children not black children. This colorblind approach represents both a rewriting and appropriation of Brown in the service (...) of formalism. The Roberts court writes not only a new version of Brown but a new historical narrative about the meaning of segregation. The theme of this new story is formal equality - equality of opportunity only - as a universal ideal. This new story is woven entirely out of the language of Brown detached from all historical context. Conservatives have long canonized Brown. It has been a kind of second constitution for the second reconstruction. But how does this new story compare to the original understanding ?: Was this the evil that Brown denounced? By framing the issue in this way the paper seeks to make an end run around an impasse in our social and legal debate. Many progressive scholars have challenged the conservative conception of formal equality by suggesting alternative ways of thinking about it: anti-subordination models, a heightened call that equality should take issues of racial caste into account. But this external critique has stalled, perhaps in part because of the slippery indeterminacy of normative ideals. Segregation is far more determinate; it is something that has been concretized not only by the lived experience of black people, but by an earlier realist tradition on the part of the Warren court which saw it as it was. Retelling the two parts of this forgotten history we expose the disconnect between the Supreme Court's universalism and the actual meaning of segregation in context. Also, by focusing on the original understanding we seek a kind of internal critique showing how the politics of historical revision does not withstand the conservatives own interpretive approach. (shrink)

This book constitutes the refereed proceedings of the Third International Workshop on Frontiers of Combining Systems, FroCoS 2000, held in Nancy, France, in March 2000.The 14 revised full papers presented together with four invited papers were carefully reviewed and selected from a total of 31 submissions. Among the topics covered are constraint processing, interval narrowing, rewriting systems, proof planning, sequent calculus, type systems, model checking, theorem proving, declarative programming, logic programming, and equational theories.

We re-express our theorem on the strong-normalisation of display calculi as a theorem about the well-foundedness of a certain ordering on first-order terms, thereby allowing us to prove the termination of systems of rewrite rules. We first show how to use our theorem to prove the well-foundedness of the lexicographic ordering, the multiset ordering and the recursive path ordering. Next, we give examples of systems of rewrite rules which cannot be handled by these methods but which can be (...) handled by ours. Finally, we show that our method can also prove the termination of the Knuth-Bendix ordering and of dependency pairs. Keywords: rewriting, termination, well-founded ordering, recursive path ordering.. (shrink)

In this paper, we give a step by step introduction to the theory of well quasi-ordered transition systems. The framework combines two concepts, namely (i) transition systems which are monotonic wrt. a well-quasi ordering ; and (ii) a scheme for symbolic backward reachability analysis. We describe several models with infinite-state spaces, which can be analyzed within the framework, e.g., Petri nets, lossy channel systems, timed automata, timed Petri nets, and multiset rewriting systems. We will also (...) present better quasi-ordered transition systems which allow the design of efficient symbolic representations of infinite sets of states. (shrink)

Logic is traditionally considered to be a purely syntactic discipline, at least in principle. However, prof. David Isles has shown that this ideal is not yet met in traditional logic. Semantic residue is present in the assumption that the domain of a variable should be fixed in advance of a derivation, and also in the notion that a numerical notation must refer to a number rather than be considered a mathematical object in and of itself. Based on his work, the (...) central question of this thesis is what kind of logic, if any, results from removing this semantic residue from traditional logic.We differ from traditional logic in two significant ways. The first is that the assumption that a numerical notation must refer to a number is denied. Numerical notations are considered as mathematical objects in their own right, related to each other by means of rewrite rules. The traditional notion of reference is then replaced by the notion of reduction (by means of the rewrite rules) to a normal form. Two numerical notations that reduce to the same normal form would traditionally be considered identical, as they would refer to the same number, and hence they would be interchangeable salva veritate. In the new system, called Buridan-Volpin (BV), the numerical notations themselves are the elements of the domains of variables, and two numerical notations that reduce to the same normal form need not be interchangeable salva veritate, except when they are syntactically identical (i.e., have the same Gödel number).The second is that we do away with the assumption that the domains of variables need to be fixed in advance of a derivation. Instead we focus on what is needed to guarantee preservation of truth in every step of a derivation. These conditions on the domains of the variables, accumulated in the course of a derivation, are combined in a reference grammar. Whereas traditionally a derivation is considered valid when the conclusion follows from the premisses by way of the derivation rules (and possibly axioms), in the BV system a derivation must meet the extra condition that no inconsistency occurs within the reference grammar. For if the reference grammar were to give rise to inconsistency (i.e., it would be impossible to assign domains to all the variables without breaking at least one of the conditions placed on them in the reference grammar), there is no longer a guarantee that truth has been preserved in every step of the derivation, and hence the truth of the conclusion is not guaranteed by the derivation.In Chapter 2 the BV system is introduced in some formal detail. Chapter 3 gives some examples of derivations, notably totality of addition, multiplication and exponentiation, as well as a lemma needed for the proof of Euclid’s Theorem. These examples, taken from prof. Isles’ First-Order Reasoning and Primitive Recursive Natural Number Notations, show that there is a real proof-theoretical difference between traditional logic and the BV system. Here we also find the first major point of departure between myself and prof. Isles, centered on the notion of inheritance of conditions in the reference grammar by way of lemmata. These different points of view are best illustrated in the sections on the totality of exponentiation and on Euclid’s Lemma: prof. Isles maintains that the proof of totality of exponentiation is not BV valid, while I maintain that it is. But I do agree with him that the traditional proof of Euclid’s Lemma is not BV valid. Chapter 6 also expands the arguments for my choice in this matter.Now that it has been shown that there is a difference between traditional logic and BV, the properties of BV need to be examined. In Chapter 4 we give a proof of Cut-elimination for BV minus induction and the subformula property for BV, which allows us to prove the consistency of BV minus induction. We also expand on the reasons for excluding induction. In Chapter 5 we consider in detail the proof of a finite analog to the Löwenheim–Skolem theorem given by prof. Isles in his article with the same title. He proves that under certain conditions it is always possible, given the existence of a (possibly uncountable) model for a derivation, to give a finite model for this derivation. The system he considers deviates from BV as considered in this thesis in two significant ways: it does not contain the induction rule and the domains contain numbers instead of numerical notations. We then go on to show that it is possible to extend the result to include induction, in the sense that the existence of a possibly uncountable model for a derivation guarantees the existence of a model that is at most countable. We also consider the complications that arise from taking numerical expressions instead of numbers as the elements of domains.Finally, in Chapter 6 we consider the philosophical consequences of the BV system, informed by the formal results from the previous chapters. In particular we discuss the relation between reduction and reference, the status of reference grammars, the notion of induction and its function within BV, and some brief considerations on the consequences of the BV system for the discussion regarding nominalism and realism with regard to mathematical objects. The object of the chapter is twofold. On the one hand applying the formal results to philosophical questions, on the other hand arguing that BV is not just a theoretically acceptable alternative to traditional logic, but is in fact deserving of further development and research into its properties. The latter will probably appeal most to those of a nominalist and/or finitist bent.Abstract prepared by Harrie de Swart and Sven Storms.E-mail:[email protected]:https://research.tilburguniversity.edu/files/6170 1294/Storms_The_Buridan_Volpin_04_05_2022.pdf. (shrink)

Twenty years is a long time in the life of a science. While the historical roots of psychology have not changed since the first edition of this book, some of the offshoots of the various theories and systems discussed have been crit ically reexamined and have undergone far-reaching modifications. New and bold research has led to a broadening of perspectives, and recent devel opments in several areas required a considerable amount of rewriting. I have been fortunate in the (...) last fifteen years to have worked with about 2,000 psychologists and other behavioral scientists who contributed to several collected volumes I have edited. As the editor-in-chief of the In ternational Encyclopedia of Psychiatry, Psychology, Psychoanalysis and Neurol ogy, I have had the privilege of reading, scrutinizing, and editing the work of 1,500 experts in psychology and related disciplines. In addition, I have written several books and monographs and over one hundred scientific papers. Armed with all that experience, I have carefully examined the pages of the first edition. Chapter 8 required substantial rewriting and several new sections have been added to other chapters: "Current Soviet Psychol ogy" (Chapter 2, Section 7); "New Ideas on Purposivism" (Chapter 5, Sec tion 4); "Recent Developments in the Sociological School of Psychoanalysis" (Chapter 9, Section 4); and "Present Status of Gestalt Psychology" (Chapter 12, Section 4). Chapter 15 was omitted, and two new chapters were added: Chapter 14 ("Humanistic Psychology") and Chapter 16 ("Selected Research Areas"). (shrink)

This essay examines the experience of rewriting historical narratives from a world-system perspective, drawing on the author's attempt to construct an integrated image of the world economy in the thirteenth century. Searching for an intermediate epistemological path between unanchored postmodern hermeneutics and overconfident positivism, the author argues that three apparent deviations from the "ideals of positivist social science," which she ironically labels eccentricity, ideology, and idiosyncrasy, can yield significant "remakings" of world history. Eccentricity, namely, recognizing perspectives other than those (...) that conventionally view the world through the eyes of the West, can help historians to escape from ethnocentrism or Eurocentrism. Ideology, more conventionally called theory, is essential if historians are to select and integrate new material. And idiosyncrasy in the interests and backgrounds of historians can often be the source of the re-vision so essential for challenging earlier historical narratives. The author alludes to parallels with ethnographic research methods and cautions against substituting these three aids to research for rigorous attention to empirical sources and "the real world.". (shrink)

This paper suggests an online solution for the optimal tracking control of robotic systems based on a single critic neural network -based reinforcement learning method. To this end, we rewrite the robotic system model as a state-space form, which will facilitate the realization of optimal tracking control synthesis. To maintain the tracking response, a steady-state control is designed, and then an adaptive optimal tracking control is used to ensure that the tracking error can achieve convergence in an optimal sense. (...) To solve the obtained optimal control via the framework of adaptive dynamic programming, the command trajectory to be tracked and the modified tracking Hamilton-Jacobi-Bellman are all formulated. An online RL algorithm is the developed to address the HJB equation using a critic NN with online learning algorithm. Simulation results are given to verify the effectiveness of the proposed method. (shrink)

The discussion on symbolic legislation unveils intriguing relationships between law and politics. However, the abundance of observations often results in conceptual chaos and raises numerous problematic questions. These inquiries revolve around the scope of the concept of symbolic legislation (is it a marginal or universal phenomenon in the legal system?), as well as the circumstances determining whether a provision or legal act is classified as symbolic legislation. Of particular interest is the question of whether a provision or legal act can (...) “become symbolic” over time. The research goal of this study is to analyse the process of “becoming symbolic” and derive conclusions that deepen the understanding of the phenomenon of symbolic legislation. This study organises the current discussion on symbolic legislation, focusing on a case study of the structure of the crime of animal abuse in the Polish Animal Protection Act. The author illustrates how certain elements of this provision “became symbolic,” demonstrating that this process is largely independent of the motives of the legislators. In conclusion, the author emphasises the importance of consistently separating the sphere of motives from the sphere of effects in the discussion on symbolic legislation. Furthermore, the author highlights the static nature of the former and the dynamic nature of the latter. (shrink)

The International workshop 'Frontiers of Combining Systems' is the only forum that is exclusively devoted to research efforts in this interdisciplinary area. This volume contains selected, edited papers from the second installment of the workshop. The contributions range from theorem proving, rewriting and logic to systems and constraints. While there is a clear emphasis on automated tools and logics, the contributions to this volume show that there exists a rapidly expanding body of solutions of particular instances of (...) the combination problem, and at the same time, that the issue of developing general frameworks for intergrating formalisms and systems is taking on an increasingly important position on the international research agenda. The idea of combining formal systems and algorithms has been attracting interest in areas as diverse as constraint logic programming, automated deduction, verification, information retrieval, computational linguistics, artificial intelligence, and logic. As any interesting real world system is a complex composite entity, decomposing its descriptive requirements (for design, verification, or maintenance purposes) into simpler, more restricted tasks is appealing as it is often the only plausible way of tackling complex modelling problems. A core body of notions, questions and results is beginning to emerge in the area, and we are beginning to understand the computational and logical impact of combining methods and algorithms. (shrink)

This essay re-examines Hegel’s critique of Spinoza’s Ethics, focusing on the question of method. Are the axioms and definitions unmotivated presuppositions that make the attainment of absolute knowledge impossible in principle, as Hegel charges? This essay develops a new reading of the Ethics to defend it from this critique. I argue that Hegel reads Spinoza as if his system were constructed only according to the mathematical second kind of knowledge, ignoring Spinoza’s clear preference for knowledge of the third kind. The (...) Ethics, I argue, is a book with several layers: it is at once a deductive mathematical system, and a handbook to aid the intuitive power of the active philosophical reader. The letter of each text may be identical, but they have little else in common – Pierre Menard’s rewriting of Don Quixote given systematic philosophical form. (shrink)

In this article, I show why it is necessary to abolish the use of predictive algorithms in the US criminal justice system at sentencing. After presenting the functioning of these algorithms in their context of emergence, I offer three arguments to demonstrate why their abolition is imperative. First, I show that sentencing based on predictive algorithms induces a process of rewriting the temporality of the judged individual, flattening their life into a present inescapably doomed by its past. Second, I (...) demonstrate that recursive processes, comprising predictive algorithms and the decisions based on their predictions, systematically suppress outliers and progressively transform reality to match predictions. In my third and final argument, I show that decisions made on the basis of predictive algorithms actively perform a biopolitical understanding of justice as management and modulation of risks. In such a framework, justice becomes a means to maintain a perverse social homeostasis that systematically exposes disenfranchised Black and Brown populations to risk. (shrink)

For several years now, Siegfried J. Schmidt’s work has provided an important complement to the field, as it bases constructivism in a philosophical and socio-cultural context. With his new book, he develops this approach, striving to overcome simplistic models that fail to specify how human constructions come into being, to challenge traditional dualistic models, and to show how social systems emerge and function… The book provides an important, prolific and strong case for constructivism as a theory of communication.

Deep inference is a natural generalisation of the one-sided sequent calculus where rules are allowed to apply deeply inside formulas, much like rewrite rules in term rewriting. This freedom in applying inference rules allows to express logical systems that are difficult or impossible to express in the cut-free sequent calculus and it also allows for a more fine-grained analysis of derivations than the sequent calculus. However, the same freedom also makes it harder to carry out this analysis, in (...) particular it is harder to design cut elimination procedures. In this paper we see a cut elimination procedure for a deep inference system for classical predicate logic. As a consequence we derive Herbrand's Theorem, which we express as a factorisation of derivations. (shrink)

We show how to encode context-free string grammars, linear context-free tree grammars, and linear context-free rewriting systems as Abstract Categorial Grammars. These three encodings share the same constructs, the only difference being the interpretation of the composition of the production rules. It is interpreted as a first-order operation in the case of context-free string grammars, as a second-order operation in the case of linear context-free tree grammars, and as a third-order operation in the case of linear context-free (...) class='Hi'>rewriting systems. This suggest the possibility of defining an Abstract Categorial Hierarchy. (shrink)

This paper is concerned with implicit computational complexity of the exptime computable functions. Modifying the lexicographic path order, we introduce a path order EPO. It is shown that a termination proof for a term rewriting system via EPO implies an exponential bound on the lengths of derivations. The path order EPO is designed so that every exptime function is representable as a term rewrite system compatible with EPO (© 2009 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim).

We consider a deterministic rewrite system for combinatory logic over combinators , and . Terms will be represented by graphs so that reduction of a duplicator will cause the duplicated expression to be "shared" rather than copied. To each normalizing term we assign a weighting which is the number of reduction steps necessary to reduce the expression to normal form. A lambda-expression may be represented by several distinct expressions in combinatory logic, and two combinatory logic expressions are considered equivalent if (...) they represent the same lambda-expression (up to --equivalence). The problem of minimizing the number of reduction steps over equivalent combinator expressions (i.e., the problem of finding the "fastest running" combinator representation for a specific lambda-expression) is proved to be NP-complete by reduction from the "Hitting Set" problem. (shrink)

We introduce Boolean-like algebras of dimension n ($$n{\mathrm {BA}}$$ n BA s) having n constants $${{{\mathsf {e}}}}_1,\ldots,{{{\mathsf {e}}}}_n$$ e 1, …, e n, and an $$(n+1)$$ ( n + 1 ) -ary operation q (a “generalised if-then-else”) that induces a decomposition of the algebra into n factors through the so-called n-central elements. Varieties of $$n{\mathrm {BA}}$$ n BA s share many remarkable properties with the variety of Boolean algebras and with primal varieties. The $$n{\mathrm {BA}}$$ n BA s provide the (...) algebraic framework for generalising the classical propositional calculus to the case of n–perfectly symmetric–truth-values. Every finite-valued tabular logic can be embedded into such a n-valued propositional logic, $$n{\mathrm {CL}}$$ n CL, and this embedding preserves validity. We define a confluent and terminating first-order rewriting system for deciding validity in $$n{\mathrm {CL}}$$ n CL, and, via the embeddings, in all the finite tabular logics. (shrink)

Ackermann’s function can be expressed using an iterative algorithm, which essentially takes the form of a term rewriting system. Although the termination of this algorithm is far from obvious, its equivalence to the traditional recursive formulation—and therefore its totality—has a simple proof in Isabelle/HOL. This is a small example of formalising mathematics using a proof assistant, with a focus on the treatment of difficult recursions.

The paper discusses the question whether T-theories explain how it is possible to understand new sentences, or learn an infinite language, as Davidson claimed. I argue against some commentators that for explanatory power we need not require that T-theories are implicitly known or mirror cognitive structures. I note contra Davidson that the recursive nature of T-theories is not sufficient for explanatory power, since humans can work out only what is computationally tractable, and recursiveness by itself allows for intractable computational complexity. (...) I finally consider the complexity of T-theories, transformed into term rewriting systems, and find that the complexity of such systems is indeed tractable. Therefore Davidson's claim stands, even though a further condition had to be met. (shrink)

Let $R$ be a (finite) rewrite system over a (finite) signature. Let $\succ$ be a strict well-founded termination ordering on the set of terms in question so that the rules of $R$ are reducing under $\succ$ . Then $R$ is terminating. In this article it is proved for a certain class of far reaching termination orderings (of order type reaching up to the first subrecursively inaccessible ordinal, i.e. the proof-theoretic ordinal of $ID_{<\omega}$ ) that – under some reasonable assumptions which (...) are met in current applications – the derivation lengths function for $R$ is bounded by a function from the slow growing hierarchy of level determined by the order type of the underlying termination ordering. This result is a (correction of the proof of and a) strong generalization of theorem 8.1 in Cichon's article Termination orderings and complexity characterisations. Leeds, Proof Theory 1990, (Aczel, Simmons, and Wainer, editors), Cambridge University Press 1992, 171-193. (shrink)

In this paper we study the termination behavior of Russell’s description elimination rewrite system. We discuss certain claims made by Kripke (2005) in his paper concerning the possible nontermination of elimination of descriptions.

In this paper we concentrate mainly on the notion of β-pregroups, which are pregroups enriched with modality operators. β-pregroups were first proposed by Fadda [11] in 2001. The motivation to introduce them was to limit the associativity in the calculus considered. In this paper we present this new calculus in the form of a rewriting system, prove the very important feature of this system - that in a given derivation the non- expanding rules must always proceed non-contracting ones in (...) order the derivation to be minimal. We also propose a sequent system for this calculus and prove the cut elimination theorem for it. As an illustration we show how to use β-pregroups for linguistical applications. (shrink)

Second-order abstract categorial grammars (de Groote in Association for computational linguistics, 39th annual meeting and 10th conference of the European chapter, proceedings of the conference, pp. 148–155, 2001) and hyperedge replacement grammars (Bauderon and Courcelle in Math Syst Theory 20:83–127, 1987; Habel and Kreowski in STACS 87: 4th Annual symposium on theoretical aspects of computer science. Lecture notes in computer science, vol 247, Springer, Berlin, pp 207–219, 1987) are two natural ways of generalizing “context-free” grammar formalisms for string and tree (...) languages. It is known that the string generating power of both formalisms is equivalent to (non-erasing) multiple context-free grammars (Seki et al. in Theor Comput Sci 88:191–229, 1991) or linear context-free rewriting systems (Weir in Characterizing mildly context-sensitive grammar formalisms, University of Pennsylvania, 1988). In this paper, we give a simple, direct proof of the fact that second-order ACGs are simulated by hyperedge replacement grammars, which implies that the string and tree generating power of the former is included in that of the latter. The normal form for tree-generating hyperedge replacement grammars given by Engelfriet and Maneth (Graph transformation. Lecture notes in computer science, vol 1764. Springer, Berlin, pp 15–29, 2000) can then be used to show that the tree generating power of second-order ACGs is exactly the same as that of hyperedge replacement grammars. (shrink)

This paper classifies a family of grammar formalisms that extendcontext-free grammar by talking about tuples of terminal strings, ratherthan independently combining single terminal words into larger singlephrases. These include a number of well-known formalisms, such as headgrammar and linear context-free rewriting systems, but also a new formalism,(simple) literal movement grammar, which strictly extends the previouslyknown formalisms, while preserving polynomial time recognizability.The descriptive capacity of simple literal movement grammars isillustrated both formally through a weak generative capacity argument and ina (...) more practical sense by the description of conjunctive cross-serialrelative clauses in Dutch. After sketching a complexity result and drawing anumber of conclusions from the illustrations, it is then suggested that thenotion of mild context-sensitivity currently in use, that depends on therather loosely defined concept of constant growth, needs a modification toapply sensibly to the illustrated facts; an attempt at such a revision isproposed. (shrink)

This volume presents the proceedings of the workshop CSL '91 (Computer Science Logic) held at the University of Berne, Switzerland, October 7-11, 1991. This was the fifth in a series of annual workshops on computer sciencelogic (the first four are recorded in LNCS volumes 329, 385, 440, and 533). The volume contains 33 invited and selected papers on a variety of logical topics in computer science, including abstract datatypes, bounded theories, complexity results, cut elimination, denotational semantics, infinitary queries, Kleene algebra (...) with recursion, minimal proofs, normal forms in infinite-valued logic, ordinal processes, persistent Petri nets, plausibility logic, program synthesis systems, quantifier hierarchies, semantics of modularization, stable logic, term rewriting systems, termination of logic programs, transitive closure logic, variants of resolution, and many others. (shrink)

We introduce a new formulation of the axiom of dependent choice, which can be viewed as an abstract termination principle that in particular generalises recursive path orderings, the latter being fundamental tools used to establish termination of rewrite systems. We consider several variants of our termination principle, and relate them to general termination theorems in the literature.

We show how to encode context-free string grammars, linear context-free tree grammars, and linear context-free rewriting systems as Abstract Categorial Grammars. These three encodings share the same constructs, the only difference being the interpretation of the composition of the production rules. It is interpreted as a first-order operation in the case of context-free string grammars, as a second-order operation in the case of linear context-free tree grammars, and as a third-order operation in the case of linear context-free (...) class='Hi'>rewriting systems. This suggest the possibility of defining an Abstract Categorial Hierarchy. (shrink)