main-content

Edited in collaboration with FoLLI, the Association of Logic, Language and Information, this book constitutes the 4th volume of the FoLLI LNAI subline; containing the refereed proceedings of the 16h International Workshop on Logic, Language, Information and Computation, WoLLIC 2009, held in Tokyo, Japan, in June 2009.

The 25 revised full papers presented together with six tutorials and invited talks were carefully reviewed and selected from 57 submissions. The papers cover some of the most active areas of research on the frontiers between computation, logic, and linguistics, with particular interest in cross-disciplinary topics. Typical areas of interest are: foundations of computing and programming; novel computation models and paradigms; broad notions of proof and belief; formal methods in software and hardware development; logical approach to natural language and reasoning; logics of programs, actions and resources; foundational aspects of information organization, search, flow, sharing, and protection.

### A Characterisation of Definable NP Search Problems in Peano Arithmetic

The complexity class of ≺

-bounded local search problems with goals

is introduced for well-orderings ≺, and is used to give a characterisation of definable

NP

search problems in Peano Arithmetic.

Arnold Beckmann

### Algebraic Valuations as Behavioral Logical Matrices

The newly developed behavioral approach to the algebraization of logics extends the applicability of the methods of algebraic logic to a wider range of logical systems, namely encompassing many-sorted languages and non-truth-functionality. However, where a logician adopting the traditional approach to algebraic logic finds in the notion of a logical matrix the most natural semantic companion, a correspondingly suitable tool is still lacking in the behavioral setting. Herein, we analyze this question and set the ground towards adopting an algebraic formulation of valuation semantics as the natural generalization of logical matrices to the behavioral setting, by establishing a few simple but promising results. For illustration, we will use da Costa’s paraconsistent logic

$\mathcal{C}_1$

.

Carlos Caleiro, Ricardo Gonçalves

### Query Answering in Description Logics: The Knots Approach

In the recent years, query answering over Description Logic (DL) knowledge bases has been receiving increasing attention, and various methods and techniques have been presented for this problem. In this paper, we consider knots, which are an instance of the mosaic technique from Modal Logic. When annotated with suitable query information, knots are a flexible tool for query answering that allows for solving the problem in a simple and intuitive way. The knot approach yields optimal complexity bounds, as we illustrate on the DLs

$\mathcal {ALCH}$

and

$\mathcal{ALCHI}$

, and can be easily extended to accommodate other constructs.

Thomas Eiter, Carsten Lutz, Magdalena Ortiz, Mantas Šimkus

### Mathematical Logic for Life Science Ontologies

We discuss how concepts and methods introduced in mathematical logic can be used to support the engineering and deployment of life science ontologies. The required applications of mathematical logic are not straighforward and we argue that such ontologies provide a new and rich family of logical theories that wait to be explored by logicians.

Carsten Lutz, Frank Wolter

### Recognizability in the Simply Typed Lambda-Calculus

We define a notion of recognizable sets of simply typed

λ

-terms that extends the notion of recognizable sets of strings or trees. This definition is based on finite models. Using intersection types, we generalize the notions of automata for strings and trees so as to grasp recognizability for

λ

-terms. We then expose the closure properties of this notion and present some of its applications.

Sylvain Salvati

### Logic-Based Probabilistic Modeling

After briefly mentioning the historical background of PLL/ SRL, we examine PRISM, a logic-based modeling language, as an instance of PLL/SRL research. We first look at the distribution semantics, PRISM’s semantics, which defines a probability measure on a set of possible Herbrand models. We then mention characteristic features of PRISM as a tool for probabilistic modeling.

Taisuke Sato

### Completions of Basic Algebras

We discuss completions of basic algebras. We prove that the ideal completion of a basic algebra is also a basic algebra. It will be shown that basic algebras are not closed under MacNeille completions. By adding the join-infinite distributive law to basic algebras, we will show that these kind of basic algebras are closed under the closed ideal completion and moreover any other regular completions of these algebras are isomorphic to the closed ideal completion. As an application we establish an algebraic completeness theorem for a logic weaker than Visser’s basic predicate logic,

BQL

, a proper subsystem of intuitionistic predicate logic,

IQL

.

### Transformations via Geometric Perspective Techniques Augmented with Cycles Normalization

A normalization procedure is presented for a classical natural deduction (

ND

) proof system. This proof system, called

N-Graphs

, has a multiple conclusion proof structure where cycles are allowed. With this, we have developed a thorough treatment of cycles, including cycles normalization via an algorithm. We also demonstrate the usefulness of the graphical framework of

N-Graphs

, where derivations are seen as digraphs. We use geometric perspective techniques to establish the normalization mechanism, thus giving a direct normalization proof.

Gleifer V. Alves, Anjolina G. de Oliveira, Ruy de Queiroz

### Observational Completeness on Abstract Interpretation

In the theory of abstract interpretation, we introduce the observational completeness, which extends the common notion of completeness. A domain is complete when abstract computations are as precise as concrete computations. A domain is observationally complete for an observable

π

when abstract computations are as precise as concrete computations, if we only look at properties in

π

. We prove that continuity of state-transition functions ensures the existence of the least observationally complete domain. When state-transition functions are additive, the least observationally complete domain boils down to the complete shell.

Gianluca Amato, Francesca Scozzari

### SAT in Monadic Gödel Logics: A Borderline between Decidability and Undecidability

We investigate satisfiability in the monadic fragment of first-order Gädel logics. These are a family of finite- and infinite-valued logics where the sets of truth values

V

are closed subsets of [0, 1] containing 0 and 1. We identify conditions on the topological type of

V

that determine the decidability or undecidability of their satisfiability problem.

Matthias Baaz, Agata Ciabattoni, Norbert Preining

### Learning by Questions and Answers: From Belief-Revision Cycles to Doxastic Fixed Points

We investigate the

long-term behavior of iterated belief revision with higher-level doxastic information

. While the classical literature on iterated belief revision [13, 11] deals only with

propositional

information, we are interested in

learning

(by an

introspective

agent, of some

partial

Q

1

,

Q

2

, ...,

Q

n

, ... that

may refer to the agent’s own beliefs

(or even to her

belief-revision plans

). Here, “learning” can be taken either in the “hard” sense (of becoming absolutely certain of the answer) or in the “soft” sense (accepting some answers as more plausible than others). If the questions are

binary

(“is

φ

true or not?”), the agent “learns” a sequence of

true

doxastic sentences

φ

1

, ...,

φ

n

, .... “Investigating the long-term behavior” of this process means that we are interested in whether or not the agent’s beliefs, her “knowledge” and her conditional beliefs stabilize eventually or keep changing forever.

Alexandru Baltag, Sonja Smets

### First-Order Linear-Time Epistemic Logic with Group Knowledge: An Axiomatisation of the Monodic Fragment

We investigate quantified interpreted systems, a computationally grounded semantics for a first-order temporal epistemic logic on linear time. We report a completeness result for the monodic fragment of a language that includes LTL modalities as well as distributed and common knowledge. We exemplify possible uses of the formalism by analysing message passing systems, a typical framework for distributed systems, in a first-order setting.

Francesco Belardinelli, Alessio Lomuscio

### On-the-Fly Macros

We present a domain-independent algorithm for planning that computes macros in a novel way. Our algorithm computes macros “on-the-fly” for a given set of states and does not require previously learned or inferred information, nor prior domain knowledge. The algorithm is used to define new domain-independent tractable classes of classical planning that are proved to include

Blocksworld-arm

and

Towers of Hanoi

.

Hubie Chen, Omer Giménez

### Abductive Logic Grammars

By extending logic grammars with constraint logic, we give them the ability to create knowledge bases that represent the meaning of an input string. Semantic information is thus defined through extra-grammatical means, and a sentence’s meaning logically follows as a by-product of string rewriting. We formalize these ideas, and exemplify them both within and outside first-order logic, and for both fixed and dynamic knowledge bases. Within the latter variety, we consider the usual left-to-right derivations that are traditional in logic grammars, but also – in a significant departure from the norm – arbitrary (i.e., order-independent) derivations. We show that rich and accurate knowledge extraction from text can be achieved through the use of this new formalism.

Henning Christiansen, Verónica Dahl

### On the Syntax-Semantics Interface: From Convergent Grammar to Abstract Categorial Grammar

Cooper’s storage technique for scoping

in situ

operators has been employed in theoretical and computational grammars of natural language (NL) for over thirty years, but has been widely viewed as ad hoc and unprincipled. Recent work by Pollard within the framework of convergent grammar (CVG) took a step in the direction of clarifying the logical status of Cooper storage by encoding its rules within an explicit but nonstandard natural deduction (ND) format. Here we provide further clarification by showing how to encode a CVG with storage within a logical grammar framework—abstract categorial grammar (ACG)—that utilizes no logical resources beyond those of standard linear deduction.

Philippe de Groote, Sylvain Pogodalla, Carl Pollard

### Observational Effort and Formally Open Mappings

Starting off with Moss and Parikh’s investigation into knowledge and topology, we propose a logical system which is capable of formally handling endomorphisms of subset spaces. The motivation for doing so originates from dynamic agent logics. Usually, these logics comprise certain epistemic actions. Our aim is to show that an appropriate extension of the Moss-Parikh system can serve similar purposes. In fact, since the semantics of an action can be described as a function inducing a change of the knowledge states of the involved agents, such transformations are to be modeled accordingly. Due to the ambivalence of the framework used here, this has some quasi-topological impact, too, in so far as a certain notion of open mapping can be captured now. The main issues of this paper concern the basic logical properties of the arising system, in particular, completeness. Our main technical resource for that is hybrid logic.

Bernhard Heinemann

### Forcing-Based Cut-Elimination for Gentzen-Style Intuitionistic Sequent Calculus

We give a simple intuitionistic completeness proof of Kripke semantics with constant domain for intuitionistic logic with implication and universal quantification. We use a cut-free intuitionistic sequent calculus as formal system and by combining soundness with completeness, we obtain an executable cut-elimination procedure. The proof, which has been formalised in the Coq proof assistant, easily extends to the case of the absurdity connective using Kripke models with exploding nodes.

Hugo Herbelin, Gyesik Lee

### Property Driven Three-Valued Model Checking on Hybrid Automata

In this paper, we present a three-valued

property driven

model checking algorithm for the logic

CTL

on hybrid automata. The technique of multi-valued model checking for hybrid automata aims at combining the advantages of classical methods based either on the preorder of simulation or on bounded reachability. However, as originally defined, it relies on the preliminary definition of special abstractions for combined over- and under-approximated reachability analysis, whose size is crucial and can be infinite. Our procedure avoids the above problem, since it is based on an incremental construction of the abstraction for the original hybrid automaton, that is suitably driven by the property under consideration.

Kerstin Bauer, Raffaella Gentilini, Klaus Schneider

### Team Logic and Second-Order Logic

Team logic is a new logic, introduced by Väänänen [1], extending dependence logic by classical negation. Dependence logic adds to first-order logic atomic formulas expressing functional dependence of variables on each other. It is known that on the level of sentences dependence logic and team logic are equivalent with existential second-order logic and full second-order logic, respectively. In this article we show that, in a sense that we make explicit, team logic and second-order logic are also equivalent with respect to open formulas. A similar earlier result relating open formulas of dependence logic to the negative fragment of existential second-order logic was proved in [2].

Juha Kontinen, Ville Nurmi

### Ludics and Its Applications to Natural Language Semantics

Proofs in Ludics, have an interpretation provided by their

counter-proofs

, that is the objects they interact with. We shall follow the same idea by proposing that sentence meanings are given by the

counter-meanings

they are opposed to in a dialectical interaction. In this aim, we shall develop many concepts of Ludics like

designs

(which generalize proofs),

cut-nets

,

orthogonality

and

behaviours

(that is sets of designs which are equal to their bi-orthogonal). Behaviours give statements their interactive meaning. Such a conception may be viewed at the intersection between

proof-theoretic

and

game-theoretical

accounts of semantics, but it enlarges them by allowing to deal with possibly infinite processes instead of getting stuck to an atomic level when decomposing a formula.

Alain Lecomte, Myriam Quatrini

### Spoilt for Choice: Full First-Order Hierarchical Decompositions

Database design aims to find a database schema that permits the efficient processing of common types of queries and updates on future database instances. Full first-order decompositions constitute a large class of database constraints that can provide assistance to the database designer in identifying a suitable database schema.

We establish a finite axiomatisation of full first-order decompositions that reflects best database design practice: an inference engine derives all potential candidates of a database schema, but the final choice remains with the database designer.

### Classic-Like Analytic Tableaux for Finite-Valued Logics

The paper provides a recipe for adequately representing a very inclusive class of finite-valued logics by way of tableaux. The only requisite for applying the method is that the object logic received as input should be sufficiently expressive, in having the appropriate linguistic resources that allow for a bivalent representation. For each logic, the tableau system obtained as output has some attractive features: exactly two signs are used as labels in the rules, as in the case of classical logic, providing thus a uniform framework in which different logics can be represented and compared; the application of the rules is analytic, in that it always reduces complexity, providing thus an immediate proof-theoretical decision procedure together with a counter-model builder for the given logic.

Carlos Caleiro, João Marcos

### A Duality for Algebras of Lattice-Valued Modal Logic

In this paper, we consider some versions of Fitting’s

L

-valued logic and

L

-valued modal logic for a finite distributive lattice

L

. Using the theory of natural dualities, we first obtain a natural duality for algebras of

L

-valued logic (i.e.,

L

-VL

-algebras), which extends Stone duality for Boolean algebras to the

L

-valued case. Then, based on this duality, we develop a Jónsson-Tarski-style duality for algebras of

L

-valued modal logic (i.e.,

L

-ML

-algebras), which extends Jónsson-Tarski duality for modal algebras to the

L

-valued case. By applying these dualities, we obtain compactness theorems for

L

-valued logic and for

L

-valued modal logic, and the classification of equivalence classes of categories of

L

-VL

-algebras for finite distributive lattices

L

.

Yoshihiro Maruyama

### An Independence Relation for Sets of Secrets

A relation between two secrets, known in the literature as

nondeducibility

, was originally introduced by Sutherland. We extend it to a relation between sets of secrets that we call

independence

. This paper proposes a formal logical system for the independence relation, proves the completeness of the system with respect to a semantics of secrets, and shows that all axioms of the system are logically independent.

Sara Miner More, Pavel Naumov

### Expressing Extension-Based Semantics Based on Stratified Minimal Models

Extension-based argumentation semantics is a successful approach for performing non-monotonic reasoning based on argumentation theory. An interesting property of some extension-based argumentation semantics is that these semantics can be characterized in terms of logic programming semantics. In this paper, we present novel results in this topic. In particular, we show that one can induce an argumentation semantics (that we call Stratified Argumentation Semantics) based on a logic programming semantics that is based on stratified minimal models. We show that the stratified argumentation semantics overcome some problems of extension-based argumentation semantics based on admissible sets and we show that it coincides with the argumentation semantics CF2.

Juan Carlos Nieves, Mauricio Osorio, Claudia Zepeda

### Deep Inference in Bi-intuitionistic Logic

Bi-intuitionistic logic is the extension of intuitionistic logic with exclusion, a connective dual to implication. Cut-elimination in bi-intuitionistic logic is complicated due to the interaction between these two connectives, and various extended sequent calculi, including a display calculus, have been proposed to address this problem.

In this paper, we present a new extended sequent calculus DBiInt for bi-intuitionistic logic which uses nested sequents and “deep inference”, i.e., inference rules can be applied at any level in the nested sequent. We show that DBiInt can simulate our previous “shallow” sequent calculus LBiInt. In particular, we show that deep inference can simulate the residuation rules in the display-like shallow calculus LBiInt. We also consider proof search and give a simple restriction of DBiInt which allows terminating proof search. Thus our work is another step towards addressing the broader problem of proof search in display logic.

Linda Postniece

### $\mathcal{CL}$ : An Action-Based Logic for Reasoning about Contracts

This paper presents a new version of the

$\mathcal{CL}$

contract specification language.

$\mathcal{CL}$

combines deontic logic with propositional dynamic logic but it applies the modalities exclusively over structured actions.

$\mathcal{CL}$

features synchronous actions, conflict relation, and an action negation operation. The

$\mathcal{CL}$

version that we present here is more expressive and has a cleaner semantics than its predecessor. We give a direct semantics for

$\mathcal{CL}$

in terms of

normative structures

. We show that

$\mathcal{CL}$

respects several desired properties from legal contracts and is decidable. We relate this semantics with a trace semantics of

$\mathcal{CL}$

which we used for run-time monitoring contracts.

Cristian Prisacariu, Gerardo Schneider

### Ehrenfeucht-Fraïssé Games on Random Structures

Certain results in circuit complexity (e.g., the theorem that AC

0

functions have low average sensitivity) [5, 17] imply the existence of winning strategies in Ehrenfeucht-Fraïssé games on pairs of random structures (e.g., ordered random graphs

G

=

G

(

n

,1/2) and

G

+

=

G

∪ {

random

edge

}). Standard probabilistic methods in circuit complexity (e.g., the Switching Lemma [11] or Razborov-Smolensky Method [19, 21]), however, give no information about how a winning strategy might look. In this paper, we attempt to identify specific winning strategies in these games (as explicitly as possible). For random structures

G

and

G

+

, we prove that the

composition of minimal strategies

in

r

-round Ehrenfeucht-Fraïssé games

$\Game_r(G,G)$

and

$\Game_r(G^{{+}},G^{{+}})$

is almost surely a winning strategy in the game

$\Game_r(G,G^{{+}})$

. We also examine a result of [20] that ordered random graphs

H

=

G

(

n

,

p

) and

H

+

=

H

∪ {random

k

-clique} with

p

(

n

) ≪

n

− 2/(

k

− 1)

(below the

k

-clique threshold) are almost surely indistinguishable by

$\lfloor k/4 \rfloor$

-variable first-order sentences of any fixed quantifier-rank

r

. We describe a winning strategy in the corresponding

r

-round

$\lfloor k/4 \rfloor$

-pebble game using a technique that combines strategies from several auxiliary games.

Benjamin Rossman

### Sound and Complete Tree-Sequent Calculus for Inquisitive Logic

We introduce a tree-sequent calculus for inquisitive logic (Groenendijk 2008) as a special form of labelled deductive system (Gabbay 1996). In particular, we establish that (i) our tree-sequent calculus is sound and complete with respect to Groenendijk’s inquisitive semantics and that (ii) our tree-sequent calculus is decidable and enjoys cut-elimination theorem. (ii) is semantically revealed by our argument for (i). The key idea which allows us to obtain these results is as follows: In Groenendijk’s inquisitive semantics, a formula of propositional logic is evaluated against a pair of worlds on a model. Given the appropriate pre-order on the set of such pairs, any inquisitive model can be regarded as a Kripke model for intuitionistic logic. This representation enables us to connect inquisitive semantics with the tree-sequent technique for non-classical logics (Kashima 1999).

Katsuhiko Sano

### The Arrow Calculus as a Quantum Programming Language

We express quantum computations (with measurements) using the arrow calculus extended with monadic constructions. This framework expresses quantum programming using well-understood and familiar classical patterns for programming in the presence of computational effects. In addition, the five laws of the arrow calculus provide a convenient framework for

equational reasoning

about quantum computations that include measurements.

Juliana Kaizer Vizzotto, André Rauber Du Bois, Amr Sabry

### Knowledge, Time, and Logical Omniscience

Knowledge’s acquisition happens

in

time. However, this feature is not reflected in the standard epistemic logics, e.g.

S4

with its possible world semantics suggested by Hintikka in [1], and hence their applications are limited. In this paper we adapt these normal modal logics to increase their expressive power such that not only is

what

is known modeled but also

when

it is known is recorded. We supplement each world with an awareness function which is an augmentation of Fagin-Halpern’s to keep track of the time when each formula is to be derived. This provides a new response to the logical omniscience problem. Our work originates from the tradition of study of

Justification Logic

, also known as

Logic of Proofs

,

LP

, introduced by Artemov ([2],[3],[4]). We will give the axiom systems of the models built here, accompanied with soundness and completeness results.

Ren-June Wang