enter search term and/or author name
Nominal Unification from a Higher-Order Perspective
Jordi Levy, Mateu Villaret
Article No.: 10
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
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...
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
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
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
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
Article No.: 16
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
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...
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...