Eliminação de redundância no cálculo de superposição

Ao provar os teoremas com o cálculo de superposição, lidamos com três tipos de regras:

1. Gerando regras: a partir do par de cláusulas A e B, gere uma nova cláusula C, mantendo o par original, por exemplo, superposição no caso geral.

2. Regras de reescrita: da cláusula A gera uma nova cláusula B, por exemplo, reflexividade da igualdade, fatoração da igualdade; a superposição com uma equação unitária também pode ser considerada uma regra de reescrita.

3. Eliminar regras: excluir uma cláusula, por exemplo, subsunção, eliminação de tautologia.

A questão é, em relação à segunda categoria, podemos executar uma reescrita rigorosa, substituindo a cláusula original pela nova ou temos que manter tanto a original quanto a nova? No caso da reflexividade da igualdade, parece que podemos fazer a primeira, mas para o fatoramento e a superposição da igualdade com uma equação unitária, não está imediatamente claro se isso preservaria a integridade.

Existe uma maneira geral de saber qual é o caso? Ou uma lista do que precisa ser feito em cada caso?

Uma das principais implementações do provador do teorema do cálculo de superposição é E. Na descrição de sua tecnologia, ele apresenta algumas teorias e antecedentes básicos em Procedimento de prova :

E usa a variante DISCOUNT [DKS97] do algoritmo de cláusula fornecida. O estado de prova é representado por dois conjuntos de cláusulas, o conjunto P de cláusulas processadas (inicialmente vazias) e o conjunto U de cláusulas não processadas. As cláusulas em U são classificadas de acordo com uma função de avaliação heurística e são processadas em ordem. O processamento simplificará primeiro a cláusula selecionada g com todas as cláusulas em P, depois simplificará P com g (movendo todas as cláusulas afetadas de P de volta para U) e depois calculará todas as consequências diretas entre g e P que podem ser derivadas usando as regras de inferência geradoras (superposição, fatoração de igualdade e resolução de igualdade). As novas cláusulas são simplificadas em relação a P e adicionadas a U, g é adicionado a P.

Esse procedimento de prova é diferente do algoritmo de cláusula fornecida implementado no Otter (e em muitos provadores desde então), que também usa U para simplificação. A variante E usa foi popularizada pela primeira vez por DISCOUNT, mas também está no centro da Waldmeister. O vampiro e o SPASS o implementam além do algoritmo primário.

portanto, [iiuc] a palavra "reescrita" pode ser um pouco inadequada nas implementações reais das regras de prova do teorema, porque as cláusulas originais nunca são "excluídas" e sempre retidas, caso possam ser afetadas ou combinadas com derivações posteriores. a reescrita "move" "reescrita" cláusulas entre$P$ e $U$ em ambas as direções.

ou seja, reescrever é basicamente como uma adição de novas cláusulas derivadas (verdadeiras) a uma lista de cláusulas verdadeiras conhecidas, e o movimento entre e é uma estratégia para encontrar novas cláusulas verdadeiras de maneira eficiente (basicamente rastreando a "fronteira" em um pesquisa mista de profundidade / largura, ordenada pela função de prioridade) e é o conjunto de cláusulas verdadeiras conhecidas.$P$$U$$P \cup U$

não sei de um juiz para isso, mas acho que aqui está a teoria sobre tudo isso. suponha que e seja "excluído". ainda é possível derivar por outras derivações e cláusulas. nesse caso, não teria efeito. mas se não puder ser derivado por outras rotas, em teoria, isso poderá levar a transformar um problema completo em um problema incompleto. Não conheço uma referência que mostre isso. pode ser um exercício factível para o leitor ter um exemplo.$A \implies B$$A$$B \implies A$

^{fineprint: apunhalando esta questão devido à falta de outras respostas. Também estou interessado em uma resposta realmente autorizada a essa pergunta. provavelmente existe um melhor que o anterior, mas este é o melhor encontrado até agora, após algumas pesquisas. suspeite que a questão possa ser melhor abordada em, por exemplo, math.se, mathoverflow ou TCS.se. também achou difícil encontrar descrições básicas desses conceitos e sem um jargão especializado pesado.}