WOLLIC
2010
Springer
13 years 10 months ago
2010
Springer
We provide a formalisation of the theory of pushdown automata (PDAs) using the HOL4 theorem prover. It illustrates how provers such as HOL can be used for mechanising complicated p...
WOLLIC
2010
Springer
13 years 10 months ago
2010
Springer
Abstract. The λ-calculus with de Bruijn indices, called λdB, assembles each α-class of λ-terms into a unique term, using indices instead of variable names. Intersection types p...
WOLLIC
2010
Springer
14 years 3 months ago
2010
Springer
sed Logic for Program Abstractions Martin Lange1 and Markus Latte2 1 Dept. of Computer Science, University of Kassel, Germany 2 Dept. of Computer Science, Ludwig-Maximilians-Univer...
WOLLIC
2010
Springer
14 years 4 months ago
2010
Springer
Proof theoretic characterizations of complexity classes are of considerable interest because they link levels of conceptual abstraction to computational complexity. We consider he...
WOLLIC
2010
Springer
14 years 4 months ago
2010
Springer
In type logical categorial grammar the analysis of an expression is a resource-conscious proof. Anaphora represents a particular challenge to this approach in that the antecedent ...
WOLLIC
2010
Springer
14 years 4 months ago
2010
Springer
Abstract. We present a modal language that includes explicit operators to count the number of elements that a model might include in the extension of a formula, and we discuss how ...
WOLLIC
2010
Springer
14 years 4 months ago
2010
Springer
The satisfiability and finite satisfiability problems for the two-variable fragment of first-order logic with counting were shown in [5] to be in NExpTime. This paper presents ...
WOLLIC
2010
Springer
14 years 4 months ago
2010
Springer
Recently, an axiomatization for functional dependencies (FDs) and multivalued dependencies (MVDs) has been established where arbitrary attributes can be specified as NOT NULL. Tha...
WOLLIC
2010
Springer
14 years 4 months ago
2010
Springer
Abstract. The intruder deduction problem for an electronic purse protocol with blind signatures is considered. The algebraic properties of the protocol are modeled by an equational...