Procesos de enseñanza basados en la descripción semántica formal y explícita de documentación educativa.

La gestión de información constituye un proceso fundamental en el desarrollo de la sociedad, y la documentación educativa constituye un pilar fundamental en este contexto. El presente trabajo tiene como objetivo fundamental el fundamentar el impacto directo que tiene la gestión de la semántica sobre: 1) la organización de la documentación educativa, 2) las facilidades de recuperación de información al utilizar sistemas más inteligentes de búsquedas de información basados en la semántica, además del 3) soporte a las herramientas de integración entre diferentes servicios. En este artículo se muestran los resultados alcanzados en el ámbito de Educative, proyecto de gestión integral de documentación educativa en el ámbito universitario en pos de una enseñanza universitaria más integral en el contexto cubano.

Semântica formal para TVQL

Modelos de bancos de dados têm sido progressivamente estendidos a fim de melhor capturar necessidades específicas de aplicações. Bancos de dados versionados, por exemplo, provêm suporte a versões alternativas de objetos. Bancos de dados temporais, por sua vez, permitem armazenar todos os estados de uma aplicação, registrando sua evolução com o passar do tempo. Tais extensões sobre os modelos de dados se refletem nas respectivas linguagens de consulta, normalmente sob a forma de extensões a linguagens conhecidas, tais como SQL ou OQL. O modelo de banco de dados TVM (Temporal Versions Model ), definido sobre o modelo de banco de dados orientado a objetos, suporta simultaneamente versões alternativas e o registro de alterações de objetos ao longo do tempo. A linguagem de consulta TVQL (Temporal Versioned Query Language), definida a partir da linguagem de consulta SQL, permite recuperar informações do modelo de dados TVM. As construções introduzidas em TVQL têm como objetivo tornar simples a consulta do banco de dados em diversos pontos da linha temporal. Apesar das vantagens da utilização da linguagem TVQL para resgatar dados temporais do modelo TVM, existem algumas limitações importantes para seu aprimoramento. Uma delas é a alta complexidade do modelo TVM, proveniente da integração de conceitos variados como estados alternativos e rótulos temporais. Outro ponto é que, até o presente momento, não existe um interpretador para TVQL, impedindo uma experiência prática de programação de consultas. O objetivo principal deste trabalho é o desenvolvimento de uma especificação formal para a linguagem TVQL, tornando possível um estudo consistente de suas construções. Adicionalmente, uma especificação formal serve como documentação para futuras implementações de interpretadores. Neste trabalho foi desenvolvido um protótipo de avaliador de consultas e verificador de tipos para um núcleo funcional da linguagem TVQL, possibilitando também uma experimentação prática sobre os modelos propostos.

Mecanización de semántica de lenguajes de programación: teoría, implementación y desarrollo.

El presente proyecto se enmarca en el área de métodos formales para computación; el objetivo de los métodos formales es asegurar, a través de herramientas lógicas y matemáticas, que sistemas computacionales satisfacen ciertas propiedades. El campo de semántica de lenguajes de programación trata justamente de construir modelos matemáticos que den cuenta de las diferentes características de cada lenguaje (estado mutable, mecanismos de paso de parámetros, órdenes de ejecución, etc.); permitiendo razonar de una manera abstracta, en vez de lidiar con las peculiaridades de implementaciones o las vaguezas de descripciones informales. Como las pruebas formales de corrección son demasiado intrincadas, es muy conveniente realizar estos desarrollos teóricos con la ayuda de asistentes de prueba. Este proceso de formalizar y corrobar aspectos semánticos a través de un asistente se denomina mecanización de semántica. Este proyecto – articulado en tres líneas: semántica de teoría de tipos, implementación de un lenguaje con tipos dependientes y semántica de lenguajes imperativos con alto orden - se propone realizar avances en el estudio semántico de lenguajes de programación, mecanizar dichos resultados, e implementar un lenguaje con tipos dependientes con la intención de que se convierta, en un mediano plazo, en un asistente de pruebas. En la línea de semántica de teoría de tipos los objetivos son: (a) extender el método de normalización por evaluación para construcciones no contempladas aun en la literatura, (b) probar la adecuación de la implementación en Haskell de dicho método de normalización, y (c) construir nuevos modelos categóricos de teoría de tipos. El objetivo de la segunda línea es el diseño e implementación de un lenguaje con tipos dependientes con la intención de que el mismo se convierta en un asistente de pruebas. Una novedad de esta implementación es que el algoritmo de chequeo de tipos es correcto y completo respecto al sistema formal, gracias a resultados ya obtenidos; además la implementación en Haskell del algoritmo de normalización (fundamental para el type-checking) también tendrá su prueba de corrección. El foco de la tercera línea está en el estudio de lenguajes de programación que combinan aspectos imperativos (estado mutable) con características de lenguajes funcionales (procedimientos y funciones). Por un lado se avanzará en la mecanización de pruebas de corrección de compiladores para lenguajes Algollike. El segundo aspecto de esta línea será la definición de semánticas operacional y denotacional del lenguaje de programación Lua y la posterior caracterización del mismo a partir de ellas. Para lograr dichos objetivos hemos dividido las tareas en actividades con metas graduales y que constituyen en sí mismas aportes al estado del arte de cada una de las líneas. La importancia académica de este proyecto radica en los avances teóricos que se propone en la línea de semántica de teoría de tipos, en las contribución para la construcción de pruebas mecanizadas de corrección de compiladores, en el aporte que constituye la definición de una semántica formal para el lenguaje Lua, y en el desarrollo de un lenguaje con tipos dependientes cuyos algoritmos más importantes están respaldados por pruebas de corrección. Además, a nivel local, este proyecto permitirá incorporar cuatro integrantes al grupo de “Semántica de la programación”.

El viejo, el amor y la hermosa como texto espectacular

Resumen: Inspirada por el Diálogo entre Amor y un viejo, de Rodrigo Cota, Interlocutores senex et amor mulierque pulcra forma es una muy interesante obra concebida para su puesta en escena; sin embargo, no posee acotación autoral alguna, lo que implica que el texto espectacular debe extraerse de la construcción semántica-formal de los signos verbales discursivos en voz de los personajes, que son los que comportan los requisitos necesarios de dramaticidad. A partir de estos signos analizaré varios aspectos contenidos en la estructura, que determino tripartita, de inicio, nudo y desenlace; por ejemplo, la actio (gestus, motus y vultus corporales), la pronuntiatio, la representación de los espacios ficcionales, y elementos obligados de caracterización. Comentaré, también, el espacio para la puesta; habré de aducir condicionantes culturales tanto para la caracterización (corporal y de indumentaria), como para los tipos de gestualidad que deben realizarse en escena (mediante el apoyo de preceptivas retóricas y obras iconográficas). No dejaré del lado la descodificación semántica asociada con todos los elementos referidos.

On the iteration of Katsuno and Mendelzon update

In this dissertation we present a model for iteration of Katsuno and Mendelzon’s Update, inspired in the developments for iteration in AGM belief revision. We adapt Darwiche and Pearls’ postulates of iterated belief revision to update (as well as the independence postulate proposed in [BM06, JT07]) and show two families of such operators, based in natural [Bou96] and lexicographic revision [Nay94a, NPP03]. In all cases, we provide a possible worlds semantics of the models.

Investigação e aplicação de operações categoriais entre atores de animações baseadas em autômatos finitos com saída

O presente trabalho apresenta uma investigação sobre algumas operações categoriais baseadas em grafos e a aplicação das mesmas a uma área específica da Ciência da Computação, a saber, animações computacionais baseadas em autômatos finitos com saída. As operações categoriais estudadas neste trabalho são: Produto, Coproduto, Soma Amalgamada e Produto Fibrado. O modelo AGA (Animação Gráfica baseada em Autômatos finitos) foi o escolhido para ser utilizado como base desta dissertação. Inspirado nestes estudos, o trabalho contém uma proposta de como aplicar tais operações com o objetivo de definir animações aparentemente complexas, de forma simples, precisa e de fácil implementação. O enfoque está baseado em J. Stoy que diz que um dos objetivos para o uso da semântica formal de teoria das categorias é “sugerir meios ou formas para o projetista desenvolver sistemas melhores, mais elegantes (“limpos”) e com descrições formais mais simples”. Entretanto, não é objetivo deste trabalho verificar se a utilização destas operações é ou não melhor do que a utilização de qualquer outra solução para criar novas animações. Esta dissertação traz uma nova versão do modelo AGA, denominada AGANd (Animação Gráfica baseada em Autômatos finitos Não determinísticos), sendo que o AGA utiliza apenas autômatos finitos determinísticos para criar os atores de uma animação. Com a utilização do AGANd obtém-se animações mais realistas e mais flexíveis. A aplicação destas operações se dá nos dois modelos, os resultados obtidos a partir de cada uma das operações sobre os mesmos são apresentados de forma detalhada e ilustrados com os autômatos resultantes no decorrer do trabalho. É apresentada uma sugestão de implementação para cada uma das operações, visando estender o protótipo já implementado do modelo AGA. Isso faz com que o leitor seja estimulado a aplicar estas e outras operações categoriais em novas animações baseadas ou não nos modelos apresentados, despertando até mesmo para seu uso em outras áreas da Ciência da Computação.

Mapeamento da linguagem Nautilus para Java

Este trabalho apresenta um mapeamento centrado nas construções não usuais da linguagem Nautilus, para a linguagem convencional, no caso Java, mantendo propriedades com atomicidade que são requisitos da semântica formal da linguagem. Nautilus é originalmente uma linguagem de especificação baseada em objetos, textual que suporta objetos concorrentes e não deterministas. Desde então a linguagem foi modificada aom extensões como classes e uma notação diagramática, além de se investigar seu uso como linguagem de programação. Suas construções incomuns (reificação, agregação, etc.) são baseados em seu domínio semântico: Automâtos Não Sequenciais. Este domíno satisfaz composição diagonal, i.e refinamentos se compõem (verticalmente) refletindo uma descrição gradual de sistemas, envolvendo múltiplos níveis de abstração, e distribui-se através de combinadores (horizontalmente), o que significa que o refinamento de um sistema composto é a combinação de do refinamento de suas partes.O trabalho inclui um mapeamento inicial de um subconjunto da linguagem(objeto base, reificação, agregação e visão), uma versão ampliada para abranger mais construções( interação e classes), e uma versão refinada mais concorrente e sugestões de modificação na linguagem.

On the iteration of Katsuno and Mendelzon update

In this dissertation we present a model for iteration of Katsuno and Mendelzon’s Update, inspired in the developments for iteration in AGM belief revision. We adapt Darwiche and Pearls’ postulates of iterated belief revision to update (as well as the independence postulate proposed in [BM06, JT07]) and show two families of such operators, based in natural [Bou96] and lexicographic revision [Nay94a, NPP03]. In all cases, we provide a possible worlds semantics of the models.

O tempo e a linguagem

Pós-graduação em Linguística e Língua Portuguesa - FCLAR

A LITTLE HISTORY OF LINGUISTIC IN BRAZIL: INTERVIEW WITH JOSÉ BORGES NETO

We are pleased to present this edition of the journal Language & Letters, interview courtesy Professor José Borges Neto, researcher recognized for the excellent work that develops in Linguistics with an emphasis in Philosophy of Language. Professor holds a degree in Literature from the Pontifical Catholic University of Paraná (1972), MA in Linguistics from the State University of Campinas (1979) and PhD in Linguistics from the State University of Campinas (1991). Professor of the Federal University of Paraná between 1999 and 2010. Retired in 2010, continues to serve as Senior Lecturer in the Graduate Program in Linguistics UFPR and a senior professor at Unioeste in the period 2012-2016. Has experience in the area of ​​linguistics, with an emphasis on semantics, acting on the following topics: Epistemology of Linguistics, Linguistics Historiography, Formal Semantics and Categorial Grammars.

On the semantics of 'pouco' (little/few) and 'um pouco' (a little/few)

this paper discusses the interpretation of expressions ‘pouco’ (‘few’) and ‘um pouco’ (‘a few/little’) from a referential approach of meaning (CHIERCHIA, 2003; among others). First, we aim to describe their syntactic and semantic behavior. After that, we search for the appropriate semantics to be attributed to ‘pouco’, which operates both on the domain of individuals and on the degree domain. In spite of this, there is a general operation that this modifier does (GUIMARÃES, 2007). We propose a semantics for ‘pouco’ which incorporates two aspects already seen in the literature: the value judgment, and the intuition that it means something like ‘less than a contextual standard’. To ‘um pouco’ we advocate a compositional approach.

La Web Semántica y los archivos de televisión: estado de la cuestión

Se analizan y describen las principales líneas de trabajo de la Web Semántica en el ámbito de los archivos de televisión. Para ello, se analiza y contextualiza la web semántica desde una perspectiva general para posteriormente analizar las principales iniciativas que trabajan con lo audiovisual: Proyecto MuNCH, Proyecto S5T, Semantic Television y VideoActive.

El procés de gramaticalització en l'adquisició del llenguatge: la categoria formal de verb

Des de diverses perspectives, alguns autors han remarcat la importància del verb en l'adquisició del llenguatge (Bloom, 1991; Pinker, 1989; Tomasello, 1992). Donat que la seva estructura semàntica proporciona un marc conceptual per incloure-hi estructures lingüistiques més àmplies, esdevé un element clau en el pas a una fase de parla organitzada gramaticalment. Es per aquest motiu que l'adquisició de la categoria formal de verb és essencial per poder entendre com els nens arriben a ser gramaticalment competents. En aquest estudi pretenem explorar com s'adquireix la classe formal de verb tenint en compte les diferents propostes que intenten explicar el procés de gramaticalització i, en concret, l'adquisició de les categories de mot. En les dades sobre l'adquisició inicial dels verbs, es troba que a partir dels tres anys hi ha un ús consistent del elements verbals, però abans d'aquesta edat alguns autors han descrit un ús dels marcadors morfològics limitat a alguns verbs (Bloom, 90) i també que la utilització de l'estructura argumental inicial sembla anar lligada a verbs individuals (Tomasello, 92, Olguin i Tomasello, 93). Aquestes dades apunten que en un principi els verbs serien utilitzats de forma lexicalitzada, de manera que s'adquiririen individualment.

Uma Proposta de especificação formal e fundamentação teórica para simulated annealing

Os algoritmos baseados no paradigma Simulated Annealing e suas variações são atualmente usados de forma ampla na resolução de problemas de otimização de larga escala. Esta popularidade é resultado da estrutura extremamente simples e aparentemente universal dos algoritmos, da aplicabilidade geral e da habilidade de fornecer soluções bastante próximas da ótima. No início da década de 80, Kirkpatrick e outros apresentaram uma proposta de utilização dos conceitos de annealing (resfriamento lento e controlado de sólidos) em otimização combinatória. Esta proposta considera a forte analogia entre o processo físico de annealing e a resolução de problemas grandes de otimização combinatória. Simulated Annealing (SA) é um denominação genérica para os algoritmos desenvolvidos com base nesta proposta. Estes algoritmos combinam técnicas de busca local e de randomização. O objetivo do presente trabalho é proporcionar um entendimento das características do Simulated Annealing e facilitar o desenvolvimento de algoritmos com estas características. Assim, é apresentado como Simulated Annealing e suas variações estão sendo utilizados na resolução de problemas de otimização combinatória, proposta uma formalização através de um método de desenvolvimento de algoritmos e analisados aspectos de complexidade. O método de desenvolvimento especifica um programa abstrato para um algoritmo Simulated Annealing seqüencial, identifica funções e predicados que constituem os procedimentos deste programa abstrato e estabelece axiomas que permitem a visualização das propriedades que estes procedimentos devem satisfazer. A complexidade do Simulated Annealing é analisada a partir do programa abstrato desenvolvido e de seus principais procedimentos, permitindo o estabelecimento de uma equação genérica para a complexidade. Esta equação genérica é aplicável aos algoritmos desenvolvidos com base no método proposto. Uma prova de correção é apresentada para o programa abstrato e um código exemplo é analisado com relação aos axiomas estabelecidos. O estabelecimento de axiomas tem como propósito definir uma semântica para o algoritmo, o que permite a um desenvolvedor analisar a correção do código especificado para um algoritmo levando em consideração estes axiomas. O trabalho foi realizado a partir de um estudo introdutório de otimização combinatória, de técnicas de resolução de problemas, de um levantamento histórico do uso do Simulated Annealing, das variações em torno do modelo e de embasamentos matemáticos documentados. Isto permitiu identificar as características essenciais dos algoritmos baseados no paradigma, analisar os aspectos relacionados com estas características, como as diferentes formas de realizar uma prescrição de resfriamento e percorrer um espaço de soluções, e construir a fundamentação teórica genérica proposta.

Um Modelo formal e executável de agentes BDI

Modelos BDI (ou seja, modelos Beliefs-Desires-Intentions models) de agentes têm sido utilizados já há algum tempo. O objetivo destes modelos é permitir a caracterização de agentes utilizando noções antropomórficas, tais como estados mentais e ações. Usualmente, estas noções e suas propriedades são formalmente definidas utilizandos formalismos lógicos que permitem aos teóricos analisar, especificar e verificar agentes racionais. No entanto, apesar de diversos sistemas já terem sido desenvolvidos baseados nestes modelos, é geralmente aceito que existe uma distância significativa entre esta lógicas BDI poderosas e sistemas reais. Este trabalho defende que a principal razão para a existência desta distância é que os formalismos lógicos utilizados para definir os modelos de agentes não possuem uma semântica operacional que os suporte. Por “semântica operacional” entende-se tanto procedimentos de prova que sejam corretos e completos em relação à semântica da lógica, bem como mecanismos que realizem os diferentes tipos de raciocínio necessários para se modelar agentes. Há, pelo menos, duas abordagens que podem ser utilizadas para superar esta limitação dos modelos BDI. Uma é estender as lógicas BDI existentes com a semântica operacional apropriada de maneira que as teorias de agentes se tornem computacionais. Isto pode ser alcançado através da definição daqueles procedimentos de prova para as lógicas usadas na definição dos estados mentais. A outra abordagem é definir os modelos BDI utilizando formalismos lógicos apropriados que sejam, ao mesmo tempo, suficientemente poderosos para representar estados mentais e que possuam procedimentos operacionais que permitam a utilizaçao da lógica como um formalismo para representação do conhecimento, ao se construir os agentes. Esta é a abordagem seguida neste trabalho. Assim, o propósito deste trabalho é apresentar um modelo BDI que, além de ser um modelo formal de agente, seja também adequado para ser utilizado para implementar agentes. Ao invés de definir um novo formalismo lógico, ou de estender um formalismo existente com uma semântica operacional, define-se as noções de crenças, desejos e intenções utilizando um formalismo lógico que seja, ao mesmo tempo, formalmente bem-definido e computacional. O formalismo escolhido é a Programação em Lógica Estendida com Negação Explícita (ELP) com a semântica dada pelaWFSX (Well-Founded Semantics with Explicit Negation - Semântica Bem-Fundada com Negação Explícita). ELP com a WFSX (referida apenas por ELP daqui para frente) estende programas em lógica ditos normais com uma segunda negação, a negação explícita1. Esta extensão permite que informação negativa seja explicitamente representada (como uma crença que uma propriedade P não se verifica, que uma intenção I não deva se verificar) e aumenta a expressividade da linguagem. No entanto, quando se introduz informação negativa, pode ser necessário ter que se lidar com programas contraditórios. A ELP, além de fornecer os procedimentos de prova necessários para as teorias expressas na sua linguagem, também fornece um mecanismo para determinar como alterar minimamente o programa em lógica de forma a remover as possíveis contradições. O modelo aqui proposto se beneficia destas características fornecidas pelo formalismo lógico. Como é usual neste tipo de contexto, este trabalho foca na definição formal dos estados mentais em como o agente se comporta, dados tais estados mentais. Mas, constrastando com as abordagens até hoje utilizadas, o modelo apresentanto não é apenas uma especificação de agente, mas pode tanto ser executado de forma a verificar o comportamento de um agente real, como ser utilizado como mecanismo de raciocínio pelo agente durante sua execução. Para construir este modelo, parte-se da análise tradicional realizada na psicologia de senso comum, onde além de crenças e desejos, intenções também é considerada como um estado mental fundamental. Assim, inicialmente define-se estes três estados mentais e as relações estáticas entre eles, notadamente restrições sobre a consistência entre estes estados mentais. Em seguida, parte-se para a definição de aspectos dinâmicos dos estados mentais, especificamente como um agente escolhe estas intenções, e quando e como ele revisa estas intenções. Em resumo, o modelo resultante possui duas características fundamentais:(1) ele pode ser usado como um ambiente para a especificação de agentes, onde é possível definir formalmente agentes utilizando estados mentais, definir formalmente propriedades para os agentes e verificar se estas propriedades são satifeitas pelos agentes; e (2) também como ambientes para implementar agentes.