PPGSC - Doutorado em Sistemas e Computação

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

Navegar

Agora exibindo 1 - 3 de 3

Algebraic semantics and calculi for Nelson's logics
(Universidade Federal do Rio Grande do Norte, 2022-02-18) Silva, Thiago Nascimento da; Almeida, João Marcos de; Rivieccio, Umberto; http://lattes.cnpq.br/0597230560325577; https://orcid.org/0000-0003-2601-8164; http://lattes.cnpq.br/3059324458238110; http://lattes.cnpq.br/1083527025772854; Liang, Fey; Flaminio, Tommaso; Busaniche, Manuela
O objetivo desta tese é estudar uma família de lógicas, composta pelas lógicas de Nelson S, lógica construtiva com negação forte N 3, lógica de quasi-Nelson QN e lógica de quasi-Nelson implicativa QN I. Isto é feito de duas maneiras. A primeira é por meio de uma axiomatização via um cálculo de Hilbert e a segunda é por meio de um estudo de algumas propriedades da correspondente quase-variedade de álgebras. A principal contribuição desta tese é demonstrar que essas lógicas se encaixam dentro da teoria das lógicas algebrizáveis. Fazendo uso dessa teoria, os seguintes resultados são demonstrados. No que diz respeito a S, nós introduzimos a primeira semântica algébrica para ela, axiomatizamo-la por meio de um cálculo de Hilbert contendo um número finito de axiomas, e também encontramos uma versão do teorema da dedução para ela. Em relação às lógicas QN e QN I, nós demonstramos que ambas são algebrizáveis com respeito à quasi-variedade de álgebras de quasi-Nelson e à variedade de àlgebras de quasi-Nelson implicativas, respectivamente; demonstramos que não são auto-extensionais; mostramos como a partir delas podemos obter outras lógicas conhecidas e bem estudadas usando extensões axiomáticas, tal como o {→, ∼}-fragmento da lógica intuicionista, o {→, ∼}- fragmento da lógica construtiva de Nelson com negação forte e a lógica clássica, e também explicitamos o termo quaternário que garante a existência de uma versão do teorema da dedução para QN e QN I. Com respeito a N 3, n´os estudamos o papel da identidade de Nelson ((φ ⇒ (φ ⇒ ψ)) ∧ (∼ ψ ⇒ (∼ ψ ⇒ ∼ φ)) ≈ φ ⇒ ψ) em estabelecer propriedades sobre a ordem do reticulado de sua semântica algébrica. Além disso, n´os estudamos os ⟨∧, ∨, ∼, ¬, 0, 1⟩-subredutos das álgebras de quasi-Nelson e fazendo uso de sua representação twist, nós demonstramos que essa correspondência entre objetos pode ser caracterizada como uma equivalência categorial. Por último, vale notar que como QN I é o {→, ∼}-fragmento de QN , alguns resultados que dizem respeito à QN I são facilmente estendíveis à QN.
Novas técnicas de instanciação e produção de demonstrações para a resolução SMT
(2017-09-05) Barbosa, Haniel Moreira; Deharbe, David Boris Paul; http://lattes.cnpq.br/2985658685449858; https://orcid.org/0000-0003-0188-2300; http://lattes.cnpq.br/6657126741011519; Reynolds, Andrew; Dubois, Catherine; Ábrahám, Erika; Almeida, João Marcos de; https://orcid.org/0000-0003-2601-8164; http://lattes.cnpq.br/3059324458238110; Fontaine, Pascal; Rümmer, Philipp; Merz, Stephan
Em muitas aplicações de métodos formais, como verificação formal, síntese de programas, testes automáticos e análise de programas, é comum depender de solucionadores de satisfatibilidade módulo teorias (SMT) como backends para resolver automaticamente condições que precisam ser verificadas e fornecer certificados de seus resultados. Nesta tese, objetivamos melhorar a eficiência dos solucionadores SMT e aumentar sua confiabilidade. Nossa primeira contribuição é fornecer um arcabouço uniforme e eficiente para raciocinar com fórmulas quantificadas em solucionadores SMT, em que, geralmente, várias técnicas de instanciação são empregadas para lidar com quantificadores. Mostramos que as principais técnicas de instanciação podem ser lançadas neste arcabouço unificador para lidar com fórmulas quantificadas com igualdade e funções não interpretadas. O arcabouço baseia-se no problema de E-ground (dis)unificação, uma variação do problema clássico de E-unificação rígida. Apresentamos um cálculo correto e completo para resolver esse problema na prática: Fechamento de Congruência com Variáveis Livres (CCFV). Uma avaliação experimental é apresentada, na qual medimos o impacto das otimizações e técnicas de instanciação baseadas no CCFV nos solucionadores SMT veriT e CVC4. Mostramos que nossas implementações exibem melhorias em relação às abordagens de última geração em várias bibliotecas de referência, decorrentes de aplicações do mundo real. Nossa segunda contribuição é uma estrutura para o processamento de fórmulas ao mesmo tempo que produz demonstrações detalhadas. Nosso objetivo é aumentar a confiabilidade nos resultados de solucionadores SMT e sistemas de raciocínio automatizado similares, fornecendo justificativas que podem ser verificadas com eficiência de forma independente e para melhorar sua usabilidade por aplicativos externos. Os assistentes de demonstração, por exemplo, geralmente requerem a reconstrução da justificação fornecida pelo solucionador em uma determinada obrigação de prova. Os principais componentes da nossa estrutura de produção de demonstrações são um algoritmo genérico de recursão contextual e um conjunto extensível de regras de inferência. Clausificação, Skolemização, simplificações específicas de teorias e expansão das expressões "let" são exemplos dessa estrutura. Com estruturas de dados adequadas, a geração de demonstrações cria apenas uma sobrecarga de tempo linear, e as demonstrações podem ser verificadas em tempo linear. Também implementamos a abordagem em veriT. Isso nos permitiu simplificar drasticamente a base do código, aumentando o número de problemas para os quais demonstrações detalhadas podem ser produzidas.
On algebras for interval-valued fuzzy logic
(2019-08-30) Pinheiro, Antônia Jocivania; Santiago, Regivan Hugo Nunes; ; ; Almeida, João Marcos de; ; Bedregal, Benjamin Rene Callejas; ; Lodwick, Weldon Alexander; ; Viana, Jorge Petrucio; ; Bergamaschi, Flaulles Boone; ; Dimuro, Graçaliz Pereira;
Este trabalho visa introduzir outras abordagens para a lógica fuzzy com valores intervalares. Essas novas abordagens foram inspiradas nos trabalhos de Lodwick e Chalco sobre intervalos restritos. Esses intervalos restritos foram usados para estender os operadores fuzzy, nos quais eles foram chamados Operadores Intervalares Restritos de Nı́vel Único (C-operador) e suas propriedades foram estudadas. Além disso, esses operadores foram estendidos a operadores corretos chamados Operadores Intervalares Restritos. Uma nova álgebra, chamada SBCI álgebra, que surge da intervalização de BCI álgebras, também é introduzida. Essas álgebras têm como objetivo ser o modelo algébrico para lógicas fuzzy com valores intervalares que levam em conta a noção de correção. Também foi estudada uma nova classe de implicações fuzzy, chamada (T, N )-implicações. O autor investigou o comportamento das BCI/SBCI álgebras e das (T, N )-implicações na nova lógica.

SIGAA

Navegar

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