Catálogo de publicaciones - libros

The abstract categorial grammars (ACGs, for short) are a type-theoretic grammatical formalism intended for the description of natural languages [1]. It is based on the implicative fragment of multiplicative linear logic, which results in a rather simple framework.

The use of formal methods provides confidence in the correctness of developments. Yet one may argue about the actual level of confidence obtained when the method itself – or its implementation – is not formally checked. We address this question for the , a widely used formal method that allows for the derivation of correct programs from specifications. Through a deep embedding of the logic in , we check the theory but also implement tools. Both aspects are illustrated by the description of a proved prover for the logic.

The Description Logics underpinning OWL impose a well-known syntactic restriction in order to preserve decidability: they do not allow to use non-simple roles—that is, transitive roles or their super-roles—in number restrictions. When modeling composite objects, for example in bio-medical ontologies, this restriction can pose problems.X

Therefore, we take a closer look at the problem of counting over non-simple roles. On the one hand, we sharpen the known undecidability results and demonstrate that: (i) for DLs with inverse roles, counting over non-simple roles leads to undecidability even when there is only one role in the language; (ii) for DLs without inverses, two transitive and an arbitrary role are sufficient for undecidability. On the other hand, we demonstrate that counting over non-simple roles does not compromise decidability in the absence of inverse roles provided that certain restrictions on role inclusion axioms are satisfied.

The guarded fragment of first-order logic, GF, enjoys the finite model property, so the satisfiability and the finite satisfiability problems coincide.

We are concerned with two extensions of the two-variable guarded fragment that do not possess the finite model property, namely, GF with equivalence and GF with transitive guards. We prove that in both cases every finitely satisfiable formula has a model of at most double exponential size w.r.t. its length.

To obtain the result we invent a strategy of building finite models that are formed from a number of multidimensional grids placed over a cylindrical surface. The construction yields a -upper bound on the complexity of the finite satisfiability problem for these fragments. For the case with equivalence guards we improve the bound to .

We study the data complexity of instance checking and conjunctive query answering in the family of description logics, with a particular emphasis on the boundary of tractability. We identify a large number of intractable extensions of , but also show that in , the extension of with inverse roles and global functionality, conjunctive query answering is tractable regarding data complexity. In contrast, already instance checking in extended with only inverse roles or global functionality is -complete regarding combined complexity.

The Knuth-Bendix ordering is usually preferred over the lexicographic path ordering in successful implementations of resolution and superposition, but it is incompatible with certain requirements of hierarchic superposition calculi. Moreover, it does not allow non-linear definition equations to be oriented in a natural way. We present an extension of the Knuth-Bendix ordering that makes it possible to overcome these restrictions.

Proof nets are a parallel syntax for sequential proofs of linear logic, firstly introduced by Girard in 1987. Here we present and intrinsic (geometrical) characterization of proof nets, that is a correctness criterion (an algorithm) for checking those proof structures which correspond to proofs of the purely multiplicative and additive fragment of linear logic. This criterion is formulated in terms of simple graph rewriting rules and it extends an initial idea of a retraction correctness criterion for proof nets of the purely multiplicative fragment of linear logic presented by Danos in his Thesis in 1990.

We investigate techniques for supporting inductive definitions (IDs) in SAT, and report on an implementation, called , of the resulting solver. This solver was first introduced in [11], as a part of a declarative problem solving framework. We go about our investigation by proposing a new formulation of the semantics of IDs as presented in [2]. This new formulation suggests a way to perform the computational task involved, resulting in an algorithm supporting IDs. We show in detail how to integrate our algorithm with traditional SAT solving techniques. We also point out the similarities with another algorithm that was recently developed for ASP [1]. Indeed, our formulation reveals a very tight relation with stable model semantics. We conclude by an experimental validation of our approach using .

Differential interaction nets (DIN) have been introduced by Thomas Ehrhard and Laurent Regnier as an extension of linear logic proof-nets. We prove that DIN enjoy an internal separation property: given two different normal nets, there exists a dual net separating them, in analogy with Böhm’s theorem for the λ− calculus. Our result implies in particular the faithfulness of every non-trivial denotational model of DIN (such as Ehrhard’s finiteness spaces). We also observe that internal separation does not hold for linear logic proof-nets: our work points out that this failure is due to the fundamental asymmetry of linear logic exponential modalities, which are instead completely symmetric in DIN.

In this paper, we continue the recently started work on integrating action formalisms with description logics (DLs), by investigating planning in the context of DLs. We prove that the plan existence problem is decidable for actions described in fragments of . More precisely, we show that its computational complexity coincides with the one of projection for DLs between and if operators contain only unconditional post-conditions. If we allow for conditional post-conditions, the plan existence problem is shown to be in 2-.