Related papers: Definitions by rewriting in the Calculus of Constr…

Constructor rewriting systems are said to be cons-free if, roughly, constructor terms in the right-hand sides of rules are subterms of constructor terms in the left-hand side; the computational intuition is that rules cannot build new data…

What is ergonomic syntax for relations? In this first paper in a series of two, to answer the question we define regular calculi: a suitably structured functor from a category representing the syntax of regular logic to the category of…

We present a comprehensive programme analysing the decomposition of proof systems for non-classical logics into proof systems for other logics, especially classical logic, using an algebra of constraints. That is, one recovers a proof…

Users of program analyses expect that results change predictably in response to changes in their programs, but many analyses fail to provide such robustness. This paper introduces a theoretical framework that provides a unified language to…

In the former article "Formal mathematical systems including a structural induction principle" we have presented a unified theory for formal mathematical systems including recursive systems closely related to formal grammars, including the…

A logic is presented for reasoning on iterated sequences of formulae over some given base language. The considered sequences, or "schemata", are defined inductively, on some algebraic structure (for instance the natural numbers, the lists,…

In this paper, we use a categorical and functorial set up to model the syntax and inference of logics with algebraic signature, extending previous works on algebraisation of logics. The main feature of this work is that structurality, or…

A version of the situation calculus in which situations are represented as first-order terms is presented. Fluents can be computed from the term structure, and actions on the situations correspond to rewrite rules on the terms. Actions that…

We present a translation function from nominal rewriting systems (NRSs) to combinatory reduction systems (CRSs), transforming closed nominal rules and ground nominal terms to CRSs rules and terms, respectively, while preserving the…

We develop a class of algebraic interpretations for many-sorted and higher-order term rewriting systems that takes type information into account. Specifically, base-type terms are mapped to \emph{tuples} of natural numbers and higher-order…

While a mature body of work supports the study of rewriting systems, abstract tools for Probabilistic Rewriting are still limited. In this paper we study the question of uniqueness of the result (unique limit distribution), and develop a…

Several types of term rewriting systems can be distinguished by the way their rules overlap. In particular, we define the classes of prefix, suffix, bottom-up and top-down systems, which generalize similar classes on words. Our aim is to…

This article shows a correspondence between abstract interpretation of imperative programs and the refinement calculus: in the refinement calculus, an abstract interpretation of a program is a specification which is a function. This…

Meseguer's rewriting logic and the rewriting logic CRWL are two well-known approaches to rewriting as logical deduction that, despite some clear similarities, were designed with different objectives. Here we study the relationships between…

The notion of class is ubiquitous in computer science and is central in many formalisms for the representation of structured knowledge used both in knowledge representation and in databases. In this paper we study the basic issues…

Software and hardware architectures are prone to modifications. We demonstrate how a mathematically founded powerful refinement calculus for a class of architectures, namely pipe and filter architectures, can be used to modify a system in a…

In deduction modulo, a theory is not represented by a set of axioms but by a congruence on propositions modulo which the inference rules of standard deductive systems---such as for instance natural deduction---are applied. Therefore, the…

Logically constrained term rewriting is a rewriting framework that supports built-in data structures such as integers and bit vectors. Recently, constrained terms play a key role in various analyses and applications of logically constrained…

Logic is the science of correct inferences and a logical system is a tool to prove assertions in a certain logic in a correct way. There are many logical systems, and many ways of formalizing them, e.g., using natural deduction or sequent…

Properties expressed as the provability of a first-order sentence can be disproved by just finding a model of the negation of the sentence. This fact, however, is meaningful in restricted cases only, depending on the shape of the sentence…