Computational Logic (TOCL)


Search Issue
enter search term and/or author name


ACM Transactions on Computational Logic (TOCL), Volume 14 Issue 4, November 2013

Enumeration of monadic second-order queries on trees
Wojciech Kazana, Luc Segoufin
Article No.: 25
DOI: 10.1145/2528928

We consider the enumeration problem of Monadic Second-Order (MSO) queries with first-order free variables over trees. In Bagan [2006] it was shown that this problem is in CONSTANT-DELAYlin. An enumeration problem belongs to...

Computing persistent homology within Coq/SSReflect
Jónathan Heras, Thierry Coquand, Anders Mörtberg, Vincent Siles
Article No.: 26
DOI: 10.1145/2528929

Persistent homology is one of the most active branches of computational algebraic topology with applications in several contexts such as optical character recognition or analysis of point cloud data. In this article, we report on the...

A unified semantic framework for fully structural propositional sequent systems
Ori Lahav, Arnon Avron
Article No.: 27
DOI: 10.1145/2528930

We identify a large family of fully structural propositional sequent systems, which we call basic systems. We present a general uniform method for providing (potentially, nondeterministic) strongly sound and complete Kripke-style semantics,...

Logical foundations for more expressive declarative temporal logic programming languages
Jose Gaintzarain, Paqui Lucio
Article No.: 28
DOI: 10.1145/2528931

In this article, we present a declarative propositional temporal logic programming language called TeDiLog that is a combination of the temporal and disjunctive paradigms in logic programming. TeDiLog is, syntactically, a sublanguage of the...

Three syntactic theories for combinatory graph reduction
Olivier Danvy, Ian Zerny
Article No.: 29
DOI: 10.1145/2528932

We present a purely syntactic theory of graph reduction for the canonical combinators S, K, and I, where graph vertices are represented with evaluation contexts and let expressions. We express this first syntactic theory as a storeless reduction...

Constraint satisfaction tractability from semi-lattice operations on infinite sets
Manuel Bodirsky, H. Dugald Macpherson, Johan Thapper
Article No.: 30
DOI: 10.1145/2528933

A famous result by Jeavons, Cohen, and Gyssens shows that every Constraint Satisfaction Problem (CSP) where the constraints are preserved by a semi-lattice operation can be solved in polynomial time. This is one of the basic facts for the...

Least upper bounds on the size of confluence and church-rosser diagrams in term rewriting and λ-calculus
Jeroen Ketema, Jakob Grue Simonsen
Article No.: 31
DOI: 10.1145/2528934

We study confluence and the Church-Rosser property in term rewriting and λ-calculus with explicit bounds on term sizes and reduction lengths. Given a system R, we are interested in the lengths of the reductions in the smallest...

Logical relations for a logical framework
Florian Rabe, Kristina Sojakova
Article No.: 32
DOI: 10.1145/2536740.2536741

Logical relations are a central concept used to study various higher-order type theories and occur frequently in the proofs of a wide variety of meta-theorems. Besides extending the logical relation principle to more general languages, an...

Verification of linear duration properties over continuous-time markov chains
Taolue Chen, Marco Diciolla, Marta Kwiatkowska, Alexandru Mereacre
Article No.: 33
DOI: 10.1145/2528935

Stochastic modelling and algorithmic verification techniques have been proved useful in analysing and detecting unusual trends in performance and energy usage of systems such as power management controllers and wireless sensor devices. Many...

Algebra, proof theory and applications for an intuitionistic logic of propositions, actions and adjoint modal operators
Roy Dyckhoff, Mehrnoosh Sadrzadeh, Julien Truffaut
Article No.: 34
DOI: 10.1145/2536740.2536742

We develop a cut-free nested sequent calculus as basis for a proof search procedure for an intuitionistic modal logic of actions and propositions. The actions act on propositions via a dynamic modality (the weakest precondition of program...