21 |
[en] EXTRACTION OF COMPUTATIONAL CONTENTS FROM INTUITIONIST PROOFS / [pt] EXTRAÇÃO DE CONTEÚDO COMPUTACIONAL DE PROVAS INTUICIONISTASGEIZA MARIA HAMAZAKI DA SILVA 10 September 2004 (has links)
[pt] Garantir que programas são implementados de forma a
cumprir uma especificação é uma questão fundamental em
computação, por isso, têm sido propostos vários métodos
que almejam provar a correção dos programas. Este
trabalho apresenta um método, baseado no isomorfismo de
Curry-Howard, que extrai conteúdos computacionais de
provas intuicionistas, conhecido como síntese construtiva
ou proofs-as-programs. É proposto um processo de síntese
construtiva de programas, onde a extração do conteúdo
computacional gera um programa em linguagem imperativa a
partir de uma prova em lógica intuicionista poli-sortida,
cujos axiomas definem os tipos abstratos de dados, sendo
utilizado como sistema dedutivo a Dedução Natural. Também
é apresentada uma prova de correção, bem como uma prova
de completude do método atráves do uso de um sistema com
regra ômega (computacional) para a aritmética de Heyting,
concluindo com uma demonstração da relação entre o uso da
indução finita no lugar da regra ômega computacional no
processo de síntese. / [en] One of the main problems in computer science is to assure
that programs are implemented in such a way that they
satisfy a given specification. There are many studies about
methods to prove correctness of programs. This work
presents a method, belonging to the constructive synthesis
or proofs-as-programs paradigm, that comes from the Curry-
Howard isomorphism and extracts the computational contents
of intuitionist proofs. The synthesis process proposed
produces a program in an imperative language from a proof
in many-sorted intuitionist logic, where the axioms define
the abstract data types using Natural Deduction as
deductive system. It is proved the correctness, as well as
the completeness of the method regarding the Heyting
arithmetic with ômega-rule(in its computational version). A
discussion about the use of the finitary induction instead
of computational ômega-rule concludes the work.
|
22 |
[en] MARKETING SOCIAL PROGRAMS ON THE BUSINESS SECTOR: MULTI-CASE ANALYSES ON CO-CREATION VALUE / [pt] PROGRAMAS DE MARKETING SOCIAL NO ÂMBITO EMPRESARIAL: ANÁLISE MULTICASOS À LUZ DA COCRIAÇÃO DE VALORANDRÉIA APARECIDA ALBINO 21 September 2016 (has links)
[pt] Considerando o aumento da participação da iniciativa privada em projetos e
programas que buscam contribuir para a elevação do bem estar da sociedade,
inclusive por meio de ações de marketing social, esta pesquisa teve como
principal objetivo identificar, na perspectiva dos atores envolvidos, em especial o
público-alvo, como a cocriação de valor é abordada (e se manifesta) nos
programas de marketing social desenvolvidos por empresas no Brasil. Para tal, foi
realizado um estudo multicasos que teve como objetos de estudo três iniciativas
promovidas por uma empresa privada do segmento de bens de consumo, em
parceria com outras organizações. Todas as iniciativas estudadas apresentam
aspectos que as caracterizavam como ações de marketing social e abrangiam
diferentes causas de interesse da sociedade: segregação de resíduos sólidos,
cuidados com a saúde cardiovascular e hábitos de higiene junto ao público
infantil, especialmente por meio da lavagem adequada das mãos. Os métodos para
coleta de dados envolveram quarenta entrevistas pessoais, por telefone e por email,
observação e consulta a arquivos e documentos diversos fornecidos por
alguns dos entrevistados. A análise dos dados foi qualitativa, seguindo categorias
pré-definidas a partir da revisão de literatura. Os resultados da pesquisa
mostraram que as iniciativas estudadas foram desenvolvidas tendo por base
diversos elementos da cocriação de valor, destacando-se, principalmente, o
projeto voltado aos cuidados com a higiene das mãos. Especificamente em relação
aos processos de descoberta, design e entrega de valor, as iniciativas estudadas,
apesar de apresentarem elementos da cocriação de valor, o fazem
predominantemente na etapa da entrega, sendo que os processos de descoberta
de design parecem ter ocorrido apenas sob a responsabilidade das organizações
envolvidas, sem evidências que sugerem a participação do público-alvo.
Identificou-se que a abordagem mais evidente nas iniciativas estudadas é a
downstream, mais voltada à mudança do comportamento individual. O presente
trabalho colabora para preencher uma lacuna na literatura referente a marketing
social e cocriação de valor, em especial no que tange ao estudo de ações
desenvolvidas pela iniciativa privada. Além disso, os resultados da pesquisa, ao
relatarem determinadas condições em que as iniciativas estudadas operam,
também indicaram aspectos em que estas podem ter seus resultados
potencializados, a partir da incorporação de mais princípios da cocriação de valor. / [en] Considering the increasingly interest of the business sector in projects and
programs which seek to contribute to society s well-being, including actions of
social marketing, this research s main objective was to identify, from the
concerned parties perspective, specially the target audience, how the co-creation
is approached (and manifested) in marketing social programs developed by
enterprises in Brazil. Therefore, a multi-case study was developed, which had, as
its objects of study, three initiatives from a private Brazilian company that
operates in the convenience goods sector, in partnership with other organizations.
All of the studied initiative show aspects that characterized them as social
marketing actions and embraced a few different aspects of interest from society,
among which were: segregation of solid residues, cardiovascular care and
children s hygiene habits, especially through adequate hand washing. Methods for
data collection include forty face to face, phone and e-mail interviews as well as
observation procedures and research of many files and documents provided by a
few of the respondents. The data analyses was qualitative, following preestablished
trends, taking the literature review as a starting point. The results from
the research pointed out that the studied initiatives were developed based on
several elements of co-creation of value, specially the project aimed at adequate
hand hygiene. Regarding the discovery, design and delivery of value processes
specifically, it is noticeable that in the initiatives studied, value co-creation
elements are predominantly in the delivery step, and the design discovery
processes seem to have occurred only under the responsibility of the organizations
involved, with no evidence to suggest the participation of the audience. It was
identified that the most obvious approach of the studied initiatives is the
downstream, more focused on individual behavior change. This work contributes
to fill a gap in respect of social marketing literature and co-creation of value,
especially in relation to the study of actions developed by the private sector. In
addition, the research s results, when reporting certain conditions under which the
studied initiatives operate, also indicated room for improvement in their results if
more principles of co-creation of value were to be implemented.
|
23 |
[pt] QUANTIFICAÇÃO IRRESTRITA E GENERALIDADE ABSOLUTA: A QUESTÃO DA POSSIBILIDADE DE UMA TEORIA SOBRE TUDO TESE / [en] UNRESTRICTED QUANTIFICATION AND ABSOLUTE GENERALITY: THE ISSUE OF THE POSSIBILITY OF A THEORY ABOUT EVERYTHINGANDRE NASCIMENTO PONTES 06 October 2015 (has links)
[pt] A presente tese tem como objetivo desenvolver uma discussão acerca das condições de possibilidade da quantificação irrestrita e existência da generalidade absoluta. O trabalho é dividido em quatro etapas. No primeiro capítulo, realizo, no âmbito da teoria dos modelos e teoria dos conjuntos, uma revisão do que chamo de semântica padrão dos quantificadores. A ideia básica é mostrar como, em tal semântica, quantificações estão associadas a domínios entendidos como conjuntos. Ao longo da tese, ficará patente que a semântica padrão impõe obstáculos intransponíveis ao tratamento formal de quantificações irrestritas. No segundo capítulo, apresento uma seleção do que considero os argumentos mais relevantes contra quantificações irrestritas e nossa capacidade de lidar formalmente com o que chamamos de generalidade absoluta. Alguns desses argumentos estão baseados em resultados tais como os paradoxos que Russell e Cantor derivaram na teoria dos conjuntos. No terceiro capítulo, apresento, de modo análogo, uma lista de argumentos agrupados em linhas de estratégias para reabilitar a quantificação irrestrita contra seus críticos. Além disso, desenvolvo uma discussão sobre os aspectos metafísicos do debate sobre o discurso a respeito da generalidade absoluta e sua correlação com argumentos por regresso ao infinito. Por fim, no quarto e último capítulo, desenvolvo um esboço geral de uma proposta alternativa de tratamento da quantificação irrestrita que apele para uma teoria paraconsistente dos conjuntos. Nela, as contradições obtidas na semântica padrão podem ser admitidas controladamente possibilitando assim a obtenção de domínios absolutos para quantificações. Essa proposta envolve a defesa de um sistema formal que seja inconsistente, porém dedutivamente não trivial. Em linhas
gerais, o presente trabalho está pautado no seguinte conjunto de teses: (i) existe uma estreita correlação entre os obstáculos impostos pela semântica padrão às quantificações irrestritas e a estrutura de argumentos por regresso ao infinito; (ii) a existência de uma generalidade absoluta é um fenômeno que se impõe às nossas mais intuitivas concepções de realidade e, portanto, não devemos descredenciar o discurso sobre tal generalidade em virtude de limitações de nossas linguagens formais; (iii) nós devemos escolher entre assumir a lógica clássica e abdicar do discurso sobre a generalidade absoluta ou manter nossa intuição mais básica descrita em (ii) e abrir espaço para um tratamento não clássico da questão; finalmente, (iv) minha sugestão no presente trabalho é que temos boas razões para nos aventurar nas paisagens descritas pelos sistemas não clássicos. / [en] In this doctoral dissertation, I tackle the issues of the conditions for the possibility of unrestricted quantification and of absolute generality. The text is framed as follows. The first chapter is devoted to reviewing what I call the standard semantics of quantifiers, within the realm of both model and set theories. In such semantics, the idea is, quantificational domains are conceived as sets. It will become clear along the way that, given this construal of quantificational domains, a formal treatment of unrestricted quantification faces insurmountable obstacles. The second chapter focuses on what I take to be the most relevant arguments against unrestricted quantification as well as against our ability to formally deal with so-called absolute generality. Some of them are based on results obtained by Russell and Cantor within set theory – the notorious Russell s paradox and Cantor s theorem. Analogously, in chapter three I review a number of grouped-into-strategic-lines arguments put forward to save unrestricted quantification against its critics. I also elaborate on the metaphysical aspects of the debate and its connections with infinite regress arguments. Lastly, in the fourth chapter I outline an alternative proposal based on paraconsistent set theory to deal with unrestricted quantification. On this approach, the contradictions found in standard semantics are admitted, yet in a controlled way, thus turning absolute quantificational domains available. The proposal is, basically, to allow the existence of inconsistent, yet deductively not trivial formal systems. The present work is broadly guided by the following set of claims: (i) there is a strong correlation between the obstacles set by standard semantics to unrestricted quantification and the structure of infinite regress arguments; (ii) absolute
generality is a phenomenon that imposes itself upon our most intuitive conceptions of reality; accordingly, the limitations suffered by our formal languages ought not to lead us to bring such generality into disrepute; (iii) one must choose between adopting classical logic and renouncing to appeal to absolute generality or sticking to our most basic intuitions as described in (ii) and make room for a non-classical treatment of the issue; (iv) we have, after all, good reasons to venture into the landscapes described by the non-classical systems.
|
24 |
[en] KNOWLEDGE BASED FOR HYDROELECTRIC MACHINES DIAGNOSIS / [pt] SISTEMA DE CONHECIMENTO PARA DIAGNÓSTICO DE MÁQUINAS HIDROGERADORASLUCIANO R CHAGAS COSTA JUNIOR 18 September 2006 (has links)
[pt] O Sistema elétrico brasileiro é baseado quase que
integralmente em energia produzida por Usinas
Hidroelétricas. Estas Máquinas Hidroelétricas possuem um
comportamento diferenciado das máquinas turbo geradoras,
cujo comportamento já foi identificado e classificado em
pesquisas anteriores. Este trabalho investiga o uso de um
Sistema baseado em Conhecimento para o diagnóstico precoce
de falhas em Máquinas Hidrogeradoras, visando redução de
custos advindos principalmente de paradas operacionais não
necessárias na máquina para manutenção. O sistema foi
criado com informação obtida a partir dos seguintes meios:
sistemática de manutenção executada nas Usinas
Hidroelétricas, através de entrevistas à equipe
responsável pela manutenção da usina de Furnas (MG); da
identificação do comportamento eletromecânico da máquina;
e do estudo de casos. O Sistema é capaz de identificar, a
partir dos sensores localizados nas máquinas, eventuais
falhas, permitindo executar paradas programadas de maneira
otimizada. Foi criado um protótipo de um sistema
computacional baseado em Conhecimento implementando tal
modelo de forma bem flexível. A modelagem criada, a
implementação do protótipo computacional e,
principalmente, a explicação do raciocínio empregado,
agregado com a possibilidade da modificação do
conhecimento através da aquisição automática, são
contribuições inovadoras deste trabalho. É descrito o
Domínio do Problema de diagnosticar falhas em Máquinas
Hidrogeradoras, identificado durante análise das
informações coletadas da equipe de manutenção na usina de
Furnas e de especialistas no comportamento eletromecânico
das máquinas.
É descrito também o modelo simbólico criado,
representativo do domínio, utilizando interface projetada,
visando a implementação prática nas usinas. É apresentado
uma solução de desacoplamento das informações advindas dos
sensores eletromecânicos da máquina e o sistema, através
de módulo baseado em Lógica Nebulosa (Fuzzy Logic) que
converte as informações numéricas em informações
simbólicas compreendidas pelo sistema de diagnóstico,
permitindo o uso do sistema, sem alteração em máquinas que
possuam características diversas. Finalmente, é
apresentada a metodologia de testes adotada para validação
do modelo implementado através da simulação de dados de
vibração e oscilação, cujo relacionamento com eventuais
falhas é parcialmente conhecido, assim como uma conclusão
sobre a viabilidade e praticidade de um modelo simbólico
na solução do diagnóstico das máquinas hidrogeradoras.
Durante o desenvolvimento da tese verificou-se que o
conhecimento sobre falhas em Máquinas Hidrogeradoras ainda
não está consolidado e que então, um Sistema baseado em
Conhecimento com aquisição de conhecimento automático
mostra-se uma excelente ferramenta de modelagem para os
especialistas. / [en] The Brazilian Electrical Energy supply is almost entirely
based on the energy produced by the Hydroeletric Power
Station Machines. These Hydroeletric Machines own
particular behavior in comparison to the turbogenerator
behavior. This work investigates the use of Knowledge
based system Hydroeletric Machines fault diagnosis. The
system was modeled using information obtained by: the
maintenance s systematic executed Hydroeletric Power
Stations, though Furnas (Minas Gerais) maintenance team
interviews; the Machine electromechanical behavior; and a
Case Based study. The system is able to identify, from
machine located sensors data analysis, eventual faults,
allowing the execution of programmed operational
interrupts in the machine in a optimized manner. A
computational prototype and, mainly, the interface explain
engine in addition to the knowledge modification through
acquisition, are the innovative contributions of this work.
The machine fault diagnosis problem domain is described,
identified in the information, collected from the
maintenance team and the electromechanical behavior
experts, analysis. It is also described the projected
symbolic model, the domain representation, using graphical
and friendly interface, aiming its practical
implementation in real Power Stations. It is shown a
sensor information detach solution, through a Fuzzy Logic
based module which converts the numerical data in a
symbolic one, known by the diagnosis system, allowing its
use, without any modification, in a sort of different
machines. Finally, it is shown the test methodology
adopted for the prototype validation through oscillation
data simulation, which relationship with machine faults is
partially known, and the symbolic model praticality and
feasibility in the Hidrogenerator Diagnosis solution.
Through the thesis development, it was verified that the
Hydrogenerator fault knowledge wasn t still consolidated.
So, the Knowledge Based system with knowledge acquisition
became an excelent modeling tool for the domain experts.
|
25 |
[en] AN EXPERIMENTAL APPROACH ON MINIMAL IMPLICATIONAL NATURAL DEDUCTION PROOFS COMPRESSION / [pt] UMA ABORDAGEM EXPERIMENTAL SOBRE A COMPRESSÃO DE PROVAS EM DEDUÇÃO NATURAL MINIMAL IMPLICACIONALJOSE FLAVIO CAVALCANTE BARROS JUNIOR 26 March 2020 (has links)
[pt] O tamanho das provas formais possui algumas importantes implicações
teóricas na área da complexidade computacional. O problema de determinar
se uma fórmula é uma tautologia da Lógica Proposicional Intuicionista e do
fragmento puramente implicacional da Lógica Minimal (M(contém)) é PSPACE-
Completo. Qualquer lógica proposicional com um sistema de dedução
natural que satisfaça o princípio da subfórmula possui o problema de
determinar tautologias em PSPACE. Saber se qualquer tautologia em M(contém)
admite provas de tamanho polinomialmente limitado está relacionado com
saber se NP = PSPACE. Técnicas de compressão de provas reportadas
na literatura utilizam duas abordagens principais para comprimir provas:
gerar provas já compactadas; comprimir uma prova já gerada. Proposta
por Gordeev e Haeusler (6), a Compressão Horizontal é uma técnica
de compressão de provas em dedução natural da M(contém) que utiliza grafos
direcionados para representar as provas. Dada a prova de uma tautologia
qualquer da M(contém), que pode possuir tamanho exponencial em relação ao
tamanho da conclusão, o objetivo da Compressão Horizontal é que a prova
resultante da compressão possua tamanho polinomialmente limitado em
relação ao tamanho da conclusão. Nosso trabalho apresenta a primeira
implementação da Compressão Horizontal, juntamente com os primeiros
resultados da aplicação da técnica sobre provas de tautologias da M(contém), além
disso, compara as taxas de compressão obtidas com técnicas tradicionais de
compressão de dados. / [en] The size of formal proofs has some important theoretical implications
in computational complexity theory. The problem of determining if some
formula of Intuitionistic Propositional Logic and the purely implicational
fragment of Minimal Logic (M(contains)) is a tautology is PSPACE-Complete. Any
propositional logic with a natural deduction system that satisfies the sub-
formula principle is PSPACE. To know if any tautology in M(contains) admits
polynomially sized proof is related to whether NP = PSPACE. Proof
compression techniques reported in literature use two main approaches
to proof compressing: generating already compressed proofs; compressing
an already generated proof. Proposed by Gordeev and Haeusler (6), the
Horizontal Compression is a natural deduction proof compression technique
that uses directed graphs to represent proofs. Given a tautology proof in
M(contains), which may have an exponential size in relation to conclusion length,
the goal of Horizontal Compression is that the compressed proof has a
polynomially limited size in relation to conclusion length. Our work presents
the first implementation of Horizontal Compression, together with the first
results of the execution of the technique on proofs of M(contains) tautologies.
|
26 |
[en] FIRST-ORDER MODAL LOGIC FOR REASONING ABOUT GAMES / [pt] LÓGICA MODAL DE PRIMEIRA-ORDEM PARA RACIOCINAR SOBRE JOGOSDAVI ROMERO DE VASCONCELOS 25 June 2007 (has links)
[pt] O termo jogo tem sido utilizado como uma metáfora, em
várias áreas
do conhecimento, para modelar e analisar situações onde
agentes(jogadores)
interagem em ambientes compartilhados para a realização de
seus objetivos sejam eles individuais ou coletivos.
Existem diversos modelos propostos
para jogos por diferentes áreas do conhecimento, tais como
matemática,
ciência da computação, ciência política e social, entre
outras. Dentre as
diversas formas de modelar jogos examinamos a Teoria dos
Jogos e as
lógicas para jogos. Neste trabalho
apresentamos uma lógica modal de
primeira-ordem baseada na lógica CTL, chamada de Game
Analysis nalysis Logic,
para raciocinar sobre jogos. Relacionamos os principais
modelos da Teoria dos Jogos (jogo estratégico,
extensivo, e de coalizão) e seus principais
conceitos de soluções(equilíbrio de Nash, equilíbrio de
subjogo perfeito,e core) aos modelos de GAL e às
fórmulas de GAL, respectivamente.
Além disso, estudamos as alternativas de quantificação De
Re e De Dicto
no contexto dos jogos extensivos, caracterizando o
conceito de equilíbrio
de Nash e equilíbrio de subjogo perfeito de acordo com as
alternativas
de quantificação. Relacionamos as lógicas Alternating-time
lternating-Tempomporal Logic (A ATL) TL) e Coalitional
Game Logic (CGL) com a lógica GAL, demonstrando
que ambas as lógicas são fragmentos da lógica GAL. Outro
resultado
deste trabalho é caracterizar uma classe de sistemas multi-
agentes,que é
baseada na arquitetura de agentes Belief-Desir Desire-
Intention(BDI), para a
qual existem jogos extensivos e vice-v versa. Como
conseqüência, os critérios
de racionalidade da Teoria dos Jogos podem ser aplicados
diretamente para
agentes BDI e vice-versa. Assim, a abordagem deste
trabalho pode ser
utilizada para analisar sistemas multi-agentes. Do ponto
de vista prático,
apresentamos um verificador de modelos para a lógica GAL.
Diversos estudos de casos são realizados utilizando o
verificador de modelos. / [en] Games are abstract models of decision-making in which
decision-makers(players)interact in a shared environment
to accomplish their
goals. Several models have been proposed to analyze a wide
variety of
applications in many disciplines such as mathematics,
computer science
and even political and social sciences among others. In
this
work, we focus
on Game Theory and Game Logics. We present a first-order
modal logic
based on CTL, namely Game Analysis Logic (GAL), to
model
and reason
about out games. The standard models of Game Theory
(strategic games,
extensiv games and coalition games) as well as their
solution concepts
(Nash equilibrium, subgame perfect equilibrium and co
re),respectively, are
express as models dels of GAL and formulas of GAL.
Moreover, we study the
alternatives of De Re and De Dicto quantification in the
context of extensive
games. We also show that two of the most representative
game logics,
namely Alternating-time lternating-Temp empor oral Logic
(A ATL) TL) and Coalitional Game Logic
(CGL), are fragments of GAL. We also characterize
haracterize a class of multi-agent
systems, which is based on the architecture Belief-Desire-
Intention (BDI),
for which there is a somehow equivalent class of games and
vice-versa. As
a consequence, criteria of rationality for agents can be
directly applied to
players and vice-versa. Game analysis formal tools can be
applied to MAS as
well. From a practical poin of view, we provide and
develop a model-checker for GAL. In addition, we perform
case studies using our prototype.
|
27 |
[pt] SISTEMAS DE PROVA E GERAÇÃO DE CONTRA EXEMPLO PARA LÓGICA PROPOSICIONAL MINIMAL IMPLICACIONAL / [en] SYSTEMS FOR PROVABILITY AND COUNTERMODEL GENERATION IN PROPOSITIONAL MINIMAL IMPLICATIONAL LOGIC23 November 2021 (has links)
[pt] Esta tese apresenta um novo cálculo de sequente, correto e completo para a Lógica Proposicional Minimal Implicacional (M →). LMT → destina-se a ser usado para a busca de provas em M →, em uma abordagem bottom-up. A Terminação do cálculo é garantida por uma estratégia de aplicação de regras que força uma maneira ordenada no procedimento de busca de provas de tal forma que todas as combinações possíveis são exploradas. Para uma fórmula inicial α, as provas em LMT→ têm um limite superior de |α|.2 |α|+1+2·log2|α|, que juntamente com a estratégia do sistema, garantem a decidibilidade do mesmo. As regras do sistema são concebidas para lidar com a necessidade de repetição de hipóteses e a natureza de perda de contexto da regra → esquerda , evitando a ocorrência de loops e o uso de backtracking. Portanto,
a busca de prova em LMT → é determinística, sempre executando buscas no sentido forward. LMT → tem a propriedade de permitir a extração de contramodelos a partir de buscas de prova que falharam (bicompletude), isto é, a árvore de tentativa de prova de um ramo totalmente expandido produz um
modelo de Kripke que falsifica a fórmula inicial. A geração de contra-modelo (usando a semântica Kripke) é obtida como consequência da completude do sistema. LMT→ é implementado como um provador de teoremas interativo baseado no cálculo proposto aqui. Comparamos nosso cálculo com outros
sistemas dedutivos conhecidos para M →, especialmente com Tableaux no estilo Fitting, um método que também tem a propriedade de ser bicompleto. Também propomos aqui uma tradução de LMT → para o verificador de prova Dedukti como uma forma de avaliar a correção da implementação que desenvolvemos,
no que diz respeito à especificação do sistema, além de torná-lo mais fácil de comparar com outros sistemas existentes. / [en] This thesis presents a new sequent calculus called LMT→ that has the properties to be terminating, sound and complete for Propositional Implicational Minimal Logic (M →). LMT→ is aimed to be used for proof
search in M →, in a bottom-up approach. Termination of the calculus is guaranteed by a strategy of rule application that forces an ordered way to search for proofs such that all possible combinations are stressed. For an initial formula α, proofs in LMT→ has an upper bound of |α|.2 |α|+1+2·log2|α|, which together with the system strategy ensure decidability. System rules are conceived to deal with the necessity of hypothesis repetition and the contextsplitting nature of → left, avoiding the occurrence of loops and the usage of backtracking. Therefore, LMT→ steers the proof search always in a forward, deterministic manner. LMT→ has the property to allow extractability of counter-models from failed proof searches (bicompleteness), i.e., the attempt proof tree of an expanded branch produces a Kripke model that falsifies the initial formula. Counter-model generation (using Kripke semantics) is achieved as a consequence of the completeness of the system. LMT→ is implemented as an interactive theorem prover based on the calculus proposed here. We compare our calculus with other known deductive systems for M →, especially
with Fitting s Tableaux, a method that also has the bicompleteness property. We also proposed here a translation of LMT→ to the Dedukti proof checker as a way to evaluate the correctness of the implementation regarding the system specification and to make our system easier to compare to others.
|
28 |
[en] LAW AND ORDER(ING): PROVIDING A NATURAL DEDUCTION SYSTEM AND NON-MONOTONIC REASONING TO AN INTUITIONISTIC DESCRIPTION LOGIC / [pt] LEI E ORDENAÇÃO: ADICIONANDO DEDUÇÃO NATURAL E MECANISMOS DE RACIOCÍNIO NÃO MONOTÔNICO A UMA LÓGICA DESCRITIVA INTUICIONISTABERNARDO PINTO DE ALKMIM 30 January 2024 (has links)
[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.
|
29 |
[pt] A LÓGICA SOBRE LEIS IALC: IMPLEMENTAÇÃO DE PROVAS DE CORREÇÃO E COMPLETUDE E PROPOSTA DE FORMALIZAÇÃO DA LEGISLAÇÃO BRASILEIRA / [en] THE LOGIC ON LAWS IALC: IMPLEMENTATION OF SOUNDNESS AND COMPLETENESS PROOFS AND A PROPOSAL FOR FORM- ALIZATION OF BRAZILIAN LAWBERNARDO PINTO DE ALKMIM 19 March 2020 (has links)
[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.
|
30 |
[en] THE INFINITE JUDGMENTS: THEIR FUNCTION AND THEIR NATURE - SOME ASPECTS OF THE PREDICATIVE NEGATION IN THE CRITIQUE OF PURE REASON / [pt] FUNÇÃO E NATUREZA DOS JUÍZOS INFINITOS: ASPECTOS DA NEGAÇÃO PREDICATIVA NA CRÍTICA DA RAZÃO PURAFABIO FRANCOIS MENDONCA DA FONSECA 03 March 2008 (has links)
[pt] O trabalho se destina a elucidar os motivos pelos quais
Kant postula, na
Crítica da Razão Pura, a tese de que os juízos infinitos
da forma S é não-P não se
reduzem aos afirmativos da forma S é P e nem aos negativos
da forma S não é
P. A distinção não parece se sustentar na abordagem
extensional que é própria da
Lógica Geral, uma vez que a equivalência entre juízos
infinitos e negativos se revela
incontornável. O método adotado segue as advertências
dadas pelo próprio Kant e
consiste em localizar algum passo da argumentação
desenvolvida na Dialética
Transcendental onde esta forma judicativa desempenhe um
papel exclusivo e
imprescindível. Duas hipóteses são examinadas. A primeira
é que os juízos infinitos
têm papel essencial na formulação e na solução da Primeira
Antinomia da Razão
Pura. A segunda é que têm função na formulação do
Princípio da Determinação
Completa, o qual é suscitado a pretexto de se elucidar o
Ideal Transcendental da
Razão Pura. Esta segunda hipótese se mostrará de fato a
solução do nosso
problema, mas terá repercussões sérias na interpretação de
toda Crítica da Razão
Pura, sobretudo ao pressupor um aspecto intensional da
predicação que, no geral,
tem sido desconsiderado e, por vezes, até mesmo recusado
pelo comentário da
filosofia de Kant. / [en] The task of this work is explaining why Kant claims in
Critique of Pure
Reason that infinite judgments of the form S is not-P are
not reducible to the
affirmative ones of the form S is P nor to the negative
ones of the form S is not
P The distinction does not seem justifiable in the
extensional approach that is
proper of General Logic, since the equivalence between
infinite and negative
judgments ends up to be inevitable. We adopt a method that
is suggested by Kant s
advices, which consists in looking for some moment in the
discussion of
Transcendental Dialectic where this form of judgment plays
an exclusive and
indispensable role. Two hypotheses are examined. The first
one is that infinite
judgments have an essential role in the formulation and in
the solution of the First
Antinomy of Pure Reason. The second one is that they have
function in the
formulation of the Principle of Complete Determination,
which is mentioned in
order to explain the Transcendental Ideal of Pure Reason.
Actually, this second
hypothesis will show up as the solution for our problem,
but also will have strong
repercussions at the interpretation of the whole Critique
of Pure Reason, especially
for presupposing an intensional aspect of predication that
generally has been ignored
and sometimes denied by Kantian philosophy s commentators.
|
Page generated in 0.0384 seconds