Behavioral equivalence of hidden k-logics: an abstract algebraic approach

This work advances a research agenda which has as its main aim the application of Abstract Algebraic Logic (AAL) methods and tools to the specification and verification of software systems. It uses a generalization of the notion of an abstract deductive system to handle multi-sorted deductive systems which differentiate visible and hidden sorts. Two main results of the paper are obtained by generalizing properties of the Leibniz congruence — the central notion in AAL. In this paper we discuss a question we posed in [1] about the relationship between the behavioral equivalences of equivalent hidden logics. We also present a necessary and sufficient intrinsic condition for two hidden logics to be equivalent.

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 componente de apoio à família na educação pré-escolar: contextos locais e lógicas de ação

A Componente de Apoio à Família surge como resposta à necessidade daquelas famílias cujo horário de trabalho não é compatível com o tempo letivo diário disponibilizado pelos jardins-de-infância públicos aos seus filhos. O Jardim-de-infância situa-se num contexto organizacional diversificado, uma vez que estabelece relações com o agrupamento de escolas a que pertence, com a autarquia, com os pais, com as associações de pais, com as instituições particulares de solidariedade social, com a comunidade e com outros parceiros educativos. Este estudo visa analisar a participação de diferentes prestadores de serviços: autarquias, associações de pais e instituições particulares de solidariedade social na organização, funcionamento e gestão da Componente de Apoio à Família. Neste contexto, pretendemos identificar os princípios e as estratégias que sustentam os diferentes prestadores de serviços e o modo como lidam com as questões da Componente de Apoio à Família, isto é, as lógicas de ação inerentes a cada prestador de serviços. Partindo de uma matriz metodológica qualitativa, recorremos ao estudo de caso, desenvolvendo o trabalho empírico em três concelhos da zona centro denominados Concelhos do Mar, da Ria e da Praia. Privilegia-se a realização de entrevistas, nomeadamente a educadores de infância, representantes dos agrupamentos de escolas, presidentes de associações de pais, diretoras/coordenadoras das instituições particulares de solidariedade social, animadores da componente de apoio à família e representantes das autarquias, num total de 56 entrevistas. Como principais resultados, verificamos que nos concelhos em estudo a resposta da Componente de Apoio à Família prestada por diferentes organizações apresentam lógicas de ação distintas: no Concelho do Mar a predominância vai para as lógicas de ação de poder local e de associativismo; no Concelho da Ria predominam lógicas de ação de natureza empresarial/mercado e de poder local; no Concelho da Praia salientamos as lógicas de ação burocrática e de poder local.

A tableau system for Quasi-hybrid logic

Hybrid logic is a valuable tool for specifying relational structures, at the same time that allows defining accessibility relations between states, it provides a way to nominate and make mention to what happens at each specific state. However, due to the many sources nowadays available, we may need to deal with contradictory information. This is the reason why we came with the idea of Quasi-hybrid logic, which is a paraconsistent version of hybrid logic capable of dealing with inconsistencies in the information, written as hybrid formulas. In [5] we have already developed a semantics for this paraconsistent logic. In this paper we go a step forward, namely we study its proof-theoretical aspects. We present a complete tableau system for Quasi-hybrid logic, by combining both tableaux for Quasi-classical and Hybrid logics.