enter search term and/or author name
A PSPACE-complete first-order fragment of computability logic
Matthew S. Bauer
Article No.: 1
In a recently launched research program for developing logic as a formal theory of (interactive) computability, several very interesting logics have been introduced and axiomatized. These fragments of the larger Computability Logic aim not only to...
Improved witnessing and local improvement principles for second-order bounded arithmetic
Arnold Beckmann, Samuel R. Buss
Article No.: 2
This article concerns the second-order systems U12 and V12 of bounded arithmetic, which have proof-theoretic strengths corresponding to polynomial-space and exponential-time computation. We formulate...
Algebra-coalgebra duality in brzozowski's minimization algorithm
Filippo Bonchi, Marcello M. Bonsangue, Helle H. Hansen, Prakash Panangaden, Jan J. M. M. Rutten, Alexandra Silva
Article No.: 3
We give a new presentation of Brzozowski's algorithm to minimize finite automata using elementary facts from universal algebra and coalgebra and building on earlier work by Arbib and Manes on a categorical presentation of Kalman duality between...
Non-finite axiomatizability of dynamic topological logic
Article No.: 4
Dynamic topological logic (DTL) is a polymodal logic designed for reasoning about dynamic topological systems. These are pairs 〈 X, f〉, where X is a topological space and f:X →...
Quantifier-free interpolation in combinations of equality interpolating theories
Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise
Article No.: 5
The use of interpolants in verification is gaining more and more importance. Since theories used in applications are usually obtained as (disjoint) combinations of simpler theories, it is important to modularly reuse interpolation algorithms for...
Degree lower bounds of tower-type for approximating formulas with parity quantifiers
Albert Atserias, Anuj Dawar
Article No.: 6
Kolaitis and Kopparty have shown that for any first-order formula with parity quantifiers over the language of graphs, there is a family of multivariate polynomials of constant-degree that agree with the formula on all but a...
Using tableau to decide description logics with full role negation and identity
Renate A. Schmidt, Dmitry Tishkovsky
Article No.: 7
This article presents a tableau approach for deciding expressive description logics with full role negation and role identity. We consider the description logic ALBOid, which is ALC extended with the Boolean role operators, inverse of...
Extending two-variable logic on data trees with order on data values and its automata
Article No.: 8
Data trees are trees in which each node, besides carrying a label from a finite alphabet, also carries a data value from an infinite domain. They have been used as an abstraction model for reasoning tasks on XML and verification. However, most...
We systematically investigate the complexity of model checking the existential positive fragment of first-order logic. In particular, for a set of existential positive sentences, we consider model checking where the sentence is restricted to fall...
A resolution calculus for the branching-time temporal logic CTL
Lan Zhang, Ullrich Hustadt, Clare Dixon
Article No.: 10
The branching-time temporal logic CTL is useful for specifying systems that change over time and involve quantification over possible futures. Here we present a resolution calculus for CTL that involves the translation of formulae to a normal form...