enter search term and/or author name
A Confluent Rewriting System Having No Computable, One-Step, Normalizing Strategy
Jakob Grue Simonsen
Article No.: 10
A full and finitely generated Church-Rosser term rewriting system is presented that has no computable one-step, normalizing strategy; the system is both left- and right-linear. The result provides a negative answer to a question posed by Kennaway...
Probabilistic Event Calculus for Event Recognition
Anastasios Skarlatidis, Georgios Paliouras, Alexander Artikis, George A. Vouros
Article No.: 11
Symbolic event recognition systems have been successfully applied to a variety of application domains, extracting useful information in the form of events, allowing experts or other systems to monitor and respond when significant events are...
Optimization Modulo Theories with Linear Rational Costs
Roberto Sebastiani, Silvia Tomasi
Article No.: 12
In the contexts of automated reasoning (AR) and formal verification (FV), important decision problems are effectively encoded into Satisfiability Modulo Theories (SMT). In the last decade, efficient SMT solvers have been developed for...
We extend the termination proof methods based on reduction orderings to higher-order rewriting systems based on higher-order pattern matching. We accommodate, on the one hand, a weakly polymorphic, algebraic extension of Church’s simply...
We introduce layer systems for proving generalizations of the modularity of confluence for first-order rewrite systems. Layer systems specify how terms can be divided into layers. We establish structural conditions on those systems that imply...
Two-Variable Separation Logic and Its Inner Circle
Stéphane Demri, Morgan Deters
Article No.: 15
Separation logic is a well-known assertion language for Hoare-style proof systems. We show that first-order separation logic with a unique record field restricted to two quantified variables and no program variables is undecidable. This is among...
Efficiently Deciding μ-Calculus with Converse over Finite Trees
Pierre Genevès, Nabil Layaïda, Alan Schmitt, Nils Gesbert
Article No.: 16
We present a sound and complete satisfiability-testing algorithm and its effective implementation for an alternation-free modal μ-calculus with converse, where formulas are cycle-free and are interpreted over finite ordered trees. The time...
The spectrum of a first-order logic sentence is the set of natural numbers that are cardinalities of its finite models. In this article, we study the hierarchy of first-order spectra based on the number of variables. It has been conjectured...
Higher Homotopies in a Hierarchy of Univalent Universes
Nicolai Kraus, Christian Sattler
Article No.: 18
For Martin-Löf type theory with a hierarchy U0:U1:U2:… of univalent universes, we show that Un is not an n-type. Our construction also solves the problem of finding a type that...