Search ACM DL

Search Issue

enter search term and/or author name

**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 **EM**_{1}-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 STA_{B}, that characterizes the PSPACE class. This system is obtained by extending STA, a type assignment for lambda-calculus inspired by...