Programme

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
15.00-15.30 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
11.00-11.30 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
12.00-12.15 Daniele Nantes Sobrinho. I-locally stable theories and Finite Abelian Groups (joint work with M. Ayala-Rincon and M. Fernandez)
12.15-12.30 Edward Hermann Haeussler. TBA

12.30-14.00 Lunch

 

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

14.00-15.00 Invited Talk: Carlos Areces – National University of Córdoba (UNC), Argentina

(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.00-15.15 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

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.

17.00 Closing

0 comments on “Programme
1 Pings/Trackbacks for "Programme"