Este artigo investiga a complexidade de tamanho e a decidibilidade da progressão de primeira ordem, um método para atualizar bases de conhecimento em IA. Ele demonstra que, para classes de ações específicas dentro da estrutura do Cálculo de Situações, a progressão de primeira ordem cresce polinomialmente e mantém a decidibilidade ao usar certos fragmentos de base de conhecimento.
O trabalho investiga como codificar tarefas fatoradas, uma representação clássica de planejamento, em SAT. Ele propõe várias estratégias para traduzir a relação de transição fatorada em lógica proposicional e analisa o impacto das transformações de tarefas no desempenho de planejadores baseados em SAT.
Research Math Agents (RMA) é uma estrutura agêntica desenvolvida para raciocínio automatizado em problemas matemáticos complexos de nível de pesquisa, diferenciando-se de trabalhos anteriores em matemática competitiva ou prova de teoremas formais. RMA utiliza módulos especializados e agentes coordenados que colaboram na geração, refinamento e verificação de provas candidatas através de um fluxo de trabalho multi-função e multi-rodada, usando uma memória estruturada compartilhada.
DreamProver é uma estrutura agente que utiliza um paradigma de indução de programa "wake-sleep" para descobrir lemas reutilizáveis para a prova formal de teoremas. Ele evolui iterativamente uma biblioteca de lemas compacta e transferível, melhorando substancialmente o desempenho em teoremas nunca antes vistos.