This work focuses on the presentation of a methodology for the development and verification of expressive ontologies. Motivated by experiences with the development of first-order logic ontologies, we call attention to the inadequacies of existing development methodologies for expressive ontologies. We attempt to incorporate pragmatic considerations inspired by our experiences while maintaining the rigorous definition and verification of requirements necessary for the development of expressive ontologies. We leverage automated reasoning tools to enable semiautomatic verification of requirements, and to assist other aspects of development where possible. In addition, we discuss the related issue of ontology quality, and formulate a set of requirements for MACLEOD - a proposed development tool that would support our lifecycle.

This work focuses on the presentation of a methodology for the development and verification of expressive ontologies. Motivated by experiences with the development of first-order logic ontologies, we call attention to the inadequacies of existing development methodologies for expressive ontologies. We attempt to incorporate pragmatic considerations inspired by our experiences while maintaining the rigorous definition and verification of requirements necessary for the development of expressive ontologies. We leverage automated reasoning tools to enable semiautomatic verification of requirements, and to assist other aspects of development where possible. In addition, we discuss the related issue of ontology quality, and formulate a set of requirements for MACLEOD - a proposed development tool that would support our lifecycle.

In this thesis we investigate the design and complexity analysis of the algorithms to solve convex programming problems under inexact first-order information. In the first part of this thesis we focus on the general non-smooth convex minimization under a stochastic oracle. We start by introducing an important algorithmic advancement in this area, namely, the development of the mirror descent stochastic approximation algorithm. The main contribution is to develop a validation procedure for this algorithm applied to stochastic programming. In the second part of this thesis we consider the Stochastic Composite Optimizaiton (SCO) which covers smooth, non-smooth and stochastic convex optimization as certain special cases. Note that the optimization algorithms that can achieve this lower bound had never been developed. Our contribution in this topic mainly consists of the following aspects. Firstly, with a novel analysis, it is demonstrated that the simple RM-SA algorithm applied to the aforementioned problems exhibits the best known so far rate of convergence. Moreover, by adapting Nesterov's optimal method, we propose an accelerated SA, which can achieve, uniformly in dimension, the theoretically optimal rate of convergence for solving this class of problems. Finally, the significant advantages of the accelerated SA over the existing algorithms are illustrated in the context of solving a class of stochastic programming problems. In the last part of this work, we extend our attention to certain deterministic optimization techniques which operate on approximate first-order information for the dual problem. In particular, we establish, for the first time in the literature, the iteration-complexity for the inexact augmented Lagrangian (I-AL) methods applied to a special class of convex programming problems.

Ce mémoire présente le résultat de mon travail de thèse sur la génération d'impliqués premiers en logique équationnelle fermée, i.e., la génération des conséquences les plus générales de formules logiques contenants des équations et des disequations entre termes sans variables. Ce mémoire est divisé en trois parties. Tout d'abord, deux calculs de génération d'impliqués sont définis. Leur complétude pour la déduction est prouvée, ce qui signifie qu'ils sont tous deux capables de générer l'ensemble des impliqués modulo redondance d'une formule équationnelle fermée. Dans une deuxième partie, une structure de données arborescente est proposée pour stocker les impliqués générés, accompagnée d'algorithmes pour déceler les redondances et couper les branches de l'arbre lorsque c'est nécessaire. Cette structure de données est adaptée aux différents types de clauses (avec et sans symboles de fonctions, avec et sans contraintes) ainsi qu'aux différentes notions de redondance utilisées dans les calculs. En effet, chaque calcul utilise un critère de redondance légèrement différent des autres. Les preuves de correction et de terminaison des algorithmes sont fournies pour chaque algorithme. Enfin, une évaluation expérimentale des différentes méthodes de génération d'impliqués premiers est réalisée. Pour cela, un prototype de ces méthodes, écrit en Ocaml est comparé à des outils de génération d'impliqués premiers récents.Les résultats de ces expériences sont utilisés pour identifier les variantes les plus efficaces des algorithmes proposés. Les résultats sont prometteurs et dans la plupart des cas, meilleurs que ceux de l'état de l'art. / The work presented in this memoir deals with the generation of prime implicates in ground equational logic, i.e., of the most general consequences of formulae containing equations and disequations between ground terms.It is divided in three parts. First, two calculi that generate implicates are defined. Their deductive-completeness is proved, meaning they can both generate all the implicates up to redundancy of equational formulae.Second, a tree data structure to store the generated implicates is proposed along with algorithms to detect redundancies and prune the branches of the tree accordingly. This data structure is adapted to the different kinds of clauses (with and without function symbols, with and without constraints) and to the various formal definitions of redundancy used in the calculi since each calculus uses different -- although similar -- redundancy criteria. Termination and correction proofs are provided with each algorithm. Finally, an experimental evaluation of the different prime implicate generation methods based on research prototypes written in Ocaml is conducted including a comparison with state-of-the-art prime implicate generation tools. This experimental study is used to identify the most efficient variants of the proposed algorithms. These show promising results overstepping the state of the art.

abstract: Natural Language Processing is a subject that combines computer science and linguistics, aiming to provide computers with the ability to understand natural language and to develop a more intuitive human-computer interaction. The research community has developed ways to translate natural language to mathematical formalisms. It has not yet been shown, however, how to automatically translate different kinds of knowledge in English to distinct formal languages. Most of the recent work presents the problem that the translation method aims to a specific formal language or is hard to generalize. In this research, I take a first step to overcome this difficulty and present two algorithms which take as input two lambda-calculus expressions G and H and compute a lambda-calculus expression F. The expression F returned by the first algorithm satisfies F@G=H and, in the case of the second algorithm, we obtain G@F=H. The lambda expressions represent the meanings of words and sentences. For each formal language that one desires to use with the algorithms, the language must be defined in terms of lambda calculus. Also, some additional concepts must be included. After doing this, given a sentence, its representation and knowing the representation of several words in the sentence, the algorithms can be used to obtain the representation of the other words in that sentence. In this work, I define two languages and show examples of their use with the algorithms. The algorithms are illustrated along with soundness and completeness proofs, the latter with respect to typed lambda-calculus formulas up to the second order. These algorithms are a core part of a natural language semantics system that translates sentences from English to formulas in different formal languages. / Dissertation/Thesis / M.S. Computer Science 2010

Orientador: Walter Carnielli / Dissertação (mestrado) - Universidade Estadual de Campinas, Instituto de Filosofia e Ciencias Humanas / Made available in DSpace on 2018-08-12T05:55:31Z (GMT). No. of bitstreams: 1 Podiacki_Rodrigo_M.pdf: 538726 bytes, checksum: 3a51529177d89ce92122bde746a321c3 (MD5) Previous issue date: 2008 / Resumo: Esta dissertação tem como objetivo desenvolver uma semântica correta e completa para uma classe de lógicas de primeira ordem conhecidas como Lógicas da Inconsistência Formal (LIFs). Após uma elucidação geral sobre semânticas paraconsistentes e de primeira ordem, uma LIF particular, chamada QmbC, será caracterizada axiomaticamente. Em seguida será construída uma semÂntica que se demonstrará correta e completa para a LIF em questão. Por fim, uma série de LIFs com propriedades sintáticas interessantes serão caracterizadas axiomaticamente, e será visto como a semântica construída para QmbC pode ser estendida para todas essas lógicas. / Abstract: This dissertation aims to develop a sound and complete semantics for a class of first-order logics known as Logics of Formal Inconsistency (LFIs). After general explanation about paraconsistent and first-order semantics, a particular LFI, labeled QmbC, will be characterized by means of an axiom system. Then a sound and complete semantics for it will be constructed. Finally, a variety of LFIs having nice syntactic properties will be axiomatically defined, and it will be shown how the semantics proposed for QmbC can be extended for all these logics. / Mestrado / Filosofia / Mestre em Filosofia

The purpose of this master thesis was to investigate which of the two methods, resolution and tableaux, that is the most appropriate for automated theorem proving. This was done by implementing an automated theorem prover, comparing and documenting implementation problems, and measuring proving efficiency. In this thesis, I conclude that the resolution method might be more suitable for an automated theorem prover than tableaux, in the aspect of ease of implementation. Regarding the efficiency, the test results indicate that resolution is the better choice. / Syftet med detta magisterarbete var att undersöka vilken av de två metoderna, resolution och tablå, som är mest lämpad för automatisk teorembevisning. Detta gjordes genom att implementera en automatisk teorembevisare, jämföra och dokumentera problem, samt att mäta prestanda för bevisning. I detta arbete drar jag slutsatsen att resolutionsmetoden förmodligen är mer lämpad än tablåmetoden för en automatisk teorembevisare, med avseende på hur svår den är att implementera. När det gäller prestanda indikerar utförda tester att resolutionsmetoden är det bästa valet.

L’ Answer Set Programming (ASP) est un formalisme capable de représenter des connaissances en Intelligence Artificielle à l’aide d’un programme logique au premier ordre pouvant contenir des négations par défaut. En quelques années, plusieurs solveurs performants ont été proposés pour calculer les solutions d’un programme ASP que l’on nomme answer sets.Nous nous intéressons ici plus particulièrement au solveur ASPeRiX qui instancie les règles au premier ordre à la volée durant le calcul des answer sets. Pour réaliser cela, ASPeRiX applique un chaînage avant sur les règles à partir de littéraux précédemment déterminés.L’étude de ce solveur nous amène notamment à considérer la notion de justification dans le cadre d’une approche de calcul d’ answer sets basée sur les règles. Les justifications permettent d’expliquer pourquoi certaines propriétés sont vérifiées. Parmi celles-ci, nous nous concentrons particulièrement sur les raisons d’échecs qui justifient pourquoi certaines branches de l’arbre de recherche n’aboutissent pas à un answer set.Cela nous conduit à implémenter une version d’ ASPeRiX proposant du backjumping qui évite de parcourir systématiquement toutes les branches de l’arbre de recherche grâce aux informations fournies par les raisons d’échecs. / Answer set programming (ASP) is a formalism able to represent knowledge in Artificial Intelligence thanks to a first order logic program which can contain default negations. In recent years, several efficient solvers have been proposed to compute the solutions of an ASP program called answer sets. We are particularly interested in the ASPeRiX solver that instantiates the first order rules on the fly during the computation of answer sets. It applies a forward chaining of rules from literals previously determined. The study of this solver leads us to consider the concept of justification as part of a rule-based approach for computing answer sets. Justifications enable to explain why some properties are true or false. Among them, we focus particularly on the failure reasons which justify why some branches of the search tree does not result in an answer set. This encourages us to implement a version of ASPeRiX with backjumping in order to jump to the last choice point related to the failure in the search tree thanks to information provided by the failure reasons.

We can classify several quite different calculi for automated reasoning in first-order logic as instantiation-based methods (IMs). Broadly speaking, unlike in traditional calculi such as resolution where the first-order satisfiability problem is tackled by deriving logical conclusions, IMs attempt to reduce the first-order satisfiability problem to propositional satisfiability by intelligently instantiating clauses. The Inst-Gen-Eq method is an instantiation-based calculus which is complete for first-order clause logic modulo equality. Its distinctive feature is that it combines first-order reasoning with efficient ground satisfiability checking, which is delegated in a modular way to any state-of-the-art ground solver for satisfiability modulo theories (SMT). The first-order reasoning modulo equality employs a superposition-style calculus which generates the instances needed by the ground solver to refine a model of a ground abstraction or to witness unsatisfiability. The thesis addresses the main issue in the Inst-Gen-Eq method, namely efficient extraction of instances, while providing powerful redundancy elimination techniques. To that end we introduce a novel labelled unit superposition calculus with sets, AND/OR trees and ordered binary decision diagrams (OBDDs) as labels. The different label structures permit redundancy elimination each to a different extent. We prove completeness of redundancy elimination from labels and further integrate simplification inferences based on term rewriting. All presented approaches, in particular the three labelled calculi are implemented in the iProver-Eq system and evaluated on standard benchmark problems.

Automated Theorem Provers (ATP) are software programs which carry out inferences over logico-mathematical systems, often with the goal of finding proofs to some given theorem. ATP systems are enormously powerful computer programs, capable of solving immensely difficult problems. Currently, many automated theorem provers exist like E, vampire, SPASS, ACL2, Coq etc. However, all the available theorem provers have some common problems: (1) Current ATP systems tend not to try to find proofs entirely on their own. They need help from human experts to supply lemmas, guide the proof, etc. (2) There is not a single proof system available which provides fully automated platforms for both First Order Logic (FOL) and other Higher Order Logic (HOL). (3) Finally, current proof systems do not have an easy way to quickly deploy and reason over new logical systems, which a logic researcher may want to test. In response to these problems, I introduce the MATR framework. MATR is a platform-independent, codelet-based (independently operating processes) proof system with an easy-to-use Graphical User Interface (GUI), where multiple codelets can be selected based on the formal system desired. MATR provides a platform for different proof strategies like deduction and backward reasoning, along with different formal systems such as non-classical logics. It enables users to design their own proof system by selecting from the list of codelets without needing to write an ATP from scratch.