63 artigos
O artigo apresenta o Apply2Isar, uma ferramenta que converte automaticamente scripts de prova procedurais no estilo "apply" para provas declarativas Isar legíveis e robustas no Isabelle/HOL, validada em um conjunto de benchmarks do Archive of Formal Proofs.
O artigo demonstra que a diferença entre o tamanho mínimo de um circuito booleano e o de uma fórmula sobre a base AIG é sempre 0 ou 1, estabelecendo teoremas que definem quando o compartilhamento de portas é necessário e como essa lacuna unitária surge exclusivamente de um único gate com fan-out 2.
Este artigo propõe os conceitos de autômato de passo e máquina de Turing de passo (STM) como extensões naturais dos modelos tradicionais que permitem a execução de um passo de ações atômicas, preenchendo a lacuna existente na literatura entre a Máquina de Turing e autômatos concorrentes.
Este artigo relata a descoberta, através da formalização em um provador de teoremas interativo, de um erro nos argumentos de um artigo amplamente citado de 2006 sobre a estabilidade do potencial do modelo de dois dupletos de Higgs, invalidando seu teorema principal e representando, até onde se sabe, o primeiro erro não trivial em um artigo de física identificado por meio dessa metodologia.
Este artigo apresenta a teoria de categorias enriquecidas em seminormas dilatadas como um quadro unificador para o Teorema do Limite Central, estabelecendo um teorema abstrato que generaliza resultados clássicos e deriva um novo limite central para variedades simpléticas com aplicações na mecânica estatística.
Este artigo demonstra que, embora a lógica de equipe inquisitiva seja expressivamente equivalente à lógica de primeira ordem para sentenças, suas fórmulas abertas possuem poder expressivo superior, permitindo expressar propriedades não definíveis na lógica de primeira ordem, como a finitude, quando estendida com um quantificador universal gerador de intervalo.
Este artigo desenvolve uma teoria de especificações GSOS abstratas para linguagens de ordem superior, transferindo os princípios do framework de Turi e Plotkin para esse contexto e estabelecendo um resultado geral de composicionalidade que se aplica a sistemas como o cálculo SKI e o cálculo lambda.
Este artigo propõe um quadro de raciocínio abduzido baseado em consistência que integra previsões de múltiplos modelos pré-treinados para mitigar a degradação de desempenho em ambientes novos, utilizando regras lógicas para selecionar um subconjunto de previsões que maximize a cobertura mantendo inconsistências abaixo de um limite, resultando em ganhos significativos de precisão e recall em comparação com modelos individuais e ensembles padrão.
Este artigo propõe o GRAMPUS, uma teoria de tipos modais graduados que utiliza grades temporais para fornecer uma semântica formal rigorosa e um modelo categórico para a especificação de cronogramas de pulsos em computadores quânticos de qubits supercondutores.
O artigo demonstra que o Problema de Skolem é decidível em anéis comutativos finitamente gerados de característica positiva, estabelecendo um algoritmo que determina a existência de termos nulos em sequências de recorrência linear sobre tais anéis.
Este trabalho apresenta algoritmos baseados em CDCL para Enumeração de Modelos Ponderados (WME), integrando propagação, poda e análise de conflitos ponderados em frameworks de retrocesso cronológico e não cronológico para permitir consultas orientadas por pesos, como a enumeração dos k melhores modelos.
Este artigo apresenta uma formalização construtiva de Sistemas de Reescrita Abstratos (ARS) no assistente de prova Agda, eliminando o uso de lógica clássica, refinando critérios de terminação e confluência e demonstrando a aplicabilidade geral através de uma formalização do cálculo lambda.
Este artigo apresenta a formalização em Lean 4 de teoremas do tipo Farkas sobre corpos ordenados linearmente e estende a teoria da dualidade na otimização linear para o caso em que alguns coeficientes podem assumir valores infinitos.
O artigo demonstra que a compacidade de uma estrutura relacional finita de largura um é provável no sistema axiomático ZF, enquanto, caso contrário, essa compacidade implica a existência de conjuntos não mensuráveis no espaço tridimensional.
Este artigo apresenta uma reformulação topológica da geometria de Tarski utilizando a teoria de tipos dependentes no Coq, onde se completa a formalização da geometria de sólidos provando a correspondência entre classes mereológicas e conjuntos abertos regulares, reduzindo o sistema axiomático e estendendo a teoria com propriedades topológicas como a de Hausdorff.
Este artigo propõe uma abordagem neuro-simbólica que integra Grandes Modelos de Linguagem (LLMs) com solucionadores de restrições para gerar lemas auxiliares e verificar conjecturas, demonstrando uma melhoria de cerca de 25% na resolução de tarefas de prova envolvendo definições indutivas em comparação com os solucionadores de última geração.
Este artigo investiga o problema de modificar conceitos de lógica descritiva (EL e ALC) com base em modelos representados como interpretações pontuadas, definindo formalmente os conceitos de evicção, recepção e revisão, e demonstrando que a revisão não se reduz a uma simples combinação das outras duas operações.
O artigo introduz uma noção de "explicação" de modelos probabilísticos generalizados como um tipo específico de span na categoria , demonstrando que tais explicações se compõem via pullback e que todo modelo probabilístico localmente finito possui uma representação clássica canônica e nítida, construída de forma funtorial.
O artigo apresenta o LTLGuard, uma ferramenta modular que combina geração com restrições e verificação formal leve para permitir que modelos de linguagem compactos (4B–14B parâmetros) traduzam requisitos informais em especificações de LTL corretas e consistentes, superando as limitações de modelos menores em lógica temporal.
Este artigo demonstra que, embora a auto-certificação em máquinas de Turing limitadas falhe devido a sobrecargas temporais, o processo iterativo de observações de parada forma uma cadeia cujo limite de Scott resolve para um ponto fixo mínimo que captura o comportamento de parada completo de uma computação ilimitada, oferecendo uma nova perspectiva sobre o problema da parada através do adiamento contínuo da diagonalização.