• JoomlaWorks Simple Image Rotator
  • JoomlaWorks Simple Image Rotator
  • JoomlaWorks Simple Image Rotator
  • JoomlaWorks Simple Image Rotator
  • JoomlaWorks Simple Image Rotator
  • JoomlaWorks Simple Image Rotator
  • JoomlaWorks Simple Image Rotator
  • JoomlaWorks Simple Image Rotator
  • JoomlaWorks Simple Image Rotator
  • JoomlaWorks Simple Image Rotator
 
  Bookmark and Share
 
 
Thèse de Doctorat
DOI
https://doi.org/10.11606/T.45.2021.tde-17062021-163257
Document
Auteur
Nom complet
Sandro Márcio da Silva Preto
Adresse Mail
Unité de l'USP
Domain de Connaissance
Date de Soutenance
Editeur
São Paulo, 2021
Directeur
Jury
Finger, Marcelo (Président)
Almeida, João Marcos de
Coniglio, Marcelo Esteban
Cozman, Fabio Gagliardi
Fermé, Eduardo Leopoldo
Titre en anglais
Semantics modulo satisfiability with applications: function representation, probabilities and game theory
Mots-clés en anglais
Coherence of constraints
Formal methods
Function representation
Lukasiewicz infinitely-valued logic
Nash equilibrium
Neural networks
Non-classical probabilities
Piecewise linear functions
Probabilistic constraints
Probabilistic satisfiability
Propositional logics
Rational McNaughton functions
Uncertain games
Valuation semantics
Resumé en anglais
In the context of propositional logics, we apply semantics modulo satisfiability - a restricted semantics which comprehends only valuations that satisfy some specific set of formulas - with the aim to efficiently solve some computational tasks. Three possible such applications are developed. We begin by studying the possibility of implicitly representing rational McNaughton functions in Lukasiewicz Infinitely-valued Logic through semantics modulo satisfiability. We theoretically investigate some approaches to such representation concept, called representation modulo satisfiability, and describe a polynomial algorithm that builds representations in the newly introduced system. An implementation of the algorithm, test results and ways to randomly generate rational McNaughton functions for testing are presented. Moreover, we propose an application of such representations to the formal verification of properties of neural networks by means of the reasoning framework of Lukasiewicz Infinitely-valued Logic. Then, we move to the investigation of the satisfiability of joint probabilistic assignments to formulas of Lukasiewicz Infinitely-valued Logic, which is known to be an NP-complete problem. We provide an exact decision algorithm derived from the combination of linear algebraic methods with semantics modulo satisfiability. Also, we provide an implementation for such algorithm for which the phenomenon of phase transition is empirically detected. Lastly, we study the game theory situation of observable games, which are games that are known to reach a Nash equilibrium, however, an external observer does not know what is the exact profile of actions that occur in a specific instance; thus, such observer assigns subjective probabilities to players actions. We study the decision problem of determining if a set of these probabilistic constraints is coherent by reducing it to the problems of satisfiability of probabilistic assignments to logical formulas both in Classical Propositional Logic and Lukasiewicz Infinitely-valued Logic depending on whether only pure equilibria or also mixed equilibria are allowed. Such reductions rely upon the properties of semantics modulo satisfiability. We provide complexity and algorithmic discussion for the coherence problem and, also, for the problem of computing maximal and minimal probabilistic constraints on actions that preserves coherence.
Titre en portugais
Semântica módulo satisfatibilidade com aplicações: representação de funções, probabilidades e teoria dos jogos
Mots-clés en portugais
Coerência de restrições
Equilíbrio de Nash
Funções lineares por partes
Funções racionais de McNaughton
Jogos com incerteza
Lógica infinito-valorada de Lukasiewicz
Lógicas proposicionais
Métodos formais
Probabilidades não clássicas
Redes neurais
Representação de funções
Restrições probabilísticas
Satisfatibilidade probabilística
Semânticas de valoração
Resumé en portugais
No contexto das lógicas proposicionais, aplicamos semânticas módulo satisfatibilidade - uma semântica restrita que contempla somente valorações que satisfazem algum conjunto específico de fórmulas - com o objetivo de resolver de forma eficiente algumas tarefas computacionais. Três destas possíveis aplicações são desenvolvidas. Começamos estudando a possibilidade de representar implicitamente funções racionais de McNaughton na Lógica Infinito-valorada de Lukasiewicz por meio de semânticas módulo satisfatibilidade. Investigamos teoricamente algumas abordagens para este conceito de representação, chamado representação módulo satisfatibilidade, e descrevemos um algoritmo polinomial que constrói representações no sistema recém-introduzido. Uma implementação do algoritmo, resultados de testes e formas de gerar aleatoriamente funções racionais de McNaughton para os testes são apresentados. Mais que isso, propomos uma aplicação destas representações à verificação formal de propriedades de redes neurais através do ferramental de inferência da Lógica Infinito-valorada de Lukasiewicz. Então, passamos a investigar a satisfatibilidade da atribuição conjunta de probabilidades a fórmulas da Lógica Infinito-valorada de Lukasiewicz, um problema sabidamente NP-completo. Fornecemos um algoritmo exato de decisão derivado da combinação de métodos de álgebra linear com semânticas módulo satisfatibilidade. Fornecemos também uma implementação para tal algoritmo para o qual o fenômeno da transição de fase é empiricamente detectado. Por último, estudamos a situação em teoria dos jogos dos chamados jogos observáveis, que são jogos que sabidamente alcançam um equilíbrio de Nash, entretanto, um observador externo não conhece qual o exato perfil de ações que ocorre em uma instância específica; então, tal observador atribui probabilidades subjetivas às ações do jogadores. Estudamos o problema de decisão de determinar se um conjunto dessas restrições probabilísticas é coerente reduzindo-o aos problemas de satisfatibilidade de atribuições probabilísticas a fórmulas lógicas tanto na Lógica Proposicional Clássica quanto na Lógica Infinito-valorada de Lukasiewicz dependendo se somente equilíbrios puros são permitidos ou, também, equilíbrios mistos. Tais reduções dependem das propriedades das semânticas módulo satisfatibilidade. Oferecemos discussões sobre complexidade e algoritmos para o problema de coerência e, também, para o problema de computar restrições probabilísticas maximal e minimal sobre ações que preservem a coerência.
 
AVERTISSEMENT - Regarde ce document est soumise à votre acceptation des conditions d'utilisation suivantes:
Ce document est uniquement à des fins privées pour la recherche et l'enseignement. Reproduction à des fins commerciales est interdite. Cette droits couvrent l'ensemble des données sur ce document ainsi que son contenu. Toute utilisation ou de copie de ce document, en totalité ou en partie, doit inclure le nom de l'auteur.
thesis_spreto.pdf (1.56 Mbytes)
Date de Publication
2021-09-03
 
AVERTISSEMENT: Apprenez ce que sont des œvres dérivées cliquant ici.
Tous droits de la thèse/dissertation appartiennent aux auteurs
CeTI-SC/STI
Bibliothèque Numérique de Thèses et Mémoires de l'USP. Copyright © 2001-2024. Tous droits réservés.