Título: Synthesis of First-Order Sentences using Ehrenfeucht–Fraïssé games

and Boolean Satisfiability

Data: 30/08/2019

Horário: 09:00h

Local: Sala de Seminários - Bloco 952

Resumo:

In this work, we investigate the problem of extracting knowledge from samples of classified relational structures in terms of first-order sentences. In other words, we investigate the following problem: for a fixed class of relational structures, given a sample of classified structures, find a first-order sentence of minimal quantifier rank that is consistent with the sample. We consider the following classes of structures: monadic structures, equivalence structures, disjoint unions of linear orders, and strings represented by finite structures with a successor relation.

We use results of the Ehrenfeucht–Fraïssé game on these classes of structures in order to design an algorithm to find such a sentence. For these classes of structures, the problem of determining whether the Duplicator has a winning strategy in an Ehrenfeucht–Fraïssé game is solved in polynomial time. We also introduce the distinguishability sentences which are sentences that distinguish between two given structures. We define the distinguishability sentences based on necessary and sufficient conditions for a winning strategy in Ehrenfeucht–Fraïssé games. Our algorithm returns a Boolean combination of such sentences. We also show that any first-order sentence is equivalent to a Boolean combination of distinguishability sentences. Finally, we also show that our algorithm’s running time is polynomial in the size of the input.

Since general first-order sentences are hard to read, we define a quantifier-free normal form (QNF) over the classes of structures we are considering. QNF sentences are defined over a richer vocabulary such that atomic formulas are an abbreviation of general first-order sentences over a standard vocabulary. Then, QNF sentences consistof Boolean combinations of such atomic sentences over this non-standard vocabulary. Moreover, we define a DNF version for QNF sentences. Then, given a sample of strings and the number of disjunctive clauses, we investigate the problem of finding a DNF formula that is consistent with the sample. We show that this problem is NP-complete and we solve it by a translation into Boolean satisfiability. We also present an extension of this problem that is robust concerning noisy samples. We solve this generalized version by a codification into the maximum satisfiability problem.

Banca:

• Prof. Drª. Ana Teresa de Castro Martins (MDCC/UFC - Orientador)
• Prof. Dr. Francicleber Martins Ferreira (MDCC/UFC - Coorientador)
• Prof. Dr. João Fernando Lima Alcântara (MDCC/UFC)
• Prof. Dr. Edward Hermann Haeusler (PUC - Rio)
• Prof. Dr. Ruy José Guerra Barretto de Queiroz(UFPE)