Proof theory for hybrid(ised) logics

Hybridisation is a systematic process along which the characteristic features of hybrid logic, both at the syntactic and the semantic levels, are developed on top of an arbitrary logic framed as an institution. In a series of papers this process has been detailed and taken as a basis for a speci cation methodology for recon gurable systems. The present paper extends this work by showing how a proof calculus (in both a Hilbert and a tableau based format) for the hybridised version of a logic can be systematically generated from a proof calculus for the latter. Such developments provide the basis for a complete proof theory for hybrid(ised) logics, and thus pave the way to the development of (dedicated) proof support.

Reuse and integration of specification logics: the hybridisation perspective

Hybridisation is a systematic process along which the characteristic features of hybrid logic, both at the syntactic and the semantic levels, are developed on top of an arbitrary logic framed as an institution. It also captures the construction of first-order encodings of such hybridised institutions into theories in first-order logic. The method was originally developed to build suitable logics for the specification of reconfigurable software systems on top of whatever logic is used to describe local requirements of each system’s configuration. Hybridisation has, however, a broader scope, providing a fresh example of yet another development in combining and reusing logics driven by a problem from Computer Science. This paper offers an overview of this method, proposes some new extensions, namely the introduction of full quantification leading to the specification of dynamic modalities, and exemplifies its potential through a didactical application. It is discussed how hybridisation can be successfully used in a formal specification course in which students progress from equational to hybrid specifications in a uniform setting, integrating paradigms, combining data and behaviour, and dealing appropriately with systems evolution and reconfiguration.

A negação nos provérbios: uma abordagem na aula de português

Com a presente dissertação pretendemos demonstrar que a abordagem da negação, enquanto processo linguístico, deverá contemplar a amplitude das suas realizações sintáticas, morfológicas, lexicais e enunciativas. Pela sua preponderância na interação discursiva, consideramos fundamental sistematizar os mecanismos através dos quais este sistema se realiza na norma do português europeu e demonstrar a sua ocorrência num corpus amplo, autêntico e facilmente reconhecido pela maioria dos falantes do português. Entendendo os provérbios portugueses como documentos de elevado interesse cultural e linguístico, examinamos os diversos processos que, num conjunto selecionado de textos, permitem marcar os valores negativos. Neste estudo, é possível observar que as construções que compõem os textos proverbiais portugueses possuem um enorme potencial enunciativo que se manifesta, sobretudo, ao nível da interpretação, da inferência e da argumentação. Seguidamente, com o intuito de ajudar a promover as competências comunicativas dos alunos, perspetivamos uma abordagem destas temáticas ao longo da escolaridade obrigatória, assente nas orientações que emanam do Programa e das Metas Curriculares de Português, atualmente, em vigor. Os exercícios propostos e aplicados são meramente ilustrativos, todavia as conclusões decorrentes podem ser um indicador válido para futuras atuações.