# Monday, 2 September 2013

**9.00-10.30 Tutorial 1**

First Steps in Hybrid Logics – Carlos Areces (charla-lsfa13)

This tutorial introduce hybrid logics, a family of modal logics in which it is possible to name states (or times, or worlds, or situations, or nodes in parse trees, or people – indeed, whatever it is that the elements of the model are taken to represent).The tutorial has two major goals. The first is to provide an introduction to modal logics and then convey, as clearly as possible, the ideas and intuitions that have guided the development of hybrid logics. The second is to introduce a concrete skill: tableau-based hybrid deduction.

**10.30-11.00 Coffee Break**

**11.00-12.30 Tutorial 2
**

A Tour of Analytic Tableaux and Related Methods – Marcello D’Agostino(presentation)

We provide an introduction to the method of analytic tableaux and discuss its relations with Gentzen’s sequent calculus and Natural Deduction. We then focus on the anomalies and limitations of the original method and discuss some more efficient variants such as the KE method and the Davis-Putnam procedure.

**12.30-14.00 Lunch**

**14.00 Opening: Maribel Fernández and Marcelo Finger **

**Session 1 – Chair: Edward Hermann Haeussler**

14.00-14.30

**Paulo Veloso, Sheila Veloso and Mario Benevides.**On a Graph Approach to Modal Logics

14.30-15.00

**Charles Morgan, Valeria De Paiva and Samuel Gomes Da Silva.**Natural Number Objects in Dialectica Categorie

**Cláudia Nalon and Oliver Kutz.**Towards resolution-based reasoning for connected logics

**15.30-16.00 Coffee Break**

**Session 2 – Chair: Alvaro Tasistro **

16.00-16.30 ** Mario Benevides.** Bisimilar and Logically Equivalent Programs in PDL

16.30-17.00 ** Bruno Lopes, Mario Benevides and Edward Hermann Haeusler. ** Extending Propositional Dynamic Logic for Petri Nets

17.00-17.30 ** Carlos Olarte, Vivek Nigam and Elaine Pimentel. ** Mobile links in Concurrent Constraint Programming

17.30-17.45 ** Daniel Ventura. ** Termination properties by non-idempotent intersection types

# Tuesday, 3 September 2013

** Session 3 – Chair: Maribel Fernández **

9.30-10.30 **Invited talk:** ** José Meseguer – University of Illinois at Urbana-Champaign**

Rewriting Logic as a Logical and Semantic Framework (sao-paulo-slides)

Rewriting logic is a simple meta-logic in which many different logics and a very wide range of models of concurrent computation and of programming and modeling languages can be naturally represented. The meaning of “naturally,” is that there are no artificial encodings, so that the distance between what is represented and its representation in the meta-logic is minimal or non-existent. The talk will summarize the extensive experience already gained in a wide range of logical and semantic framework applications, and some of the features making such applications easy to develop such as concurrency, high-performance executability, support for logical reflection and meta-logical reasoning, support for binding operators, and support for user-definable algebraic data types modulo structural axioms.

**10.30-11.00 Coffee Break**

**Session 4 – Chair: Elaine Pimentel**

**Paulo T. Guerra and Renata Wassermann.**On the Difference Between Revising Models and Revising Specifications

11.30-12.00

**Walter Carnielli and Mariana Matulovic.**Non-deterministic Semantics in Polynomial Format

**Daniele Nantes Sobrinho.**I-locally stable theories and Finite Abelian Groups (joint work with M. Ayala-Rincon and M. Fernandez)

**Edward Hermann Haeussler.**TBA

**12.30-14.00 Lunch**

**Session 5 – Chair: Maurício Ayala-Rincón**

**Invited Talk:**

**Carlos Areces – National University of Córdoba (UNC), Argentina**

(Really) Dynamic Modal LogicsDifferent Dynamic Modal Logics have been investigated in the literature (e.g., Propositional Dynamic Logics). Interestingly, the semantics of most of these logics is actually *static*, the model over which a formula is evaluated never changes. We are interested in logics with operators that can actually alter the model during evaluation. We will present a number of these operators, discuss its expressive power, and the complexity of it model checking and satisfiability problem.

**Alvaro Tasistro.**TBA

15.15-15.30

**Marcelo Finger.**Recent developments in Probabilistic Satisfiability

**15.30-16.00 Coffee Break**

Session 6 – Chair: Marcelo Finger

Session 6 – Chair: Marcelo Finger

16.00-17.00

**Invited Talk:**

**Marcello D’Agostino – University of Ferrara, Italy**

Depth-Bounded Boolean LogicsWe present a unifying semantic and proof-theoretical framework for investigating depth-bounded approximations to Boolean Logic in which the number of nested applications of a single structural rule, representing the classical Principle of Bivalence (classical cut), is bounded above by a fixed natural number. These approximations provide a hierarchy of tractable logical systems that indefinitely converge to classical propositional logic and can be usefully employed to model the inferential activity of real-life, resource-bounded agents.

**17.00 Closing**

[…] Programme […]