previous day
all days

View: session overviewtalk overviewside by side with other conferences

08:45-10:15 Session 159E
Location: FH, Hörsaal 4
From display logic to nested sequents via residuated frames
SPEAKER: Nick Galatos
First-order non-classical logics: an order-based approach
SPEAKER: Petr Cintula

ABSTRACT. It is well-known, already in classical logic, that propositional logics have a limited expressive power which can fail to provide satisfactory means for modelling and analysis in certain contexts. For this reason it is highly desirable to introduce, for every logic, a predicate extension allowing to distinguish between properties and objects. There have been systematic studies of predicate versions for some families of non-classical logics, such as super-intuitionistic, modal, or fuzzy logics. In other cases there are numerous competing partial approaches.

In this talk I will present a unified approach allowing to build a predicate version for (almost) any non-classical logic as long as its algebraic semantics features some natural ordering. Following the pioneering works of Mostowski, Rasiowa, and Sikorski, one interprets quantifiers using infima/suprema with respect to this ordering. I will provide a complete axiomatization of this intended semantics (generalizing Henkin's proof for classical logic), formulate Skolem and Herbrand theorems in a restricted setting, survey known results from model theory of these logics, and present further possible research directions in this fascinating area.

10:15-10:45Coffee Break
10:45-13:00 Session 166K
Location: FH, Hörsaal 4
Broadly truth-functional logics through classical lenses
SPEAKER: João Marcos

ABSTRACT. With different motivations and goals, Roman Suszko, Dana Scott and Newton da Costa have all suggested in the 70s that Tarskian logics, however many-valued they might initially appear to be, could always be characterized with the use of only two _logical values_. A programmatic effort to show how such a presentation could be attained for increasingly larger classes of logics, while at the same time avoiding serious losses of nice computational properties, was carefully undertaken in the last decade. In this talk I will show how bivalent effective semantics and uniform classic-like analytic tableaux may be obtained for logics characterized by way of finite-valued nondeterministic semantics.

The latest developments concern ongoing work with Carlos Caleiro and Carlos Silva.

Natural deduction for non-deterministic finite-valued logics
The procedural understanding of meaning and compositionality in formal semantics

ABSTRACT. BCI-algebras are related to formal systems of Fuzzy Logic. They model the so
called BCI-logics which are based on Curry combinators (B) xyz.x(yz), (C)
xyz.xzy and (I) x.x. They are algebras of the form <A,⊖,⊥> which satisfy
the following properties:

BCI-1 ((x ⊖ y) ⊖ (x ⊖ z)) ⊖ (z ⊖ y) =⊥
BCI-2 (x ⊖ (x ⊖ y)) ⊖ y =⊥
BCI-3 x ⊖ x =⊥
BCI-4 x ⊖ y =⊥ and y ⊖ x =⊥ =⇒ x = y.

A BCI-algebra is called BCK-algebra, whenever it also satisfies:

BCK-1 ⊥ ⊖ x =⊥

On any BCI-algebra it is possible to define a partial order “≤” as:

“x ≤ y iff x ⊖ y =⊥”.

In this talk we will propose a generalization for such algebras, in order to capture some phenomena of Lukasiewcz Interval implications.

13:00-14:30Lunch Break
14:30-16:00 Session 172K
Location: FH, Hörsaal 4
An intuitionistic ALC description default logic

ABSTRACT. Knowledge formalization and reasoning automation are central within

Artificial Intelligence.  Classical logic has been traditionally used

for such purposes. However, it is better suited to deal with complete

knowledge in ideal circumstances. In real situations, in which the

knowledge is partial, classical logic is not sufficient since it is

monotonic. Nonmonotonic logics have been proposed to better cope with

practical reasoning. A successful formalization of nonmonotonic

reasoning is the Reiter's default logic which extends classical logic

with default rules. Unfortunately, default logic is undecidable. One

reason for that is the use of classical logic as its monotonic basis.


In this work, we change the default logic monotonic basis and propose

a new default logics based on its intuitionistic version iALC. This

new default logics are decidable and useful to formalize practical

reasoning on hierarchical ontologies with exceptions, specially the

ones that deals with legal knowledge and reasoning. On the default

counterpart, we add some restrictions to the application of defaults

in order to obtain nice properties such as coherence and elimination

of anomalous extensions. We present the main algorithms used to build

the extension for this logic, including the sequent calculus for

iALC, with its complexity analysis.


An infinitary deduction system for CTL*
SPEAKER: Luca Viganò
Modal functions as moody truth-functions
SPEAKER: Pedro Falcão
We can think of the usual (S5) modalities as 'moody' truth-functions. E.g. the necessity operator 'works' as falsum (constant falsehood) if the argument is contingent, and it works as the identity function if the argument is rigid (i.e. non-contingent); the possibility operator 'works' as verum (constant truth) if the argument is contingent and works as the identity if the argument is rigid.
We show how (the 16) pairs of unary truth-functions correspond unequivocally to unary modal functions; moreover we show how to generalize this to establish a correspondence between modal functions of arbitrary degree and sequences of truth-functions.
16:00-16:30Coffee Break
16:30-18:00 Session 175L
Location: FH, Hörsaal 4
On subexponentials, focusing and modalities in concurrent systems

ABSTRACT. Concurrent Constraint Programming (CCP) is a simple and powerful model for concurrency where agents interact by telling and asking constraints. Since their inception, CCP-languages have been designed for having a strong connection to logic. In fact, the underlying constraint system can be built from a suitable fragment of intuitionistic (linear) logic --ILL-- and processes can be interpreted as formulas in ILL. Constraints as ILL formulas fail to represent accurately situations where ``preferences'' (called soft constraints) such as probabilities, uncertainty or fuzziness are present. In order to circumvent this problem, c-semirings have been proposed as algebraic structures for defining constraint systems where agents are allowed to tell and ask soft constraints. Nevertheless, in this case, the tight connection to logic and proof theory is lost. In this work, we give a proof theoretical meaning to soft constraints: they can be defined as formulas in a suitable fragment of ILL with subexponentials (SELL) where subexponentials, ordered in a c-semiring structure, are interpreted as preferences. We hence achieve two goals: (1) obtain a CCP language where agents can tell and ask soft constraints and (2) prove that the language in (1) has a strong connection with logic. Hence we keep a declarative reading of processes as formulas while providing a logical framework for soft-CCP based systems. An interesting side effect of (1) is that one is also able to handle probabilities (and other modalities) in SELL, by restricting the use of the promotion rule for non-idempotent c-semirings. This finer way of controlling subexponentials allows for considering more interesting spaces and restrictions, and it opens the possibility of specifying more challenging computational systems.


Quantum state transformations and distributed temporal logic
SPEAKER: Luca Viganò
Combining non-determinism and context awareness in consistency restoration systems
SPEAKER: Anna Zamansky