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.
14.00 Opening: Maribel Fernández and Marcelo Finger
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
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
11.30-12.00 Walter Carnielli and Mariana Matulovic. Non-deterministic Semantics in Polynomial Format
Session 5 – Chair: Maurício Ayala-Rincón
(Really) Dynamic Modal Logics
Different 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.
15.15-15.30 Marcelo Finger. Recent developments in Probabilistic Satisfiability
Session 6 – Chair: Marcelo Finger
16.00-17.00 Invited Talk: Marcello D’Agostino – University of Ferrara, Italy
Depth-Bounded Boolean Logics
We 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.