[pt] Garantir que uma base de conhecimento com atos da administração pública contenha apenas fatos em conformidade com sua legislação torna-se um desafio para qualquer gestor público. Para isso, dado o grande volume de dados gerados por empresas públicas, faz-se necessário o emprego de recursos tecnológicos que auxiliem o processo de análise de conformidade destes atos. Este trabalho apresenta uma arquitetura computacional capaz de extrair informações publicados dos diários oficiais e então serializá-los em duas bases de conhecimento: triplas RDF/XML de fatos e triplas de RDF/XML de regras formalizadas em lógica iALC, uma lógica de descrição intuicionista. Para garantir a consistência desta base de conhecimento, foi desenvolvido um SAT Solver para iALC em forma de tableau semântico intuicionista. Uma extensão do tableau intuicionista de primeira ordem apresentado por Fitting (1969). Este SAT Solver faz parte de um módulo que além de gerar modelos e contra-exemplos para as regras formalizadas em iALC, também gera um código preliminar de consultas em SPARQL. Esta abordagem permite inferir e certificar a qualidade dos dados disponíveis na base de conhecimento RDF/XML de fatos. Para garantir a qualidade do nosso SAT Solver, fizemos a prova de soundness das suas regras. Para garantir a qualidade da nossa abordagem lógica, construímos um conjunto de 21 Questões de Competência e aplicamos à nossa ferramenta. Os resultados deste estudo de caso mostraram a eficácia e eficiência da nossa abordagem. / [en] Ensuring that a knowledge base with public administration acts contains only facts in accordance with its legislation becomes a challenge for any public manager. To achieve this, given the large volume of data generated by public companies, it is necessary to apply technological resources that assist in the process of analyzing the compliance of these acts. This work presents a computational architecture capable of extracting information published in official gazettes and then serializing it into two knowledge bases, RDF/XML triples of facts and RDF/XML triples of rules formalized in iALC logic, an intuitionistic description logic. To ensure the consistency of this knowledge base, a SAT Solver for iALC was developed in the form of an intuitionistic semantic tableau. An extension of the first-order intuitionist tableau presented by Fitting (1960). This SAT Solver is part of a module that generates models and counter-examples for rules formalized in iALC and generates a preliminary query code in SPARQL. This approach allows infer and certify the quality of the data available in the RDF/XML knowledge base of facts. To guarantee the quality of our SAT Solver, we carry out the soundness proof of its rules. To ensure the quality of our logical approach, we built a set of 21 Competency Questions and applied our tool. The results of this case study showed our approach s effectiveness and efficiency.

[pt] A lógica descritiva intuicionista iALC foi criada para modelar e raciocinar sobre o domínio de Leis baseada na Jurisprudência Kelseniana [1]. No decorrer da década anterior, essa lógica foi usada de diversas maneiras para modelar normas ou formalizar raciocínio jurídico [2, 3, 4, 5, 6, 7, 8, 9, 10]. Neste trabalho pretendemos complementar trabalhos anteriores ralizados com essa lógica ao preencher algumas lacunas encontradas enquanto trabalhando com ela. A primeira lacuna ocorre por iALC não ter um modo intuitivo de explicar raciocínio nela realizado para pessoas fora do domínio da Lógica. Ela tem um Cálculo de Sequentes (CS) [6] correto e completo (com respeito a modelos conceituais intuitionistas [3]) que tem sido menos usado que o desejado, e isso se dá em grande parte devido à maneira pouco intuitiva com que CS representa provas. Apresentamos um sistema de Dedução Natural (DN) correto e completo e com (quasi-)normalização para compensar por essa dificuldade em explicar CS para não-lógicos, especialmente os do domínio legal, essenciais para nossa pesquisa. Normalização completa não é possível devido a um tipo de derivação - tirando essa exceção, o resto do sistema gera derivações uniformes. A segunda lacuna envolve não poder lidar com raciocínio não-monotônico (RNM). Em geral, utiliza-se raciocínio monotônico, no qual, se é possível concluir algo de um conjunto de premissas, não há como acrescentar outra premissa de modo a evitar a conclusão prévia. Isso não é o caso em um julgamento legal, por exemplo, no qual lados opostos buscam convencer um juiz ou júri de consequências opostas ao adicionar premissas diferentes ao caso em questão. Propomos uma investigação de caráter exploratório em busca de uma extensão de iALC para lidar com RNM a fim de representar raciocínio jurídico em outras facetas da Lei como o processo judicial, que é não-monotônico por natureza. Apresentamos propriedades desejadas e uma possível aplicação de um sistema assim via um estudo de caso. Detalhamos mais a motivação tanto para o sistema de DN quanto a extensão de RNM, assim como as decisões tomadas ao criar cada um. / [en] The intuitionistic description logic iALC was created to model and reason over the domain of Law based on Kelsenian Jurisprudence [1]. Over the past decade, this logic has been used in several ways to either model norms or formalise legal reasoning [2, 3, 4, 5, 6, 7, 8, 9, 10]. In this work we intend to complement previous research done with this logic by filling some gaps found while working with it. The first gap occurs in iALC needing an intuitive way to explain reasoning for non-logicians. It has a sound and complete (concerning intuitionistic conceptual models [3]) Sequent Calculus (SC) [6] that has seen less usage than expected due to its non-intuitive way of presenting a proof. We present a (quasi-)normalising, sound and complete (w.r.t. TBox validity for intuitionistic conceptual models) Natural Deduction (ND) System to cover this difficulty in explaining SC to non-logicians, especially those in the domain of Law, which are essential to us. We do not achieve full normalisation due to a kind of derivation which cannot be normalised - aside from this exception, the rest of the system can provide uniform derivations. The second gap is being unable to deal with non-monotonic reasoning (NMR). Usually, one considers monotonic reasoning, in which, if one can conclude something from a set of premises, there is no way to add another premise to avoid said conclusion. This is not the case in a court of law, for instance, in which different parties aim to convince a judge or jury of opposite consequences by adding different premises to the case itself. We provide an exploratory investigation of an extension of iALC to deal with NMR to represent legal reasoning in aspects of the Law, such as the judicial process, which is non-monotonic by nature. We present desirable properties and a possible application of such a system via a case study. We explain further the motivation for both the ND system and the NMR extension and the decisions taken for both.

[pt] A lógica iALC é uma lógica de descrição de caráter intuicionista, criada para lidar com textos jurídicos como alternativa à mais comumente utilizada lógica deôntica, por conseguir contornar problemas que se encontra ao utilizar esta última. Nesta dissertação, introduzimos os principais conceitos que formam iALC, argumentamos sobre sua utilização em vez de demais lógicas para formalização de leis, implementamos suas provas de correção e completude no assistente de provas L(existe algum)(para cada)N, e apresentamos uma proposta de formalização de leis brasileiras em iALC. Além disso, mostramos um exemplo de aplicação desta formalização para resolução de questões de múltipla escolha da primeira fase do exame da OAB, que tem por objetivo avaliar a aptidão dos candidatos para a prática da advocacia no Brasil. São vistos três exemplos de questões, cujas características são discutidas e comparadas umas às outras. / [en] The logic iALC is a description logic with an intuitionistic aspect to it, created to deal with legal texts as an alternative to the more common deontic logic, by being able to avoid problems found when utilizing the latter. In this dissertation, we introduce the core concepts which form iALC, debate on its utilization instead of other logics for legal formalization, implement the soundness and completeness proofs for it in the proof assistant L(there is some)(for each)N, and present a proposal for formalization of Brazilian law in iALC. Furthermore, we show an example of application of this formalization in order to reason on multiple choice questions of the first part of the OAB Exam (the Brazilian national Bar exam), which aims to test candidates for their aptitude to practice the law in Brazil. We will show three examples, whose characteristics will be discussed and then compared to the others.