Logical Foundations of Computer Science

We are concerned with the subvariety of commutative, bounded, and integral residuated lattices, satisfying divisibility and prelinearity, namely, BL-algebras. We give an explicit combinatorial description of the category that is dual to finite BL-algebras. Building on this, we obtain detailed structural information on the locally finite subvarieties of BL-algebras that are analogous to Grigolia’s subvarieties of finite-valued MV-algebras. As an illustration of the power of the finite duality presented here, we give an exact recursive formula for the cardinality of free finitely generated algebras in such varieties.

Memory logics are a family of modal logics in which standard relational structures are augmented with data structures and additional operations to modify and query these structures. In this paper we present sound and complete axiomatizations for some members of this family. We analyze the use of nominals to achieve completeness, and present one example in which they can be avoided.

Canonical propositional Gentzen-type calculi are a natural class of systems which in addition to the standard axioms and structural rules have only logical rules where exactly one occurrence of a connective is introduced and no other connective is mentioned. Cut-elimination in such systems is fully characterized by a syntactic constructive criterion of coherence. In this paper we extend the theory of canonical systems to the considerably more general class of

signed calculi

. We show that the extended criterion of coherence fully characterizes only analytic cut-elimination in such calculi, while for characterizing strong and standard cut-elimination a stronger criterion of density is required. Modular semantics based on non-deterministic matrices are provided for every coherent canonical signed calculus.

In this paper we study several properties of the Exogenous Probabilistic Propositional Logic

(EPPL )

, a logic for reasoning about probabilities, with the purpose of introducing a temporal version - Exogenous Probabilistic Linear Temporal Logic

(EPLTL)

. In detail, we give a small model theorem for

EPPL

and introduce a satisfaction and a model checking algorithm for both

EPPL

and

EPLTL

. We are also able to provide a (weakly) complete calculus for

EPLTL

. Finally, we conclude by pointing out some future work.

In this paper we consider languages of labelled

N

-free posets over countable and scattered linear orderings. We prove that a language of such posets is series-rational if and only if it is recognizable by a finite depth-nilpotent algebra if and only if it is bounded-width and monadic second-order definable. This extends previous results on languages of labelled

N

-free finite and

ω

-posets and on languages of labelled countable and scattered linear orderings.

We explore an intuitionistic fragment of Artëmov’s

Logic of Proofs

as a type system for a programming language for

mobile units

. Such units consist of both a code and certificate component. Dubbed the

Certifying Mobile Calculus

, our language caters for both code and certificate development in a unified theory. In the same way that mobile code is constructed out of code components and extant type systems track local resource usage to ensure the mobile nature of these components, our system

additionally

ensures correct

certificate construction

out of certificate components. We present proofs of type safety and strong normalization for a run-time system based on an abstract machine.

We extend the alternating-time temporal logics

ATL

and

ATL

* with

strategy contexts

and

memory constraints

: the first extension makes strategy quantifiers to not “forget” the strategies being executed by the other players. The second extension allows strategy quantifiers to restrict to memoryless or bounded-memory strategies.

We first consider expressiveness issues. We show that our logics can express important properties such as equilibria, and we formally compare them with other similar formalisms (

ATL

,

ATL

*, Game Logic, Strategy Logic, ...). We then address the problem of model-checking for our logics, especially we provide a

PSPACE

algorithm for the sublogics involving only memoryless strategies and an

EXPSPACE

algorithm for the bounded-memory case.

We recently introduced an extensional model of the pure

λ

-calculus living in a canonical cartesian closed category of sets and relations [6]. In the present paper, we study the non-deterministic features of this model. Unlike most traditional approaches, our way of interpreting non-determinism does not require any additional powerdomain construction. We show that our model provides a straightforward semantics of

non-determinism

(

may

convergence) by means of

unions

of interpretations, as well as of

parallelism

(

must

convergence) by means of a binary, non-idempotent operation available on the model, which is related to the

mix rule

of Linear Logic. More precisely, we introduce a

λ

-calculus extended with non-deterministic choice and parallel composition, and we define its operational semantics (based on the

may

and

must

intuitions underlying our two additional operations). We describe the interpretation of this calculus in our model and show that this interpretation is sensible with respect to our operational semantics: a term converges if, and only if, it has a non-empty interpretation.

Justification Logic studies epistemic and provability phenomena by introducing justifications/proofs into the language in the form of justification terms. Pure justification logics serve as counterparts of traditional modal epistemic logics, and hybrid logics combine epistemic modalities with justification terms. The computational complexity of pure justification logics is typically lower than that of the corresponding modal logics. Moreover, the so-called reflected fragments, which still contain complete information about the respective justification logics, are known to be in NP for a wide range of justification logics, pure and hybrid alike. This paper shows that, under reasonable additional restrictions, these reflected fragments are NP-complete, thereby proving a matching lower bound.

Pure, or type-free, Linear Logic proof nets are Turing complete once cut-elimination is considered as computation. We introduce

modal impredicativity

as a new form of impredicativity causing cut-elimination to be problematic from a complexity point of view. Modal impredicativity occurs when, during reduction, the conclusion of a residual of a box

b

interacts with a node that belongs to the proof net

inside

another residual of

b

. Technically speaking,

superlazy reduction

is a new notion of reduction that allows to control modal impredicativity. More specifically, superlazy reduction replicates a box only when all its copies are opened. This makes the overall cost of reducing a proof net finite and predictable. Specifically, superlazy reduction applied to any pure proof nets takes primitive recursive time. Moreover, any primitive recursive function can be computed by a pure proof net via superlazy reduction.

We introduce and illustrate a graph calculus for proving and deciding the positive identities and inclusions of fork algebras, i.e., those without occurrences of complementation. We show that this graph calculus is sound, complete and decidable. Moreover, the playful nature of this calculus renders it much more intuitive than its equational counterpart.

In this paper, we show how Ehrenfeucht-Fraïssé games can be successfully exploited to compare (finite) strings. More precisely, we give necessary and sufficient conditions for Spoiler/Duplicator to win games played on finite structures with a limited order relation, that lies in between the successor relation and the usual (linear) order relation, and a finite number of unary predicates. On the basis of such conditions, we outline a polynomial (in the size of the input strings) algorithm to compute the “remoteness” of a game and to determine the optimal strategies/moves for both players.

We propose axiomatizations of monadic second-order logic (

MSO

), monadic transitive closure logic (

FO(TC

1

)

) and monadic least fixpoint logic (

FO(LFP

1

)

) on finite node-labeled sibling-ordered trees. We show by a uniform argument, that our axiomatizations are complete, i.e., in each of our logics, every formula which is valid on the class of finite trees is provable using our axioms. We are interested in this class of structures because it allows to represent basic structures of computer science such as XML documents, linguistic parse trees and treebanks. The logics we consider are rich enough to express interesting properties such as reachability. On arbitrary structures, they are well known to be not recursively axiomatizable.

We study the multiagent epistemic logic

CMAEL(CD)

with operators for common and distributed knowledge for all coalitions of agents. We introduce Hintikka structures for this logic and prove that satisfiability in such structures is equivalent to satisfiability in standard models. Using this result, we design an incremental tableau based decision procedure for testing satisfiability in

CMAEL(CD)

.

This work defines an extension CERES

2

of the first-order cut-elimination method CERES to the subclass of sequent calculus proofs in second-order logic using quantifier-free comprehension. This extension is motivated by the fact that cut-elimination can be used as a tool to extract information from real mathematical proofs, and often a crucial part of such proofs is the definition of sets by formulas. This is expressed by the comprehension axiom scheme, which is representable in second-order logic. At the core of CERES

2

lies the production of a set of clauses CL(

ϕ

) from a proof

ϕ

that is always unsatisfiable. From a resolution refutation

γ

of CL(

ϕ

), a proof without essential cuts can be constructed. The main theoretical obstacle in the extension of CERES to second-order logic is the construction of this proof from

γ

. This issue is solved for the subclass considered in this paper. Moreover, we discuss the problems that have to be solved to extend CERES

2

to the complete class of second-order proofs. Finally, the method is applied to a simple mathematical proof that involves induction and comprehension and the resulting proof is analyzed.

The admissible rules of a logic are those rules under which the set of theorems of the logic is closed. In a previous paper by the authors, formal systems for deriving the admissible rules of Intuitionistic Logic and a class of modal logics were defined in a proof-theoretic framework where the basic objects of the systems are sequent rules. Here, the framework is extended to cover derivability of the admissible rules of intermediate logics and a wider class of modal logics, in this case, by taking hypersequent rules as the basic objects.

Starting from Girard’s seminal paper on light linear logic (LLL), a number of works investigated on systems derived from linear logic to capture polynomial time computation within the computation-as-cut-elimination paradigm.

The original syntax of LLL is too complicated, mainly because one has to deal with sequents which not just consist of formulas but also of ‘blocks’ of formulas. We circumvent the complications of ‘blocks’ by introducing a new modality

$\nabla$

which is exclusively in charge of ‘additive blocks’. The most interesting feature of this purely multiplicative

$\nabla$

is the possibility of the second-order encodings of additive connectives.

The resulting system (with the traditional syntax), called Easy-LLL, is still powerful to represent any deterministic polynomial time computations in purely logical terms. Unlike the original LLL, Easy-LLL admits polynomial time strong normalization, namely, cut elimination terminates in a

unique way

in polytime by any choice of cut reduction strategies.

We present

${\mathbf{FixIt}}{\mathbb{(ALC)}}$

, a novel procedure for deciding knowledge base (KB) satisfiability in the Fuzzy Description Logic (FDL)

${\mathbb{ALC}}$

.

${\mathbf{FixIt}}{\mathbb{(ALC)}}$

does not search for tree-structured models as in tableau-based proof procedures, but embodies a (greatest) fixpoint-computation of canonical models that are not necessarily tree-structured, based on a type-elimination process. Soundness, completeness and termination are proven and the runtime and space complexity are discussed. We give a precise characterization of the worst-case complexity of deciding KB satisfiability (as well as related terminological and assertional reasoning tasks) in

${\mathbb{ALC}}$

in the general case and show that our method yields a worst-case optimal decision procedure (under reasonable assumptions). To the best of our knowledge it is the first

fixpoint-based

decision procedure for FDLs, hence introducing a new class of inference procedures into FDL reasoning.

We address the problem of quantitative comparison of classical and intuitionistic logics within the language of the full propositional system. We apply two different approaches, to estimate the asymptotic fraction of intuitionistic tautologies among classical tautologies, obtaining the same results for both. Our results justify informal statements such as “about 5/8 of classical tautologies are intuitionistic”.

Justification Logic is a new generation of epistemic logics which along with the traditional modal knowledge/belief operators also consider justification assertions ‘

t

is a justification for

F

.’ In this paper, we introduce a prefixed tableau system for one of the major logics of this kind

S4LPN

, which combines the logic of proofs (

LP

) and epistemic logic

S4

with an explicit negative introspection principle

$\neg t\!:\! F \to \Box \neg t\!:\! F$

. We show that the prefixed tableau system for

S4LPN

is sound and complete with respect to Fitting-style semantics. We also introduce a hypersequent calculus

HS4LPN

and show that

HS4LPN

is complete as far as we confine ourselves to a case where only a single formula is to be proven. We establish this fact by using a translation from the prefixed tableau system to the hypersequent calculus. This completeness result gives us a semantic proof of cut-admissibility for

S4LPN

under the aforementioned restriction.

Just as forcing, or Boolean-valued models, produce a model of ZF (when the meta-theory is, or the ground model satisfies, ZF), so do Heyting-valued models satisfy IZF, which stands for Intuitionistic ZF, the standard constructive re-working of the ZF axioms. In this paper, a variant model is introduced (with truth values the Heyting algebra of open sets of a topological space), along with a correspondingly revised forcing or satisfaction relation. Such a model is shown to satisfy only a fragment of IZF. Natural properties of the underlying topological space are shown to imply stronger closure properties of the model. (It is impossible, except in trivial cases, for Power Set to be satisfied.) This semantics generalizes the second model of [9], which is the current semantics for the special case of the underlying topological space being

${\mathbb R}$

.

In answer set programming (ASP), one does not allow the use of function symbols. Disallowing function symbols avoids the problem of having logic programs which have stable models of excessively high complexity. For example, Marek, Nerode, and Remmel showed that there exist finite predicate logic programs which have stable models but which have no hyperarithmetic stable model. Of course, by eliminating function symbols, one loses a lot of expressive power in the language. In particular, it is difficult to directly reason about infinite sets in ASP.

Blair, Marek, and Remmel [BMR08] developed an extension of logic programming called

set based logic programming

. In the theory of set based logic programming, the atoms represent subsets of a fixed universe

X

and one is allowed to compose the one-step consequence operator with a monotonic idempotent operator

O

so as to ensure that the analogue of stable models are always closed under

O

. We show that if the sets represented by the atoms in a finite set based program

P

are languages accepted by finite automaton, and the operators involved in the construction have a certain natural property, then all the stable models of

P

are languages accepted by finite automaton and one can effectively check whether a language accepted by a finite automaton is a stable model of the set based logic program. Thus in this setting, one can effectively reason about certain classes of infinite sets.

We give a sound and complete labeled natural deduction system for an interesting fragment of

$\mathit{CTL^*}$

, namely the until-free version of

$\mathit{BCTL^*}$

. The logic

$\mathit{BCTL^*}$

is obtained by referring to a more general semantics than that of

$\mathit{CTL^*}$

, where we only require that the set of paths in a model is closed under taking suffixes (i.e. is suffix-closed) and is closed under putting together a finite prefix of one path with the suffix of any other path beginning at the same state where the prefix ends (i.e. is fusion-closed). In other words, this logic does not enjoy the so-called limit-closure property of the standard

$\mathit{CTL^*}$

validity semantics.

In [1], Fitting showed that the standard hierarchy of logics of justified knowledge is conservative (e.g. a logic with positive introspection operator ! is conservative over the logic without !). We do the same with most logics of justified belief, but taking a semantic approach rather than Fitting’s syntactic one. A brief example shows that conservativity does not hold for logics of justified consistent belief.

We present a foundational framework, which we call D, unifying a lazy programming language with an impredicative constructive set theory IZF

R

by means of dependent types. We show that unification brings many benefits to both worlds. First, D supports two paramount paradigms of creating reliable software: correctness by construction and post-construction verification, while retaining the expressiveness of set theory. Second, D provides new expressive power, which makes it possible to internalize and prove

inside

D the standard meta-theoretic properties of constructive systems, such as Numerical Existence Property and Program Extraction. Finally, computation arising from the programming language significantly enriches set theory, as we show that D is stronger than IZF

R

and that its real numbers behave in a better way.

In this paper we prove that the derivability problems for product-free Lambek calculus and product-free Lambek calculus allowing empty premises are NP-complete. Also we introduce a new derivability characterization for these calculi.

Bounded phase multi-stack pushdown automata have been studied recently. In this paper we show that parity games over bounded phase multi-stack pushdown systems are effectively solvable and winning strategy in these games can be effectively synthesized. We show some applications of our result, including a new proof of a known result that emptiness problem for bounded phase multi-stack automata is decidable.

Information systems support data privacy by granting access only to certain (public) views. The data privacy problem is to decide whether hidden (private) information may be inferred from the public views and some additional general background knowledge. We study the problem of provable privacy in the context of

$\mathcal{ALC}$

knowledge bases. First we show that the

$\mathcal{ALC}$

privacy problem wrt. concept retrieval and subsumption queries is ExpTime-complete. Then we provide a sufficient condition for data privacy that can be checked in PTime.

In our former work [K. Tadaki, Local Proceedings of CiE 2008, pp. 425–434, 2008], we developed a statistical mechanical interpretation of algorithmic information theory by introducing the notion of thermodynamic quantities, such as free energy

F

(

T

), energy

E

(

T

), and statistical mechanical entropy

S

(

T

), into the theory. We then discovered that, in the interpretation, the temperature

T

equals to the partial randomness of the values of all these thermodynamic quantities, where the notion of partial randomness is a stronger representation of the compression rate by program-size complexity. Furthermore, we showed that this situation holds for the temperature itself as a thermodynamic quantity. Namely, the computability of the value of partition function

Z

(

T

) gives a sufficient condition for

T

 ∈ (0,1) to be a fixed point on partial randomness. In this paper, we show that the computability of each of all the thermodynamic quantities above gives the sufficient condition also. Moreover, we show that the computability of

F

(

T

) gives completely different fixed points from the computability of

Z

(

T

).

We study computational aspects of a probabilistic logic based on a well-known model of induction by Valiant. We prove that for this paraconsistent logic the set of valid formulas is undecidable.

A bialgebra is a structure which is simultaneously an algebra and a coalgebra, such that the algebraic and coalgebraic parts are “compatible”. In this paper, we apply the defining diagrams of algebras, coalgebras, and bialgebras to categories of semimodules and semimodule homomorphisms over a commutative semiring. We then show that formal language theory and the theory of bialgebras have essentially undergone “convergent evolution”. For example, formal languages correspond to elements of dual algebras of coalgebras, automata are “pointed representation objects” of algebras, automaton morphisms are instances of linear intertwiners, and a construction from the theory of bialgebras shows how to run two automata in parallel. We also show how to associate an automaton with an arbitrary algebra, which in the classical case yields the automaton whose states are formal languages and whose transitions are given by language differentiation.