Os sistemas Q1 e Q2, desenvolvidos por Andréa Lopari?, perfazem três principais modificações na semântica clássica: primeiramente, o universo do discurso pode não estar limitado aos objetos que pertencem ao domínio de uma dada estrutura; em segundo lugar, a relação de identidade é determinada como a diagonal desse domínio (assim, tal relação pode não ser aplicável a todas as coisas sobre as quais a linguagem possa falar); em terceiro lugar, o quantificador existencial, em Q1, bem como o universal, em Q2, podem alcançar valores que estejam fora do domínio da estrutura. Como consequência, embora definida classicamente, a negação apresenta alguns comportamentos não clássicos - a negação de um predicado numa fórmula atômica, por exemplo, pode caracterizar algo maior que, e não tão bem definido quanto, o complemento da extensão desse predicado relativamente ao domínio. [...]. / The systems Q1 and Q2, developed by Andréa Lopari?, make up three main changes in classical semantics: first, the universe of discourse can be not limited by the objects that belongs to the domain of a given structure; second, the relation of identity is fixed as a diagonal of this domain (so, it may be not applicable to all things about what the language can speak); third, the existential quantifier in Q1, as well as the universal in Q2, may capture values out of the domain of the structure. As a consequence, although classically defined, the negation presents some non-classical behavior - a negated predicate in an atomic formula, for instance, may characterize something larger and not as well defined as the complement of the extension of this predicate relatively to the domain. [...].

Submitted by Automa??o e Estat?stica (sst@bczm.ufrn.br) on 2017-12-12T17:57:13Z No. of bitstreams: 1 HanielMoreiraBarbosa_TESE.pdf: 2203436 bytes, checksum: 38477e5641001f5d9fdcb2ab0ac16855 (MD5) / Approved for entry into archive by Arlan Eloi Leite Silva (eloihistoriador@yahoo.com.br) on 2017-12-13T18:11:52Z (GMT) No. of bitstreams: 1 HanielMoreiraBarbosa_TESE.pdf: 2203436 bytes, checksum: 38477e5641001f5d9fdcb2ab0ac16855 (MD5) / Made available in DSpace on 2017-12-13T18:11:52Z (GMT). No. of bitstreams: 1 HanielMoreiraBarbosa_TESE.pdf: 2203436 bytes, checksum: 38477e5641001f5d9fdcb2ab0ac16855 (MD5) Previous issue date: 2017-09-05 / Em muitas aplica??es de m?todos formais, como verifica??o formal, s?ntese de programas, testes autom?ticos e an?lise de programas, ? comum depender de solucionadores de satisfatibilidade m?dulo teorias (SMT) como backends para resolver automaticamente condi??es que precisam ser verificadas e fornecer certificados de seus resultados. Nesta tese, objetivamos melhorar a efici?ncia dos solucionadores SMT e aumentar sua confiabilidade. Nossa primeira contribui??o ? fornecer um arcabou?o uniforme e eficiente para raciocinar com f?rmulas quantificadas em solucionadores SMT, em que, geralmente, v?rias t?cnicas de instancia??o s?o empregadas para lidar com quantificadores. Mostramos que as principais t?cnicas de instancia??o podem ser lan?adas neste arcabou?o unificador para lidar com f?rmulas quantificadas com igualdade e fun??es n?o interpretadas. O arcabou?o baseia-se no problema de E-ground (dis)unifica??o, uma varia??o do problema cl?ssico de E-unifica??o r?gida. Apresentamos um c?lculo correto e completo para resolver esse problema na pr?tica: Fechamento de Congru?ncia com Vari?veis Livres (CCFV). Uma avalia??o experimental ? apresentada, na qual medimos o impacto das otimiza??es e t?cnicas de instancia??o baseadas no CCFV nos solucionadores SMT veriT e CVC4. Mostramos que nossas implementa??es exibem melhorias em rela??o ?s abordagens de ?ltima gera??o em v?rias bibliotecas de refer?ncia, decorrentes de aplica??es do mundo real. Nossa segunda contribui??o ? uma estrutura para o processamento de f?rmulas ao mesmo tempo que produz demonstra??es detalhadas. Nosso objetivo ? aumentar a confiabilidade nos resultados de solucionadores SMT e sistemas de racioc?nio automatizado similares, fornecendo justificativas que podem ser verificadas com efici?ncia de forma independente e para melhorar sua usabilidade por aplicativos externos. Os assistentes de demonstra??o, por exemplo, geralmente requerem a reconstru??o da justifica??o fornecida pelo solucionador em uma determinada obriga??o de prova. Os principais componentes da nossa estrutura de produ??o de demonstra??es s?o um algoritmo gen?rico de recurs?o contextual e um conjunto extens?vel de regras de infer?ncia. Clausifica??o, Skolemiza??o, simplifica??es espec?ficas de teorias e expans?o das express?es "let" s?o exemplos dessa estrutura. Com estruturas de dados adequadas, a gera??o de demonstra??es cria apenas uma sobrecarga de tempo linear, e as demonstra??es podem ser verificadas em tempo linear. Tamb?m implementamos a abordagem em veriT. Isso nos permitiu simplificar drasticamente a base do c?digo, aumentando o n?mero de problemas para os quais demonstra??es detalhadas podem ser produzidas. / In many formal methods applications it is common to rely on SMT solvers to automatically discharge conditions that need to be checked and provide certificates of their results. In this thesis we aim both to improve their efficiency of and to increase their reliability. Our first contribution is a uniform framework for reasoning with quantified formulas in SMT solvers, in which generally various instantiation techniques are employed. We show that the major instantiation techniques can be all cast in this unifying framework. Its basis is the problem of E-ground (dis)unification, a variation of the classic rigid E-unification problem. We introduce a decision procedure to solve this problem in practice: Congruence Closure with Free Variables (CCFV). We measure the impact of optimizations and instantiation techniques based on CCFV in the SMT solvers veriT and CVC4, showing that our implementations exhibit improvements over state-of-the-art approaches in several benchmark libraries stemming from real world applications. Our second contribution is a framework for processing formulas while producing detailed proofs. The main components of our proof producing framework are a generic contextual recursion algorithm and an extensible set of inference rules. With suitable data structures, proof generation creates only a linear-time overhead, and proofs can be checked in linear time. We also implemented the approach in veriT. This allowed us to dramatically simplify the code base while increasing the number of problems for which detailed proofs can be produced.

Os sistemas Q1 e Q2, desenvolvidos por Andréa Lopari?, perfazem três principais modificações na semântica clássica: primeiramente, o universo do discurso pode não estar limitado aos objetos que pertencem ao domínio de uma dada estrutura; em segundo lugar, a relação de identidade é determinada como a diagonal desse domínio (assim, tal relação pode não ser aplicável a todas as coisas sobre as quais a linguagem possa falar); em terceiro lugar, o quantificador existencial, em Q1, bem como o universal, em Q2, podem alcançar valores que estejam fora do domínio da estrutura. Como consequência, embora definida classicamente, a negação apresenta alguns comportamentos não clássicos - a negação de um predicado numa fórmula atômica, por exemplo, pode caracterizar algo maior que, e não tão bem definido quanto, o complemento da extensão desse predicado relativamente ao domínio. [...]. / The systems Q1 and Q2, developed by Andréa Lopari?, make up three main changes in classical semantics: first, the universe of discourse can be not limited by the objects that belongs to the domain of a given structure; second, the relation of identity is fixed as a diagonal of this domain (so, it may be not applicable to all things about what the language can speak); third, the existential quantifier in Q1, as well as the universal in Q2, may capture values out of the domain of the structure. As a consequence, although classically defined, the negation presents some non-classical behavior - a negated predicate in an atomic formula, for instance, may characterize something larger and not as well defined as the complement of the extension of this predicate relatively to the domain. [...].

[pt] Existem diferentes estilos de cálculos dedutivos, usados para derivar os teoremas de uma lógica. Os mais habituais são os sistemas axiomáticos; mas, do ponto de vista da teoria da prova, os sistemas em dedução natural parecem ser mais interessantes. Essa é a motivação que leva ao desenvolvimento de técnicas que visam a facilitar a transformação de um cálculo dedutivo para o estilo em dedução natural. Esse trabalho se concentra no aspecto de modelar regras para os quantificadores da linguagem considerada e, para isso, faz uso de rótulos. Após uma apresentação intuitiva da técnica desenvolvida, passa-se à exposição de sistemas lógicos tratados pelo método: lógica de ultrafiltros, lógica de filtros, CTL, lógica de Keisler e CTL*. Em cada caso, analisam-se aspectos de teoria da prova. / [en] There are many kinds of deductive calculus. The axiomatic ones are the more usual. However, from the point of view of proof theory, Natural Deduction systems seem to be more interesting. This is the motivation for developping a technique that aims to ease the transformation from deductive calculus to Natural Deduction style. This work concentrates on the aspect of modeling the rules for the quantifiers of the logic considered, and for this purpose labels are used. After an intuitive presentation of the technique developped, some logical systems are treated by the method: ultrafilter logic, filter logic, CTL, Keisler`s logic and CTL*. For each one of them proof-theoretical aspects are analysed.