Dissertação

{en_GB=Algorithms for Markov Logic Networks} {} EVALUATED

{pt=Muitas aplicações do mundo real têm que lidar com incerteza. Assim, estas aplicações requerem métodos probabilísticos para representar informação do domínio de modo a descrever a sua probabilidade. As MLN associam fórmulas em lógica de primeira ordem a um valor real (peso) que representa a sua probabilidade. Esta tese investiga duas hipóteses. Em primeiro lugar, exploramos o uso de Satisfação Máxima incremental para resolver problemas de MLN. Métodos existentes que resolvem MLN dependem de várias chamadas independentes a uma ferramenta que resolve problemas de Satisfação parcial máxima com pesos (MaxSAT). O nosso objectivo principal é tirar proveito das recentes melhorias nas técnicas para resolver MaxSAT. Neste caso particular, queremos que as anteriores chamadas à ferramenta de MaxSAT sejam úteis para as chamadas seguintes. Em segundo lugar, exploramos a ideia de usar uma ferramenta que resolve problemas de Satisfação Módulo Teorias (SMT) para validar cada uma das regras. Algumas abordagens do estado da arte usam uma ferramenta de Datalog para validar as regras. Este método implica o uso de uma base de dados. Um dos nossos objectivos é evitar o uso de uma base de dados. No final, avaliamos a nossa abordagem com duas ferramentas do estado da arte (Tuffy e IPR). O nosso algoritmo, Inference using PROpagation and Validation (ImPROV) devolve soluções correctas e óptimas, que era o nosso principal objectivo., en=Many real world applications have to deal with uncertainty. Consequently, they demand probabilistic methods to represent some (if not all) of their events to describe their likelihood. MLN associates first-order logic formulas to a real value (weight) that represents their likelihood. This thesis explores two main hypothesis. First, we explore the use of incremental Maximum Satisfiability (MaxSAT) to solve MLN problems. Existing methods that solve MLN rely on various independent Weighted Partial Maximum Satisfiability (WPMS) solver calls. Our main goal is to benefit from recent improvements in (WPMS) solving techniques. In this particular case, we intend to make previous (WPMS) solver calls useful to the subsequent WPMS solver calls. Secondly, we explore the hypothesis of using an Satisfiability Modulo Theories (SMT) solver to validate the constraints. In other words, during the algorithm we need to guarantee that the current solution does not violate any rules that are not yet instantiated. Some state-of-the-art approaches use a Datalog solver to validate each constraint. This method implies the use of queries to a database. Our main goal is to avoid having a database altogether. Finally, we evaluate our approach with two state-of-the-art tools (Tuffy and IPR). Our algorithm, Inference using PROpagation and Validation (ImPROV) returns sound and optimal solutions, which is our first and most important goal. }
{pt=Redes logicas de Markov, Satisfação Módulo Teorias, Satisfação Máxima, en=Markov logic networks, Satisfiability Modulo Theories, Maximum Satisfiability}

Novembro 10, 2017, 13:0

Publicação

Obra sujeita a Direitos de Autor

Orientação

ORIENTADOR

Vasco Miguel Gomes Nunes Manquinho

Departamento de Engenharia Informática (DEI)

Professor Associado