ACM DL

Computational Logic (TOCL)

Menu

Search Issue
enter search term and/or author name

Archive


ACM Transactions on Computational Logic (TOCL), Volume 16 Issue 2, March 2015

A Confluent Rewriting System Having No Computable, One-Step, Normalizing Strategy
Jakob Grue Simonsen
Article No.: 10
DOI: 10.1145/2699917

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
DOI: 10.1145/2699916

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
DOI: 10.1145/2699915

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...

Normal Higher-Order Termination
Jean-Pierre Jouannaud, Albert Rubio
Article No.: 13
DOI: 10.1145/2699913

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...

Layer Systems for Proving Confluence
Bertram Felgenhauer, Aart Middeldorp, Harald Zankl, Vincent Van Oostrom
Article No.: 14
DOI: 10.1145/2710017

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
DOI: 10.1145/2724711

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
DOI: 10.1145/2724712

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...

On the Variable Hierarchy of First-Order Spectra
Eryk Kopczyński, Tony Tan
Article No.: 17
DOI: 10.1145/2733376

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
DOI: 10.1145/2729979

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...