ACM DL

Computational Logic (TOCL)

Menu

Search Issue
enter search term and/or author name

Archive


ACM Transactions on Computational Logic (TOCL), Volume 13 Issue 2, April 2012

Nominal Unification from a Higher-Order Perspective
Jordi Levy, Mateu Villaret
Article No.: 10
DOI: 10.1145/2159531.2159532

Nominal logic is an extension of first-order logic with equality, name-binding, renaming via name-swapping and freshness of names. Contrarily to lambda-terms, in nominal terms, bindable names, called atoms, and instantiable variables are...

Interactive Realizers: A New Approach to Program Extraction from Nonconstructive Proofs
Stefano Berardi, Ugo de’Liguoro
Article No.: 11
DOI: 10.1145/2159531.2159533

We propose a realizability interpretation of a system for quantier free arithmetic which is equivalent to the fragment of classical arithmetic without nested quantifiers, called here EM1-arithmetic. We interpret classical...

Model Checking of Recursive Probabilistic Systems
Kousha Etessami, Mihalis Yannakakis
Article No.: 12
DOI: 10.1145/2159531.2159534

Recursive Markov Chains (RMCs) are a natural abstract model of procedural probabilistic programs and related systems involving recursion and probability. They succinctly define a class of denumerable Markov chains that generalize several other...

Annotated Probabilistic Temporal Logic: Approximate Fixpoint Implementation
Paulo Shakarian, Gerardo I. Simari, V. S. Subrahmanian
Article No.: 13
DOI: 10.1145/2159531.2159535

Annotated Probabilistic Temporal (APT) logic programs support building applications where we wish to reason about statements of the form “Formula G becomes true with a probability in the range [L, U] within (or in...

Simplification Rules for Intuitionistic Propositional Tableaux
Mauro Ferrari, Camillo Fiorentini, Guido Fiorino
Article No.: 14
DOI: 10.1145/2159531.2159536

The implementation of a logic requires, besides the definition of a calculus and a decision procedure, the development of techniques to reduce the search space. In this article we introduce some simplification rules for Intuitionistic...

Complexity of Data Dependence Problems for Program Schemas with Concurrency
Sebastian Danicic, Robert M. Hierons, Michael R. Laurence
Article No.: 15
DOI: 10.1145/2159531.2159537

The problem of deciding whether one point in a program is data dependent upon another is fundamental to program analysis and has been widely studied. In this article we consider this problem at the abstraction level of program schemas in...

On the Relative Strength of Pebbling and Resolution
Jakob Nordström
Article No.: 16
DOI: 10.1145/2159531.2159538

The last decade has seen a revival of interest in pebble games in the context of proof complexity. Pebbling has proven to be a useful tool for studying resolution-based proof systems when comparing the strength of different subsystems, showing...

The Complexity of Reasoning for Fragments of Autoepistemic Logic
Nadia Creignou, Arne Meier, Heribert Vollmer, Michael Thomas
Article No.: 17
DOI: 10.1145/2159531.2159539

Autoepistemic logic extends propositional logic by the modal operator L. A formula ϕ that is preceded by an L is said to be “believed.” The logic was introduced by Moore in 1985 for modeling an ideally...

An Implicit Characterization of PSPACE
Marco Gaboardi, Jean-Yves Marion, Simona Ronchi Della Rocca
Article No.: 18
DOI: 10.1145/2159531.2159540

We present a type system for an extension of lambda calculus with a conditional construction, named STAB, that characterizes the PSPACE class. This system is obtained by extending STA, a type assignment for lambda-calculus inspired by...