Skolemization for Substructural Logics

The usual Skolemization procedure, which removes strong quantifiers by introducing new function symbols, is in general unsound for first-order substructural logics defined based on classes of complete residuated lattices. However, it is shown here (following similar ideas of Baaz and Iemhoff for first-order intermediate logics in [1]) that first-order substructural logics with a semantics satisfying certain witnessing conditions admit a ���parallel��� Skolemization procedure where a strong quantifier is removed by introducing a finite disjunction or conjunction (as appropriate) of formulas with multiple new function symbols. These logics typically lack equivalent prenex forms. Also, semantic consequence does not in general reduce to satisfiability. The Skolemization theorems presented here therefore take various forms, applying to the left or right of the consequence relation, and to all formulas or only prenex formulas.

An improved bit parallel exact maximum clique algorithm

This paper describes new improvements for BB-MaxClique (San Segundo et al. in Comput Oper Resour 38(2):571���581, 2011 ), a leading maximum clique algorithm which uses bit strings to efficiently compute basic operations during search by bit masking. Improvements include a recently described recoloring strategy in Tomita et al. (Proceedings of the 4th International Workshop on Algorithms and Computation. Lecture Notes in Computer Science, vol 5942. Springer, Berlin, pp 191���203, 2010 ), which is now integrated in the bit string framework, as well as different optimization strategies for fast bit scanning. Reported results over DIMACS and random graphs show that the new variants improve over previous BB-MaxClique for a vast majority of cases. It is also established that recoloring is mainly useful for graphs with high densities.

Hiord: A type-free higher-order logic programming language with predicate abstraction

A new formalism, called Hiord, for defining type-free higherorder logic programming languages with predicate abstraction is introduced. A model theory, based on partial combinatory algebras, is presented, with respect to which the formalism is shown sound. A programming language built on a subset of Hiord, and its implementation are discussed. A new proposal for defining modules in this framework is considered, along with several examples.

An Introductory Course on Constraint Logic Programming

The purpose of this document is to serve as the printed material for the seminar "An Introductory Course on Constraint Logic Programming". The intended audience of this seminar are industrial programmers with a degree in Computer Science but little previous experience with constraint programming. The seminar itself has been field tested, prior to the writing of this document, with a group of the application programmers of Esprit project P23182, "VOCAL", aimed at developing an application in scheduling of field maintenance tasks in the context of an electric utility company. The contents of this paper follow essentially the flow of the seminar slides. However, there are some differences. These differences stem from our perception from the experience of teaching the seminar, that the technical aspects are the ones which need more attention and clearer explanations in the written version. Thus, this document includes more examples than those in the slides, more exercises (and the solutions to them), as well as four additional programming projects, with which we hope the reader will obtain a clearer view of the process of development and tuning of programs using CLP. On the other hand, several parts of the seminar have been taken out: those related with the account of fields and applications in which C(L)P is useful, and the enumerations of C(L)P tools available. We feel that the slides are clear enough, and that for more information on available tools, the interested reader will find more up-to-date information by browsing the Web or asking the vendors directly. More details in this direction will actually boil down to summarizing a user manual, which is not the aim of this document.

Modelado y Comparaci��n de Colecciones en la Web Sem��ntica

En esta tesis se estudia la representaci��n, modelado y comparaci��n de colecciones mediante el uso de ontolog��as en el ��mbito de la Web Sem��ntica. Las colecciones, entendidas como agrupaciones de objetos o elementos con entidad propia, son construcciones que aparecen frecuentemente en pr��cticamente todos los dominios del mundo real, y por tanto, es imprescindible disponer de conceptualizaciones de estas estructuras abstractas y de representaciones de estas conceptualizaciones en los sistemas inform��ticos, que definan adecuadamente su sem��ntica. Mientras que en muchos ��mbitos de la Inform��tica y la Inteligencia Artificial, como por ejemplo la programaci��n, las bases de datos o la recuperaci��n de informaci��n, las colecciones han sido ampliamente estudiadas y se han desarrollado representaciones que responden a multitud de conceptualizaciones, en el ��mbito de la Web Sem��ntica, sin embargo, su estudio ha sido bastante limitado. De hecho hasta la fecha existen pocas propuestas de representaci��n de colecciones mediante ontolog��as, y las que hay s��lo cubren algunos tipos de colecciones y presentan importantes limitaciones. Esto impide la representaci��n adecuada de colecciones y dificulta otras tareas comunes como la comparaci��n de colecciones, algo cr��tico en operaciones habituales como las b��squedas sem��nticas o el enlazado de datos en la Web Sem��ntica. Para solventar este problema esta tesis hace una propuesta de modelizaci��n de colecciones basada en una nueva clasificaci��n de colecciones de acuerdo a sus caracter��sticas estructurales (homogeneidad, unicidad, orden y cardinalidad). Esta clasificaci��n permite definir una taxonom��a con hasta 16 tipos de colecciones distintas. Entre otras ventajas, esta nueva clasificaci��n permite aprovechar la sem��ntica de las propiedades estructurales de cada tipo de colecci��n para realizar comparaciones utilizando las funciones de similitud y disimilitud m��s apropiadas. De este modo, la tesis desarrolla adem��s un nuevo cat��logo de funciones de similitud para las distintas colecciones, donde se han recogido las funciones de (di)similitud m��s conocidas y tambi��n algunas nuevas. Esta propuesta se ha implementado mediante dos ontolog��as paralelas, la ontolog��a E-Collections, que representa los distintos tipos de colecciones de la taxonom��a y su axiom��tica, y la ontolog��a SIMEON (Similarity Measures Ontology) que representa los tipos de funciones de (di)similitud para cada tipo de colecci��n. Gracias a estas ontolog��as, para comparar dos colecciones, una vez representadas como instancias de la clase m��s apropiada de la ontolog��a E-Collections, autom��ticamente se sabe qu�� funciones de (di)similitud de la ontolog��a SIMEON pueden utilizarse para su comparaci��n. Abstract This thesis studies the representation, modeling and comparison of collections in the Semantic Web using ontologies. Collections, understood as groups of objects or elements with their own identities, are constructions that appear frequently in almost all areas of the real world. Therefore, it is essential to have conceptualizations of these abstract structures and representations of these conceptualizations in computer systems, that define their semantic properly. While in many areas of Computer Science and Artificial Intelligence, such as Programming, Databases or Information Retrieval, the collections have been extensively studied and there are representations that match many conceptualizations, in the field Semantic Web, however, their study has been quite limited. In fact, there are few representations of collections using ontologies so far, and they only cover some types of collections and have important limitations. This hinders a proper representation of collections and other common tasks like comparing collections, something critical in usual operations such as semantic search or linking data on the Semantic Web. To solve this problem this thesis makes a proposal for modelling collections based on a new classification of collections according to their structural characteristics (homogeneity, uniqueness, order and cardinality). This classification allows to define a taxonomy with up to 16 different types of collections. Among other advantages, this new classification can leverage the semantics of the structural properties of each type of collection to make comparisons using the most appropriate (dis)similarity functions. Thus, the thesis also develops a new catalog of similarity functions for the different types of collections. This catalog contains the most common (dis)similarity functions as well as new ones. This proposal is implemented through two parallel ontologies, the E-Collections ontology that represents the different types of collections in the taxonomy and their axiomatic, and the SIMEON ontology (Similarity Measures Ontology) that represents the types of (dis)similarity functions for each type of collection. Thanks to these ontologies, to compare two collections, once represented as instances of the appropriate class of E-Collections ontology, we can know automatically which (dis)similarity functions of the SIMEON ontology are suitable for the comparison. Finally, the feasibility and usefulness of this modeling and comparison of collections proposal is proved in the field of oenology, applying both E-Collections and SIMEON ontologies to the representation and comparison of wines with the E-Baco ontology.

A parallel method for impulsive image noise removal on hybrid CPU/GPU systems

A parallel algorithm for image noise removal is proposed. The algorithm is based on peer group concept and uses a fuzzy metric. An optimization study on the use of the CUDA platform to remove impulsive noise using this algorithm is presented. Moreover, an implementation of the algorithm on multi-core platforms using OpenMP is presented. Performance is evaluated in terms of execution time and a comparison of the implementation parallelised in multi-core, GPUs and the combination of both is conducted. A performance analysis with large images is conducted in order to identify the amount of pixels to allocate in the CPU and GPU. The observed time shows that both devices must have work to do, leaving the most to the GPU. Results show that parallel implementations of denoising filters on GPUs and multi-cores are very advisable, and they open the door to use such algorithms for real-time processing.

A Code for zero-one integer programming, ILLIP-2 : a programming manual for ILLIP-2 /

"UILU-ENG 77 1711."

Numerical software, science or alchemy? /

Bibliography: p. 23-34.

An algorithm for solving linear recurrence systems on parallel and pipelined machines /

"UILU-ENG 78 1745."

Adaptive merging by parallel disjoint comparisons /

Includes bibliographical references.

The concept of time in programming languages.

Thesis (M.S.)--University of Illinois at Urbana-Champaign.

A parallel QR-algorithm for tridiagonal symmetric matrices /

"NSF-OCA-GJ-36936-000008."

Parallel techniques.

Originally presented as the author's thesis, University of Illinois at Urbana-Champaign.