Publications

In this paper we present a computer assisted proof of the correctness of a partial derivative automata construction from a regular expression within the Coq proof assistant. This proof is part of a formalization of Kleene algebra and regular languages in Coq towards their usage in program certification.

We present a new incremental algorithm for minimising deterministic finite automata. It runs in quadratic time for any practical application and may be halted at any point, returning a partially minimised automaton. Hence, the algorithm may be applied to a given automaton at the same time as it is processing a string for acceptance. We also include some experimental comparative results.

In this paper, the relation between the Glushkov automaton Nfapos and the partial derivative automaton (Nfapd) of a given regular expression, in terms of transition complexity, is studied. The average transition complexity of Nfapos was proved by Nicaud to be linear in the size of the corresponding expression. This result was obtained using an upper bound of the number of transitions of NFApos. Here we present a new l quadratic construction of NFApos that leads to a more elegant and straightforward implementation, and that allows the exact counting of the number of transitions. Based on that, a better estimation of the average size is presented. Asymptotically, and as the alphabet size grows, the number of transitions per state is on average 2.

Broda et al. computed an upper bound for the ratio of the number of states of NFApd to the number of states of NFApos, which is about 1/2 for large alphabet sizes. Here we show how to obtain an upper bound for the number of transitions in NFApd, which we then use to get an average case approximation. Some experimental results are presented that illustrate the quality of our estimate.

In this paper we present a mechanically verified implementation of an algorithm for deciding regular expression (in-)equivalence within the COQ proof assistant. This algorithm is a version of a functional algorithm proposed by Almeida et al. which decides regular expression equivalence through an iterated process of testing the equivalence of their partial derivatives. In particular, this algorithm has a refutation step which improves the process of checking if two regular expressions are not equivalent.

Recently the descriptional complexity of formal languages has been extensively researched. One of the most studied complexity measures for regular languages is the number of states of its minimal automaton (state complexity of the language). Other measures can be related to other structural components and other models of computation. The complexity of a language operation is the complexity of the resulting language seen as a function of the complexities of the operation arguments. This proliferous research gave origin to a multitude of results scattered over more than 200 articles, with the inevitable lack of unified terminology and notation. This makes it very difficult to a interested researcher to have a global perspective of this field and realize what is the current coverage achieved in order to know where to allocate more research efforts. In this paper we present a first step towards the development of a Web based information system were descriptional complexity results can be structurally introduced, queried, and viewed. This tool will also interact with symbolic manipulation systems in order to obtain examples and perform experimental tests. Moreover the system enables the user to easily customize the database queries in order to get novel views over the existing results and respective bounds. Here we describe the main components of the database, the technologies used and the Web user interface.

In this paper, the relation between the Glushkov automaton (nfaPos) and the partial derivative automaton (nfaPd) of a given regular expression, in terms of transition complexity, is studied. The average transition complexity of nfaPos was proved by Nicaud to be linear in the size of the corresponding expression. This result was obtained using an upper bound of the number of transitions of nfaPos. Here we present a new quadratic construction of nfaPos that leads to a more elegant and straightforward implementation, and that allows the exact counting of the number of transitions. Based on that, a better estimation of the average size is presented. Asymptotically, and as the alphabet size grows, the number of transitions per state is on average 2.

Broda et al. computed an upper bound for the ratio of the number of states of nfaPd to the number of states of nfaPos, which is about 1/2 for large alphabet sizes. Here we show how to obtain an upper bound for the number of transitions in nfaPd, which we then use to get an average case approximation. Some experimental results are presented that illustrate the quality of our estimate.

Dynamic languages, like Python, are attractive because they guarantee that no correct program is rejected prematurely. However, this comes at a price of losing early error detection, and making both code optimization and certification harder tasks when compared with static typed languages. Having the static certification of Python programs as a goal, we developed a static type inference system for a subset of Python, known as RPython. Some dynamic features are absent from RPython, nevertheless it is powerful enough as a Python dialect and exhibits most of its main features. Our type inference system tackles with almost all language constructions, such as object inheritance and subtyping, polymorphic and recursive functions, exceptions, generators, modules, etc., and is itself written in Python.

The partial derivative automaton Apd is usually smaller than other nondeterministic finite automata constructed from a regular expression, and it can be seen as a quotient of the Glushkov automaton (Apos). By estimating the number of regular expressions that have epsilon as a partial derivative, we compute a lower bound of the average number of mergings of states in Apos and describe its asymptotic behaviour. This depends on the alphabet size, k, and for growing k's its limit approaches half the number of states in Apos. The lower bound corresponds to consider the Apd automaton for the marked version of the re, i.e. where all its letters are made different. Experimental results suggest that the average number of states of this automaton, and of the APd automaton for the unmarked re, are very close to each other.

Recently, the problem of obtaining a short regular expression equivalent to a given finite automaton has been intensively investigated. Algorithms for converting finite automata to regular expressions have an exponential blow-up in the worst-case. To overcome this, simple heuristic methods have been proposed. In this paper we analyse some of the heuris- tics presented in the literature and propose new ones. We also present some experimental comparative results based on uniform random gener- ated deterministic finite automata.

The partial derivative automaton (NFA_Pd) is usually smaller than other non-deterministic finite automata constructed from a regular expression, and it can be seen as a quotient of the Glushkov automaton (NFA_Pos). By estimating the number of regular expressions that have epsilon as a partial derivative, we compute a lower bound of the average number of mergings of states in NFA_Pos and describe its asymptotic behaviour. This depends on the alphabet size, k, and its limit, as k goes to infinity, is 1/2. The lower bound corresponds exactly to consider the NFA_Pd automaton for the marked version of the RE, i.e. where all its letters are made different. Experimental results suggest that the average number of states of this automaton, and of the NFA_Pos automaton for the unmarked RE, are very close to each other.

Regular expressions (RES), because of their succinctness and clear syntax, are the common choice to represent regular languages. However, efficient pattern matching or word recognition depend on the size of the equivalent nondeterministic finite automata (NFA). We present the implementation of several algorithms for constructing small epsilon-free NFAs from RES within the FAdo system, and a comparison of regular expression measures and NFA sizes based on experimental results obtained from uniform random generated RES. For this analysis, nonredundant RES and reduced RES in star normal form were considered.

The minimal deterministic finite automaton is generally used to determine regular languages equality. Using Brzozowski's notion of derivative, Antimirov and Mosses proposed a rewrite system for deciding regular expressions equivalence of which Almeida et al. presented an improved variant. Hopcroft and Karp proposed an almost linear algorithm for testing the equivalence of two deterministic finite automata that avoids minimisation. In this paper we improve this algorithm's best-case running time, present an extension to non-deterministic finite automata, and establish a relationship with the one proposed in Almeida et al., for which we also exhibit an exponential lower bound. We also present some experimental comparative results.

The partial derivative automaton (NFA_PD) is usually smaller than other non-deterministic finite automata constructed from a regular expression, and it can be seen as a quotient of the Glushkov automaton (NFA_POS). By estimating the number of regular expressions that have epsilon as a partial derivative, we compute a lower bound of the average number of mergings of states in NFA_POS. and describe its asymptotic behaviour. This depends on the alphabet size, k, and its limit, as k goes to infinity, is 1. The lower bound corresponds exactly to consider the NFA_PD automaton for the marked version of the RE, i.e. where all its letters are made different. Experimental results suggest that the average number of states of this automaton, and of the NFA_PD automaton for the unmarked RE, are very close to each other.

This paper presents a brief description of the current work on a tool that analyses temporal behaviour of Ada/RavenSPARK programs. The approach takes as a basis two previous publications that introduce innovative methods in the field of verification of real-time systems. The development of a tool that automatically generates models (timed automata) from Ada/RavenSPARK source code and uses the model checker to verify timing properties is discussed.

As linguagens dinamicamente tipificadas, como a linguagem Python, permitem ao programador uma maior flexibilidade, no entanto privam-no das vantagens da tipificação estática, como a detecção precoce de erros. Este artigo tem como objectivo descrever um sistema estático de tipos para um subconjunto do Python (RPython). Acreditamos que a definição de um este sistema de inferência de tipos, como este, é um passo importante para a construção de um sistema de verificação formal de programas Python.

GUItar is a graphical environment for graph visualization, editing, and interaction, that specially focuses in finite automata dia- grams. The application incorporates mechanisms to facilitate the editing of these graphs. It also provides a style manager that allows the cre- ation of rich state and arc styles to be used in the drawing of its ob- jects. This style manager allows the system to cope with complex styles, broaden the application scope to graphical representations of other com- putational models like transducers or Turing machines. GUItar also has a foreign function call (FFC) mechanism for the easy integration of exter- nal modules and libraries like automata symbolic manipulators or graph drawing libraries. For automatic graph drawing we are developing FA- goo, a package that seeks to provide tools capable of finding pleasant graph drawings. FAgoo implements graph drawing algorithms that find embeddings which the user, with minimal manual changes, can adjust to its aesthetically taste. Both GUItar and FAgoo are on going projects licensed under GPL.

GUItar is a visualization software tool for various types of automata (standard, weighted, pushdown, transducers, Turing machines, etc.). It provides interactive manipulation of diagrams, comprehensive graphic style creation, multiple export/import filters, and a generic "foreign function calls" (ffc) interface with external systems. In this paper we describe GUItar's XML framework and show how it allows for extensibility, modularity and interoperability.

FAdo is an ongoing project which aims to provide a set of tools for symbolic manipulation of formal languages. To allow high-level programming with complex data structures, easy prototyping of algorithms, and portability (to use in computer grid systems for example), are its main features. Our main motivation is the theoretical and experimental research, but we have also in mind the construction of a pedagogical tool for teaching automata theory and formal languages. For the graphical visualization and interactive manipulation a new interface application, GUItar, is being developed. In this paper, we describe the main components of the FAdo system as well as the basics of the graphical interface and editor, the export/import filters and its generic interface with external systems, such as FAdo.

Computing short regular expressions equivalent to a given finite automaton is a hard task. In this work we present a class of acyclic automata for which it is possible to obtain in time O(n^2logn) an equivalent regular expression of size O(n). A characterisation of this class is made using properties of the underlying digraphs that correspond to the series-parallel digraphs class. Using this characterisation we present an algorithm for the generation of automata of this class and an enumerative formula for the underlying digraphs with a given number of vertices.

In this article we describe an implementation of Kleene algebra with tests (KAT) in the Coq theorem prover. KAT is an equational system that has been successfully applied in program verification and, in particular, it subsumes the propositional Hoare logic (PHL). We also present an PHL encoding in KAT, by deriving its deduction rules as theorems of KAT. Some examples of simple program's formal correctness are given. This work is part of a study of the feasibility of using KAT in the automatic production of certificates in the context of (source-level) Proof-Carrying-Code (PCC).

Antimirov and Mosses proposed a rewrite system for deciding the equivalence of two (extended) regular expressions. In this paper we present a functional approach to that method, prove its correctness, and give some experimental comparative results. Besides an improved version of AM's algorithm, we present a version using partial derivatives. Our preliminary results lead to the conclusion that, indeed, these methods are feasible and, generally, faster than the classical methods.

We give a canonical representation for minimal acyclic deterministic finite automata (Madfa) with n states over an alphabet of k symbols. Using this normal form, we present a method for the exact generation of Madfas. This method avoids a rejection phase that would be needed if a generation algorithm for a larger class of objects that contains the Madfas were used. We give upper and lower bounds for Madfas enumeration and some exact formulas for small values of n.

We present an interactive graphical environment for the manipulation of context-free languages. The graphical environment allows the editing of a context-free grammar, the conversion to Chomsky normal form, word parsing and the (interactive) construction of parse trees. It is possible to store positive and negative datasets of words to be tested by a given grammar. The main goal of this system is to provide a pedagogical tool for studying grammar construction and parse trees.

We give a canonical representation for trim acyclic deterministic finite automata (Adfas) with n states over an alphabet of k symbols. Using this normal form, we present a backtracking algorithm for the exact generation of Adfas. This algorithm is a non trivial adaptation of the algorithm for the exact generation of minimal acyclic deterministic finite automata , presented by Almeida et al..

Apart from the theoretical worst-case running time analysis not much is known about the average-case analysis or practical performance of finite automata minimization algorithms. On this paper we compare the running time of four minimization algorithms based on experimental results, and apply them to both deterministic and non-deterministic random automata. Although there is no clear winner, some conclusions can be taken for specific cases. Hopcroft's algorithm performs better for Dfas with small alphabets, and, regardless of the alphabet size, Brzozowski's algorithm is the clearly the fastest dealing with Nfas.

Emotional-BDI agents are BDI agents whose behaviour is guided not only by beliefs, desires and intentions, but also by the role of emotions in reasoning and decision-making. The Ebdi logic is a formal system for expressing the concepts of the Emotional-BDI model of agency. In this paper we present an improved version of the Ebdi logic and show how it can be used to model the role of three emotions in Emotional-BDI agents: fear, anxiety and self-confidence. We also focus in the computational properties of Ebdi which can lead to its use in automated proof systems.

There are several well known algorithms to minimize deterministic finite automata. Apart from the theoretical worst-case running time analysis, however, not much is known about the average-case analysis or practical performance of each of these algorithms. On this paper we compare three minimization algorithms based on experimental results. The choice of the algorithms was based on the fact that although having different worst-case complexities they are usually considered to be ones that achieve best performance. We used an uniform random generator of (initially-connected) deterministic finite automata for the input data, and thus our results are statistically accurate. Because one of the algorithms allowed to minimize non-deterministic finite automata (NFA), we also developed a non-uniform random generator for NFAs. Nevertheless, although not statistically significant, the results in this case are fairly interesting.

Emotional-BDI agents are BDI agents whose behaviour is guided not only by beliefs, desires and intentions, but also by the role of emotions in reasoning and decision-making. The EBDI logic is a formal system for expressing the concepts of the Emotional-BDI model of agency. In this paper we present an improved version of the EBDI logic and show how it can be used to model the role of three emotions in Emotional-BDI agents: fear, anxiety and self-confidence. We also focus in the computational properties of EBDI which can lead to its use in automated proof systems.

We give a canonical representation for minimal acyclic deterministic finite automata (MADFA) with n states over an alphabet of k symbols. Using this normal form, we present a method for the exact generation of MADFAs. This method avoids a rejection phase, that would be needed if a generation algorithm for a larger class of objects that contains the MADFAs were used. We give an upper bound for MADFAs enumeration that is exact for small values of n.

Neste trabalho, apresentamos um conjunto de ferramentas, baseadas em tecnologias XML, para a produção, indexação, classificação e pesquisa de documentos multimédia associados a entrevistas. Estas ferramentas foram desenvolvidas no âmbito do projecto de história oral da Universidade Popular do Porto cujo objectivo é a preservação e divulgação da memória social e laboral do Porto no séc. XX.

The representation of combinatorial objects is decisive for the feasibility of several enumerative tasks. In this work, we present a unique string representation for complete initially-connected deterministic automata (ICDFAs) with n states over an alphabet of k symbols. For these strings we give a regular expression and show how they are adequate for exact and random generation, allow an alternative way for enumeration and lead to an upper bound for the number of ICDFAs. The exact generation algorithm can be used to partition the set of ICDFAs in order to parallelize the counting of minimal automata, and thus of regular languages. A uniform random generator for ICDFAs is presented that uses a table of pre-calculated values. Based on the same table, an optimal coding for ICDFAs is obtained.

The representation of combinatorial objects is decisive for the feasibility of several enumerative tasks. In this work, we present a (unique) string representation for (complete) initially-connected deterministic automata (ICDFA's) with n states over an alphabet of k symbols. For these strings we give a regular expression and show how they are adequate for exact and random generation, allow an alternative way for enumeration and lead to an upper bound for the number of ICDFA's. The exact generation algorithm can be used to partition the set of ICDFA's in order to parallelize the counting of minimal automata (and thus of regular languages). A uniform random generator for ICDFA's is presented that uses a table of pre-calculated values. Based on the same table, an optimal coding for ICDFA's is obtained. We also establish an explicit relationship between our method and the one used by Nicaud et al.

In general, the representation of combinatorial objects is decisive for the feasibility of several enumerative tasks. In this work, we show how a (unique) string representation for (complete) initially-connected deterministic automata (ICDFA's) with n states over an alphabet of k symbols can be used for counting, exact enumeration, sampling and optimal coding, not only the set of ICDFA's but, to some extent, the set of regular languages. An exact generation algorithm can be used to partition the set of ICDFA's in order to parallelize the counting of minimal automata (and thus of regular languages). We present also a uniform random generator for ICDFA's that uses a table of pre-calculated values. Based on the same table it is also possible to obtain an optimal coding for ICDFA's.

Emotional-BDI agents are agents whose behaviour is guided not only by beliefs, desires and intentions, but also by the role of emotions in reasoning and decision-making. In this paper we introduce the logic for specifying Emotional-BDI agents in general and a special kind of Emotional-BDI agent under the effect of fear. The focus of this work is in the expressiveness of and on using it to establish some properties which agents under the effect of an emotion should exhibit.

We present a conditional rewrite system for arithmetic and membership univariate constraints over real numbers, designed for computer assisted learning (CAL) in elementary math. Two fundamental principles guided the design of the proposed rewrite rules: cognitive fidelity (emulating steps students should take) and correctness, aiming that step-by-step solutions to problems look like ones carried out by students. In order to gain more flexibility to modify rules, add new ones and customize solvers, the rules are written in a specification language and then compiled to Prolog. The rewrite system is complete for a relevant subset of problems found in high-school math textbooks.

In this report we present the Emotional-BDI architecture, an extension to the BDI architecture supporting Artificial Emotions and including internal representations for agent's Capabilities and Resources. The architecture we present here, is conceptual, defining which components should exist so that Emotional- BDI agents can use Effective Capabilities as well as Effective Resources in order to better cope with highly dynamic environments.

We present a solver for arithmetic and membership constraints over real numbers, for computer assisted learning (CAL) in math. The solver works as a rewrite system. What makes it novel are the proposed rewriting rules that go beyond simple algebraic reductions. Instead they work at high abstraction level and use some knowledge about the functions behaviour to shortcut solving steps. Designed with pedagogic concerns, they are useful to produce step-by-step solutions that look like ones worked out by students. In this way the solver may be more advantageous in some learning environments than sophisticated mathematical software, which is certainly the choice for scientific applications and advanced algebraic manipulations. The proposed solver is correct and although it is complete for a relevant set of problems arising in high-school math curricula, it is incomplete in general. Indeed, this is inherent to the addressed problem. A prototype is being developed in Prolog for a specific application domain, reusing some modules of Demomath for symbolic manipulation of sets and exact arithmetic, that employ CLP(Q) and CLP(R) to some extent. This work is part of AGILMAT project in which a web application to automatically generate and solve math drills is being developed.

We give an unique string representation, up to isomorphism, for initially connected deterministic finite automata (ICDFA's) with n states over an alphabet of k symbols. We show how to generate all these strings for each n and k, and how its enumeration provides an alternative way to obtain the exact number of ICDFA's.

Computing short regular expressions equivalent to a given finite automaton is a hard task. In this work we present a class of acyclic automata for which it is easy-to-find a regular expression that has linear size. We call those automata UDR. A UDR automaton is characterized by properties of its underlying digraph. We present a characterisation theorem and an efficient algorithm to determine if an acyclic automaton is UDR. This algorithm can be adapted to compute a short regular expression equivalent to a given UDR automaton.

FAdo is an ongoing project which aims the development of an interactive environment for symbolic manipulation of formal languages. In this paper we focus in the description of interactive tools for teaching and assisting research on regular languages, and in particular finite automata and regular expressions. Those tools implement most standard automata operations, conversion between automata and regular expressions, and word recognition. We illustrate their use in training and automatic assessment. Finally we present a graphical environment for editing and interactive visualisation.

Keywords: Automata theory, Interactive visual tools, e-learning

Com o advento da sociedade digital aparecem novos paradigmas na área da educação. É fundamental conceber soluções de e-Learning que flexibilizem o acesso aos recursos de aprendizagem. Assim, neste trabalho, apresenta-se o desenho duma plataforma que assenta nos princípios básicos de desenvolvimento das aplicações de e-Learning, mas com agregação de funcionalidades que permitirão aos professores manter a sua informação organizada e disponível. Para tal definiu-se uma linguagem XML para a manipulação de exercícios e de testes, que serve de base para o desenvolvimento duma aplicação que permita aos professores a edição de exercícios de diferentes disciplinas, para posterior elaboração, aleatória ou assistida, de documentos de apoio às aulas e de avaliação, e sua resolução e correcção. Também os alunos poderão, gerar testes de treino e de avaliação. Pretende-se ainda que a maior parte dos exercícios sejam de correcção automática, para permitir uma avaliação interactiva e mais frequente.

Keywords: e-learning,XML, integrated knowledge management,automatic assessement

We present a family of regular languages representing partitions of a set N_n={1,...,n} in less or equal c parts. We determine explicit formulas for the density of those languages and their relationship with well known integer sequences involving Stirling numbers of second kind. We also determine their limit frequency. This work was motivated by computational representations of the configurations of some numerical games.

In one of his numerous lectures, Frank Harary, talked about one of his many games, that, as usual, had a very difficult problem associated to it. In this case, a family of games for two players in which the selected number of columns in the game has a vital importance. He has proved that for 2 and 3 columns the longest match has 9 and 24 moves respectively, that is to say that H2=9 and H3=24. At the same time it was announced that he knew a solution of length 67 for the problem with 4 columns, but he didn't know if it was the maximum. We present here a program that proves that H4=67. Although it uses but a brute-force approach, its soundness seems good fun to prove.

We propose a web-based timetabling system for a typical situation in universities, where agents (usually departments or faculties) compete for a set of resources (class rooms) on a given number of time slots. Each agent (typically a person, on the behalf of a department) proposes the placement (room and time) for events. A dispatching system decides which event should be scheduled next, based on a pre-established set of rules, and asks its placement to the corresponding department. The system also includes a solver that suggests the placement of an event to each agent, thus allowing a completely automated timetable construction. We describe a prototype being implemented at the Faculty of Sciences, University of Porto.

FAdo is an ongoing project which goal is the development of a Python environment for manipulation of finite automata and regular expressions. Currently it provides most standard automata operations including conversion from deterministic to non-deterministic, minimisation, boolean operations, concatenation, conversion between automata and regular expressions, and word recognition. It includes, also, an innovative method for testing non-equivalence of two automata (or regular expressions) using a DFA canonical form and a witness generator of the difference of two automata.

Our main motivation is the development of interactive tools for teaching concepts in automata theory and formal languages. Towards this goal we are also developing graphical tools for creating and manipulating automata and a graphical user interface.

Keywords: Automata theory, Interactive visual tools, e-learning

Edic is a Web courseware for an introductory course on the UNIX operating system. In this research we developed a XML language for describing pedagogical content and an exploratory environment, as means for structuring the courseware. In this paper we describe the XML language and its conversion to HTML, introducing graphical layout and navigation. We describe also the exploratory environment and its features for assisted execution, visualisation of the file system and automatic grading of exercises.

Keywords: E-Learning, ICT, XML, exploratory environment

The traditional method of automatically assessing programming exercises in Computer Science uses a black-box approach where a set of test data is inputed to both students and teachers programs and their outputs compared. This approach is useful for grading but inadequate for detecting and correcting students errors. In this paper we present several cases where we were able to develop matching algorithms to compare answers with solutions and pinpoint differences between them. In some cases the matching is based on the actual structure of answers and solutions. In other cases we use execution side-effects to collect a structure that can be compared using a matching algorithm. This approach is currently being used in Ganesh - a web environment for learning Computer Science.

Keywords: Program assessment; Computer assisted instruction

This report describes a system for solving programming exercises in a controlled environment allowing the evaluation of the student's programming skills. The system's main component is the solving environment in which the students solves individually the examination, and submits it for automatic grading. The system provides also a monitoring environment to be used by the course teacher to oversee the examination.

In this report we include an evaluation of the described system based on feedback of students and teachers. This evaluation lead to the proposal of directions for future research.

Keywords: Program assessment; Computer assisted instruction

Teaching the very basic concepts of a computer architecture, instruction set and operation, based on a real microprocessor is usually an unfruitful task as the essential notions are obscured by the specific details of its architecture. A machine emulator has the benefit of providing a portable environment that can run in several platforms and that can be easily adapted for pedagogical purposes. In this work we present an environment for a first course in assembly language programming that aims to be a flexible and effective pedagogical tool. Apoo is a virtual machine with a very simple architecture and instruction set that mimics almost all the essential features of a modern microprocessor. The Apoo Interface is a graphical environment that monitors the state of the machine during the execution of a program and allows the writing/editing/execution of programs in assembly language. The Apoo Tutor is a module that aims the grading of student programs based on a description of what should be the execution of the program for specified input data sets. This module is currently used to evaluate students programming skills in an interactive, Web based learning/grading system, not only allowing the detection of errors but trying to give extra information in order that the student can understand and correct his/her mistakes more easily.

In recent years, symbolic constraints have raised a considerable interest in several areas of computation and particularly in the Computational Linguistics community. As a matter of fact constraints over the algebra of rational trees can significantly contribute to the reduction of the search space of problems in Natural Language Processing, while increasing the formalisms expressive power. In this thesis we developed a formal and computational framework for constraint languages over the algebras of finite, rational and feature trees. Although, the first-order theories of these algebras are decidable, they are computationally intractable. Our goal was to design a formal model and decision procedures to face that problem, and that have been (successfully) used in the implementation of several grammar formalisms, called constraint logic grammars (CLG).

The main contributions of this thesis are:

Complete solvers for complex constraints in the algebras of finite and rational trees. In order to face the NP-hardness of the satisfiability problem for complex constraints, our approach was based in factoring out, in polynomial time, deterministic information contained in a complex constraint, simplifying the remaining formula using that information and delaying as much as possible the explosion of disjunctions. We also developed rewrite systems for detection of common factors in disjuncts and rewrite systems that use negative information for the simplification process. We investigated the problem of eliminating negative constraints and presented a decision procedure for finite signatures.

Establishment of a relation between the algebra of rational trees and the algebra of feature trees, such that the satisfiability problem in one can be reduced to the satisfiability problem in the other. A method for the computation of the minimal models of certain classes of satisfiable constraints. These characterizations are useful to simplify and to detect equivalent constraints. A low-level implementation of the main features of the complete solvers.

A higher order tree descriptions Calculus based on a typed λ-calculus, which extended the previous techniques developed for resolving complex constraints. The higher order tree descriptions were used as semantic representations in categorial grammars for Natural Language.

Although unification can be used to implement a weak form of β-reduction, several linguistic phenomena are better handled by using some form of λ-calculus. In this paper we present a higher order feature description calculus based on a typed λ-calculus. We show how the techniques used in CLG for resolving complex feature constraints can be efficiently extended. CCLG is a simple formalism, based on categorial grammars, designed to test the practical feasibility of such a calculus.

Keywords: constraint satisfaction, computational semantics, high-order programming.

This work presents a constraint solver for the domain of rational trees. Since the problem is NP-hard the strategy used by the solver is to reduce as much as possible, in polynomial time, the size of the constraints using a rewriting system before applying a complete algorithm. This rewriting system works essentially by rewriting constraints using the information in a partial model. An efficient C implementation of the rewriting system is described and an algorithm for factoring complex constraints is also presented.

We present an algorithm for decidibility of formulas over the Herbrand Universe with an infinite alphabet, based on rewriting rules and quantifier elimination.

In this paper a model for temporal references in natural language (NL) is studied and a Prolog implementation of it is presented. This model is intended to be a common framework for semantic analysis of verb tenses and temporal adverbial phrases. The time model choosen was based on time intervals and temporal relations. The notion of “proposition type” and temporal concepts of tense, aspect, duration, location and iteration were represented as temporal relations between some special time intervals and temporal quantifiers over time intervals. The implementation consisted in extending an existing semantic analyser.

Keywords: Natural Language Understanding