enter search term and/or author name
A system of interaction and structure
Article No.: 1
This article introduces a logical system, called BV, which extends multiplicative linear logic by a noncommutative self-dual logical operator. This extension is particularly challenging for the sequent calculus, and so far, it is not achieved...
Compilability of propositional abduction
Paolo Liberatore, Marco Schaerf
Article No.: 2
Abduction is one of the most important forms of reasoning; it has been successfully applied to several practical problems, such as diagnosis. In this article we investigate whether the computational complexity of abduction can be reduced by an...
Results on the quantitative μ-calculus qMμ
Annabelle McIver, Carroll Morgan
Article No.: 3
The μ-calculus is a powerful tool for specifying and verifying transition systems, including those with both demonic (universal) and angelic (existential) choice; its quantitative generalization qMμ extends to include...
On compositionality and its limitations
Article No.: 4
The aim of this article is to examine the applicability of a compositional method developed for a generalized product construction by Feferman and Vaught to the field of program verification.We suggest an instance of the generalized product...
Logical characterizations of heap abstractions
Greta Yorsh, Thomas Reps, Mooly Sagiv, Reinhard Wilhelm
Article No.: 5
Shape analysis concerns the problem of determining “shape invariants” for programs that perform destructive updating on dynamically allocated storage. In recent work, we have shown how shape analysis can be performed using an abstract...
Abstract canonical inference
Maria Paola Bonacina, Nachum Dershowitz
Article No.: 6
An abstract framework of canonical inference is used to explore how different proof orderings induce different variants of saturation and completeness. Notions like completion, paramodulation, saturation, redundancy elimination, and rewrite-system...
Erratum to splitting an operator: Algebraic modularity results for logics with fixpoint semantics
Joost Vennekens, David Gilis, Marc Denecker
Article No.: 7