Workshop on Logic, Language and Information

Venue

 October 13th, 2015

 Universidade Federal Fluminense
 Insituto de Computação
 Av. Gal. Milton Tavares de Souza, s/n
 Gragoatá
 Niterói - RJ

Program

Speakers

Carlos Olarte (ECT/UFRN)

From subexponentials in linear logic to concurrent programming and back (slides)

Abstract. Reasoning about concurrent programs is much harder than reasoning about sequential ones. Programmers often find themselves overwhelmed by the many subtle cases of thread interactions they must be aware of to decide whether a concurrent program is correct or not. In this talk I will introduce Saraswat's Concurrent Constraint Programming (CCP), a declarative model of concurrency where agents can be seen, coherently, as (concurrent) processes and formulas in logic. The core CCP language can be extended to deal with different modalities (e.g., temporal, spatial and epistemic modalities) as well as with preferences (e.g., probabilities, fuzzy information, etc.). By giving a logical characterization of such modalities, we show that CCP's extensions are not ad-hoc. More precisely, we can exhibit a tight adequacy result between operational steps in the (extended) CCP language and derivations in linear logic with subexponentials (SELL). Moreover, by studying the proof theory of SELL, we show how to define new declarative constructors for CCP. Hence, SELL is not only a framework for verifying CCP programs but it is also useful to enrich the language of processes to cope with more interesting behaviors in concurrent systems.

Cláudia Nalon (CiC/UnB)

Polluted Resolution and other Combined Proof Search Methods for Propositional Modal Logics (slides)

Abstract. Several resolution-based methods have been designed to deal with the satisfiability problem in modal logics. As its classical counterpart, those methods often follow a pure syntactical approach and rely on heavy preprocessing of the formulae being tested for satisfiability. In this talk, we give an overview on how such calculi can be enriched with semantic annotation and discuss some aspects related to the effectiveness and efficiency of the resulting calculi.

Edward Hermann Haeusler (DI/PUC-Rio)

On the computational complexity of propositional systems

Abstract. We discuss some aspects related to the computational complexity of propositional logics and the feasiability of automated theorem proving.

Elaine Pimentel (DMAT/UFRN)

Proof search in modal logics (slides)

Abstract. We propose a notion of focusing for nested sequent calculi for modal logics which brings down the complexity of proof search to that of the corresponding sequent calculi. The resulting systems are amenable to specifications in linear logic. Examples include modal logic K, a simply dependent bimodal logic and the standard non-normal modal logics. As byproduct we obtain the first nested sequent calculi for the considered non-normal modal logics.

Hugo Macedo (DI/PUC-Rio)

Defining Effectiveness Using Finite Sets - A Study on Computability

Abstract. We study effectiveness in the domain of computability. In the context of model-theoretical approaches to effectiveness, where a function is considered effective if there is a model containing a representation of such function, our definition relies in a model provided by functions between finite sets and uses category theory as its mathematical foundations. In our model we use the fact that every function between finite sets is computable, and that finite composition of such functions is also computable. Our approach is an alternative to the traditional model-theoretical based works which rely on (ZFC) set theory as a mathematical foundation, and our approach is also novel when compared to the works using category theory to approach computability results.

Jean-Baptiste Joinet (FP/Université de Lyon 3)

TBA

Abstract. TBA

Lew Gordeev (CSD/Universitat Tübingen)

On sequent calculi vs natural deductions in logic and computer science (slides)

Abstract. This is a short comparison of some important consequences of sequent calculus and natural deduction formalisms to logic and computer science.

Mario Benevides (COPPE/UFRJ)

Epistemic Logics for Authentication and Secrecy in Protocols (slides)

Abstract. It is proposed a new Epistemic logic aimed to reasoning about authentication and secrecy in communication protocols. The logic is based on Dolev Yao model for analyzing security of public key protocols. It is presented an axiomatization and proofs of soundness and completeness. In oder to illustrate the applicability of this new logic it is verified some examples and some well known protocols (Keberos and RPC). Finally, the logic is extended with common knowledge operator and again a sound and complete axiomatization is provided.

Petrucio Viana (IME/UFF)

Methods of proof for residuated algebras of binary relations (slides)

Abstract. We define the quasi-equational and Horn-quasi-equational theories of residuated algebras of binary relations. We review some negative results showing that these theories are not finitely axiomatizable (on the top of equational logic). We present two alternatives for proving the valid quasi-equations and Horn-quasi-equations: Calculational Reasoning and Diagrammatic Reasoning. We close by discussing some open problems relating these environments. This is a joint work with Marcia Cerioli (IM/COPPE/UFRJ).

Vaston Gonçalves (DCC/UFG)

TBA

Abstract. TBA

Committees

Program Committee

• Bruno Lopes (IC/UFF)
• Edward Hermann Haeusler (DI/PUC-Rio)
• Luiz Carlos Pereira (DeFil/PUC-Rio)

Organization

Bruno Lopes (IC/UFF)

Realization

Support