PPGSC - Mestrado em Sistemas e Computação

URI Permanente para esta coleçãohttps://repositorio.ufrn.br/handle/123456789/12059

Navegar

Agora exibindo 1 - 6 de 6

Algebraic semantics for Nelson’s logic S
(2018-01-25) Silva, Thiago Nascimento da; Rivieccio, Umberto; Almeida, João Marcos de; ; ; ; Mariano, Hugo Luiz;
Além da mais conhecida lógica de Nelson (𝒩3) e da lógica paraconsistente de Nelson (𝒩4), David Nelson introduziu no artigo de 1959 "Negation and separation of concepts in constructive systems", com motivações de aritmética e construtividade, a lógica que ele chamou de "𝒮". Naquele trabalho, a lógica é definida por meio de um cálculo (que carece crucialmente da regra de contração) tendo infinitos esquemas de regras, e nenhuma semântica é fornecida. Neste trabalho nós tomamos o fragmento proposicional de 𝒮, mostrando que ele é algebrizável (de fato, implicativo) no sentido de Blok & Pigozzi com respeito a uma classe de reticulados residuados involutivos. Assim, fornecemos a primeira semântica para 𝒮 (que chamamos de 𝒮-álgebras), bem como um cálculo estilo Hilbert finito equivalente à apresentação de Nelson. Fornecemos um algoritmo para construir 𝒮-álgebras a partir de 𝒮-álgebras ou reticulados implicativos e demonstramos alguns resultados sobre a classe de álgebras que introduzimos. Nós também comparamos 𝒮 com outras lógicas da família de Nelson, a saber, 𝒩3 e 𝒩4.
Algebraization in quasi-Nelson logics
(Universidade Federal do Rio Grande do Norte, 2023-10-31) Lima Neto, Clodomir Silva; Rivieccio, Umberto; Almeida, João Marcos de; https://orcid.org/0000-0003-2601-8164; http://lattes.cnpq.br/3059324458238110; http://lattes.cnpq.br/0597230560325577; https://orcid.org/0000-0001-9835-9481; http://lattes.cnpq.br/6847191906266562; Santiago, Regivan Hugo Nunes; Biraben, Rodolfo Ertola
A lógica quase-Nelson é uma generalização recentemente introduzida da lógica construtiva com negação forte de Nelson para um cenário não involutivo. O presente trabalho se propõe a estudar a lógica de alguns fragmentos da lógica de quase-Nelson, a saber: pocrims (ℒQNP) e semihoops (ℒQNS); além da lógica de quase-N4-reticulados (ℒQN4). Isso é feito por meio de uma axiomatização através de um cálculo finito no estilo Hilbert. A principal questão que abordaremos é se a semântica algébrica de um determinado fragmento da lógica quase-Nelson (ou classe quase-N4-reticulados) pode ser axiomatizada por meio de equações ou quase-equações. A ferramenta matemática utilizada nesta investigação será a representação twist-álgebra. Chegando à questão da algebrização, lembramos que a lógica quase-Nelson (como extensão de ℱℒew) é algebrizável no sentido de Blok e Pigozzi. Além disso, mostramos a algebrizabilidade de ℒQNP, ℒQNS e LQN4, que é BPalgebrizável com o conjunto de equações definidoras E(x) := {x = x → x} e o conjunto de fórmulas de equivalência ∆(x, y) := {x → y, y → x, ∼ x →∼ y, ∼ y → ∼ x}.
Hilbert-style formalism for two-dimensional notions of consequence
(Universidade Federal do Rio Grande do Norte, 2022-02-21) Greati, Vitor Rodrigues; Almeida, João Marcos de; Marcelino, Sérgio Roseiro Teles; 00000000000; http://lattes.cnpq.br/3059324458238110; http://lattes.cnpq.br/0343448850800210; Rivieccio, Umberto; http://lattes.cnpq.br/0597230560325577
O presente trabalho propõe um formalismo dedutivo bidimensional à Hilbert (H-formalismo) para relações de B-consequência, uma classe de lógicas bidimensionais que generalizam as noções usuais (tarskianas, unidimensionais) de lógica. Nós sustentamos que o ambiente bidimensional é apropriado para o estudo do bilateralismo em lógica, por permitir que julgamentos primitivos de asserção e rechaço (ou, como preferimos, as atitudes cognitivas de aceitação e rejeição) ajam em dimensões independentes e capazes de interagir entre si ao determinar as inferências válidas de uma lógica. Nessa perspectiva, o formalismo proposto constitui um aparato inferencial para raciocinar sobre julgamentos bilateralistas. Após uma descrição detalhada do funcionamento do formalismo proposto, o qual é inspirado nos sistemas de Hilbert simétricos, nós provemos um algoritmo de busca de demonstrações que executa em tempo exponencial, em geral, e em tempo polinomial quando apenas regras contendo no máximo uma fórmula no sucedente estão presentes no sistema em questão. Então, nós passamos a investigar semânticas não-determinísticas bidimensionais por meio de estruturas de matrizes contendo dois conjuntos de valores distinguidos, um qualificando alguns valores de verdade como aceitos, e o outro, alguns valores como rejeitados, constituindo um caminho semântico para o bilateralismo no ambiente bidimensional. Nós apresentamos também um algoritmo para a produção de sistemas de Hilbert bidimensionais para matrizes não-determinísticas bidimensionais suficientemente expressivas, bem como alguns procedimentos de simplificação que permitem reduzir consideravelmente o tamanho e a complexidade do sistema resultante. Para matrizes finitas, vale apontar, o procedimento resulta em sistemas finitos. Ao final, como estudo de caso, investigamos a lógica da inconsistência formal chamada mCi quanto à sua axiomatizabilidade por sistemas ao estilo de Hilbert. Demonstramos que não há sistemas de Hilbert finitos unidimensionais que capturem essa lógica, mas que ela habita uma relação de consequência bidimensional finitamente axiomatizável por um sistema de Hilbert bidimensional. A existência desse sistema segue diretamente do algoritmo de axiomatização proposto, em vista da semântica bidimensional 5-valorada não-determinística suficientemente expressiva que determina a relação de consequência bidimensional mencionada.
A integração do tutorial interativo TryLogic via IMS Learning Tools Interoperability: construindo uma infraestrutura para o ensino de Lógica através de estratégias de demonstração e refutação
(Universidade Federal do Rio Grande do Norte, 2013-06-03) Terrematte, Patrick Cesar Alves; Almeida, João Marcos de; ; ; Haeusler, Edward Hermann; ; http://lattes.cnpq.br/6075905438020841; Miranda, Leonardo Cunha de; ; Santiago, Regivan Hugo Nunes; ; http://buscatextual.cnpq.br/buscatextual/visualizacv.do?id=K4790032Z4
A disciplina de Lógica representa um desa o tanto para docentes como para discentes, o que em muitos casos resulta em reprovações e desistências. Dentre as dificuldades enfrentadas pelos alunos está a sobrecarga da capacidade cognitiva para compreender os conceitos lógicos de forma relevante. Neste sentido, as ferramentas computacionais de aprendizagem são recursos que auxiliam a redução de cenários de sobrecarga cognitiva, como também permitem a experiência prática de conceitos teóricos. O presente trabalho propõe uma tutorial interativo chamado TryLogic, visando ao ensino da tarefa de Demonstração ou Refutação (DxR) de conjecturas lógicas. Trata-se de uma ferramenta desenvolvida a partir da arquitetura do TryOcaml através do suporte de comunicação da interface web ProofWeb para acessar o assistente de demonstração de teoremas Coq. Os objetivos do TryLogic são: (1) Apresentar um conjunto de lições para aplicar estratégias heurísticas de análise de problemas em Lógica Proposicional; (2) Organizar em passo-a-passo a exposi ção dos conteúdos de Dedução Natural e Semântica Proposicional de forma sequencial; e (3) Fornecer aos alunos tarefas interativas. O presente trabalho propõe também apresentar a nossa implementação de um sistema formal de refutação; descrever a integração de nossa infraestrutura com o Ambiente Virtual de Aprendizagem Moodle através da especi cação IMS Learning Tools Interoperability ; apresentar o Gerador de Conjecturas de tarefas de Demonstração e Refutação e, por m, avaliar a experiência da aprendizagem de alunos de Lógica através da aplicação da tarefa de DxR em associação à utilização do TryLogic
On rich modal logics
(Universidade Federal do Rio Grande do Norte, 2013-11-19) Dodó, Adriano Alves; Bedregal, Benjamin René Callejas; ; http://buscatextual.cnpq.br/buscatextual/visualizacv.do?id=K4781417E7; ; http://lattes.cnpq.br/5374175200188654; Nalon, Cláudia; ; http://lattes.cnpq.br/7793795625581127; Pimentel, Elaine Gouvêa; ; http://lattes.cnpq.br/3298246411086415; Almeida, João Marcos de;
Esta dissertação trata do enriquecimento de lógicas modais. O termo enriquecimento é usado em dois sentidos distintos. No primeiro deles, de fundo semântico, propomos uma semântica difusa para diversas lógicas modais normais e demonstramos um resultado de completude para uma extensa classe dessas lógicas enriquecidas com múltiplas instâncias do axioma da confluência. Um fato curioso a respeito dessa semântica é que ela se comporta como as semânticas de Kripke usuais. O outro enriquecimento diz respeito à expressividade da lógica e se dá por meio da adição de novos conectivos, especialmente de negações modais. Neste sentido, estudamos inicialmente o fragmento da lógica clássica positiva estendido com uma negação modal paraconsistente e mostramos que essa linguagem é forte o suficiente para expressar as linguagens modais normais. Vemos que também é possível definir uma negação modal paracompleta e conectivos de restauração que internalizam as noções de consistência e determinação a nível da linguagem-objeto. Esta lógica constitui-se em uma Lógica da Inconsistência Formal e em uma Lógica da Indeterminação Formal. Em tais lógicas, com o objetivo de recuperar inferências clássicas perdidas, demonstram-se Teoremas de Ajuste de Derivabilidade. No caso da lógica estendida com uma negação paraconsistente, se removermos a implicação ainda lidaremos com uma linguagem bastante rica, com ambas negações paranormais e seus respectivos conectivos de restauração. Sobre esta linguagem estudamos a lógica modal normal minimal definida por meio de um cálculo de Gentzen apropriado, à diferença dos demais sistemas estudados até então, que são apresentados via cálculo de Hilbert. Em seguida após demonstrarmos a completude do sistema dedutivo associado a este cálculo, introduzimos algumas extensões desse sistema e buscamos Teoremas de Ajuste de Derivabilidade adequados
What is a Fuzzy Bi-implication?
(Universidade Federal do Rio Grande do Norte, 2012-02-13) Olguín, Claudio Andrés Callejas; Bedregal, Benjamin René Callejas; Musicante, Martin Alejandro; ; http://lattes.cnpq.br/6034405930958244; ; http://buscatextual.cnpq.br/buscatextual/visualizacv.do?id=K4781417E7; ; http://lattes.cnpq.br/6212733101266338; Almeida, João Marcos de; ; Santiago, Regivan Hugo Nunes; ; http://buscatextual.cnpq.br/buscatextual/visualizacv.do?id=K4790032Z4; Viana, Jorge Petrucio; ; http://lattes.cnpq.br/2332327416299928
A fim de tornar este documento auto-suficiente, nós apresentamos toda a teoria necessária como arcabouço teórico. Em seguida, estudamos várias definições que estenderam a bi-implicação clássica para o domínio da bem estabelecida lógica difusa, ou seja, no intervalo [0; 1]. Essas abordagens da bi-implicação difusa podem ser resumidas da seguinte forma: duas definições axiomatizadas, que demonstramos que representam a mesma classe de funções, quatro padrões definitórios (dois deles proposto por nós), que variam com o número de diferentes operadores que as compõem e quais restrições que tinham para satisfazer. Nós demonstramos que esses padrões definitórios representam apenas duas classes de funções, tendo uma como uma subclasse própria da outra, mas sendo ambas subclasses da classe representada pelas definições axiomatizadas. Uma vez que esses três clases satisfazer algumas restrições que julgamos desnecessárias, propusemos um novo padrão definitório sem essas restrições e que representa uma classe de funções que se interseta com a classe representada pelas definições axiomatizadas. Nesta dissertação estamos pretendendo estabelecer as bases para futuras pesquisas sobre este operador

SIGAA

Navegar

Navegando PPGSC - Mestrado em Sistemas e Computação por Autor "Almeida, João Marcos de"