A resolução proposicional é um sistema completo de provas?

15

Esta pergunta é sobre lógica proposicional e todas as ocorrências de "resolução" devem ser lidas como "resolução proposicional".

Essa questão é extremamente básica, mas está me incomodando há algum tempo. Vejo pessoas afirmarem que a resolução proposicional está completa, mas também vejo pessoas afirmarem que a resolução está incompleta. Entendo o sentido em que a resolução é incompleta. Também vejo por que as pessoas podem afirmar que está completa, mas a palavra "completo" difere da maneira como "completo" é usada ao descrever dedução natural ou cálculo sucessivo. Mesmo o qualificador "refutação concluída" não ajuda porque as fórmulas precisam estar em CNF e a transformação de uma fórmula em uma fórmula CNF equivalente ou em uma fórmula CNF equisatisfatória por meio da transformação Tseitin não é contabilizada no sistema de prova.

Solidez e Completude

Vamos assumir o estabelecimento da lógica proposicional clássica com uma relação entre algum universo de estruturas e um conjunto de fórmulas e a noção tarskiana clássica de verdade em uma estrutura. Nós escrevemos φ se φ é verdadeira em todas as estruturas sendo considerado. Eu também assumirá um sistema φφ para derivar fórmulas a partir de fórmulas.

O sistema é som com respeito a se sempre que temos & Phi; , nós também temos & Phi; . O sistema está completo em relação a se sempre que tivermos φ , também tivermos φ .φφφφ

A regra da resolução

Um literal é uma proposição atômica ou sua negação. Uma cláusula é uma disjunção de literais. Uma fórmula no CNF é uma conjunção de cláusulas. A regra de resolução afirma que

A regra de resolução afirma que, se a conjunção da cláusula com a cláusula ¬ p D for satisfatória, a cláusula C DCp¬pDCD também deverá ser satisfatória.

Não tenho certeza se a regra de resolução sozinha pode ser entendida como um sistema de prova, porque não existem regras para a introdução de fórmulas. Suponho que pelo menos precisamos de uma regra de hipótese que permita a introdução de cláusulas.

Incompleto de resolução

Sabe-se que a resolução é um sistema à prova de som. Ou seja, se pudermos derivar uma cláusula de uma fórmula F usando resolução, então FCF . Resolução também érefutaçãosignificadocompletose tivermosFFC então podemos derivar de F usando resolução.FF

Considere a fórmula

e ψ : = p q .φ:=pqψ:=pq

No sistema LK de Gentzen ou usando dedução natural, posso derivar a implicação inteiramente dentro do sistema de prova. Não posso derivar essa implicação usando a resolução, porque se eu começar com φ , não haverá resoluções.φψφ

Vejo como posso provar a validade dessa implicação usando a resolução:

  1. Considere a fórmula ¬(φψ)
  2. Transforme a fórmula acima em CNF usando regras de distributividade padrão ou usando a transformação Tseitin
  3. Derivar da fórmula transformada usando resolução.

Essa abordagem é insatisfatória para mim porque exige que eu execute as etapas (1) e (2) que estão fora do sistema de prova de resolução. Portanto, parece que existe uma sensação muito clara de que a resolução não está completa da maneira que dizemos que a dedução natural ou os cálculos sequenciais estão completos.

Questões

Dado tudo isso acima, minhas perguntas são:

  1. Que sistema de prova está sendo considerado ao discutir a resolução? É apenas a regra de resolução? Quais são as outras regras?
  2. Parece-me muito claro que a resolução não está completa no sentido de que a dedução natural e os cálculos sequenciais estão completos. A literatura que afirma que a resolução é terminologia de abuso completa apenas porque o sentido em que a resolução é concluída é mais interessante do que o sentido em que é incompleta?
  3. Essa diferença nas noções de completude aplicada à resolução e em outros lugares e como reconciliá-las foi discutida com maior profundidade na literatura?
  4. Percebo também que a resolução pode ser formulada dentro de cálculos sequenciais em termos da regra de corte. A visão teórica da resolução da prova "correta" é apenas um fragmento do cálculo seqüencial que é suficiente para verificar a satisfação das fórmulas na CNF?
Vijay D
fonte
1
(1) fórmulas CNF com apenas resolução (ou, se você fizer QBF, então fórmulas QCNF com resolução e redução total); (2) Sim, é refutação completa e ainda tem um significado ligeiramente diferente, a saber, se então ψ . ψψ
Radu GRIGore
pergunta aproximadamente semelhante aqui. thx para postagem. basicamente, iiuc / afaik, a resolução é usada para sistemas muito mais do que a lógica de 1ª ordem, mas dentro da lógica de 1ª ordem é "som / completo", embora isso nem sempre seja muito bem descrito, porque geralmente é usado apenas para provas de refutação. nos sistemas "maiores", onde os termos não são meramente variáveis ​​booleanas, mas, por exemplo, qualificadores existenciais, etc., não está completo. o campo da lógica não padronizar suas definições da terminologia muito bem, há um monte de "sobrecarga" de termos etc ....
vzn
1
É por isso que algumas pessoas dizem que é " refutacionalmente completo", por exemplo, L. Bachmair e H. Ganzinger, "Resolução do teorema da resolução", Manual de raciocínio automatizado, vol. 1, pp. 19–99, 2001.
Trylks
A questão discute a integridade refutacional.
Vijay D

Respostas:

10

Que sistema de prova está sendo considerado ao discutir a resolução? É apenas a regra de resolução? Quais são as outras regras?

Discuto a resolução no contexto de "cláusulas", que são sequências compostas apenas de literais . Uma cláusula clássica pareceria Mas também podemos escrevê-la como

A1,,AnB1,,Bm
e trabalhar com apenas um lado sequentes. É convencional tratar essas seqüências unilaterais comovários conjuntosde literais.
A¯1,,A¯n,B1,,Bm

LK restrito a cláusulas possui apenas quatro regras de inferência:

  • identidade
  • cut (resolução proposicional)
  • contração (fatoração proposicional)
  • enfraquecendo

É óbvio que essas quatro regras estão completas para deduzir cláusulas, ou seja,

Proposição 1 Para qualquer cláusula e conjunto de cláusulas SCSSCSC

A prova de refutação converte o problema de em SN ( C ) , onde N ( C ) = { { ˉSCSN(C)N(C)={{A¯}AC}C

É claro que SCSN(C)

CSSCSN(C)

O ponto de converter o problema em provas de refutação é duplo:

  • N(C)
  • Temos um controle sobre a lógica completa de predicados, cujas fórmulas podem ser transformadas em CNF até a satisfação.

A visão teórica da resolução da prova "correta" é apenas um fragmento do cálculo seqüencial que é suficiente para verificar a satisfação das fórmulas na CNF?

De fato!

Uday Reddy
fonte
Obrigado Uday. Uma pergunta: a regra de corte ainda mantém as cláusulas da fórmula original redonda no consequente. Na resolução, eles são "otimizados" com apenas uma cláusula no consequente. Você concorda que essa resolução é uma regra mínima ou local devido a todas as cláusulas que não aparecem na regra?
precisa
@VijayD. Estamos usando precisamente a regra do corte, mas de uma maneira diferente de Gentzen. Provas Gentzen seria da formaCSC
você também poderia adicionar à sua resposta o que você acha que é uma descrição precisa e com uma frase da integridade da resolução?
Vijay D
@VijayD. Havia duas declarações "se e somente se" na minha resposta original, que eram as duas propriedades de completude. Para maior clareza, eu os destaquei como proposições para você. (Eu ainda não estou certo de onde suas mentiras confusão Talvez isso tenha a ver com o idioma que estamos a trabalhar com, como Kaveh tem implicado.?)
Uday Reddy
2
@VijayD. Eu não acho que você possa dizer que a resolução está "incompleta". Tudo o que você disse em sua pergunta original foi que as transformações necessárias para colocar fórmulas proposicionais em forma de oração são "insatisfatórias" para você. Isso não significa que eles estejam "incompletos".
precisa
13

1)

A única regra não estrutural é a resolução (nos átomos).

φC,ψC¯φψ

No entanto, uma regra por si só não fornece um sistema de prova. Veja a parte 3.

2)

Pense desta maneira: o PK de cálculo sequencial de Gentzen está completo se estivermos usando algum outro conjunto de conectivos no lugar de {,,¬}? Os conectivos lógicos usados ​​são importantes para resultados lógicos, como integridade. É com relação às fórmulas nesse idioma que um sistema de prova pode ser completo. PK não pode falar sobre fórmulas em outro idioma. Seu problema com a resolução é semelhante. Sim, se estamos falando de integridade em relação a fórmulas gerais com{,,¬} conectivos, a resolução não está completa, mas também não são cálculos sequenciais e deduções naturais com relação a fórmulas que não estão em seu idioma.

Enquanto houver uma tradução "legal" de um idioma para outro, podemos falar sobre integridade. O que importa essencialmente é que podemos traduzir fórmulas de uma para a outra e vice-versa com eficiência. Você pode verificar a tese de Robert Reckhow, onde ele lida com a questão do conectivo e mostra que, para os sistemas Frege, a duração das provas não muda mais do que um polinômio; portanto, é bom, em certo sentido, escolher qualquer conjunto de conectivos adequados que você goste.

A situação da resolução é semelhante. Pela redução do SAT para o 3SAT, podemos restringir nossa atenção aos CNFs e a transformação pode ser feita com muita eficiência.

Observe que a resolução não está sozinha aqui, o problema também se aplica a outros sistemas de prova. Tomemos, por exemplo, Frege de profundidade limitada, onde a profundidade das fórmulas deve ser delimitada por uma constante; portanto, por definição, ela não pode provar nenhuma família de fórmulas de profundidade ilimitada.

3)

Vamos definir o que significa que um sistema de prova de proposição seja completo. Por Cook-Reckhow, um sistema de prova proposicionalP é uma relação binária P Satisfazendo as seguintes condições:

  • Eficiência: P é decidível em tempo polinomial, ou seja, dada uma string φ (fórmula) e uma string π (prova), podemos decidir se π é um Pà prova de φ em tempo polinomial.

  • Solidez: se houver Pà prova de φ, então φ é verdade.

  • Completude: se φ é verdade, então há um Pà prova de φ.

A definição é muito geral e não fala sobre a estrutura da prova. Qualquer coisa que satisfaça essas condições é um sistema de prova proposicional.

Que classe de fórmula devemos considerar nesses itens? Diferentes classes de fórmulas foram consideradas e o primeiro tratamento do problema que conheço é a tese de Robert Reckhow onde ele mostra que, desde que se preocupe com os sistemas Frege, não importa qual conjunto adequado de conectores se usa, todos eles são equivalentes.

Em relação à resolução, se alguém realmente deseja ter integridade em relação a todas as fórmulas e não apenas aos CNFs, pode incorporar uma tradução em tempo polinomial fixo de fórmulas arbitrárias para CNFs no sistema de prova sem nenhum problema, pois a tradução é computável em tempo polinomial.

De qualquer forma, o sistema de prova de resolução funciona da seguinte maneira: verifica se o π é uma derivação de usando a regra de resolução do conjunto de cláusulas obtidas na tradução de ¬φa cláusulas. Este é o sistema de prova proposicional que as pessoas chamam de sistema de prova proposicional de resolução.

4)

A resolução é boa como está, no entanto, também se pode pensar da maneira mencionada, ou seja, é claro que podemos pensar nela como a regra de corte quando a fórmula de corte é um átomo positivo movendo os átomos negativos para o antecedente e mantendo o positivos no sucessivo:

φ,CCψφ,ψ

Observe que o que define o poder de um sistema de prova proposicional nos subsistemas de Frege (e mesmo nos subsistemas de sistemas de prova proposicional semelhantes mais poderosos, como a lógica proposicional quantificada G) é principalmente a classe de fórmulas que se pode cortar. Acho que podemos usar a PK de Gentzen e apenas restringir a regra de corte a ser aplicada a essas fórmulas de corte e o sistema de prova resultante não será mais poderoso que a resolução na comprovação de CNFs. Qualquer prova de um CNFs (escrito na forma sequencial com átomos positivos) pode ter apenas sequências semelhantes, ou seja, fórmulas mais complicadas não servem para provar CNFs (observe que o corte é a única regra que pode remover fórmulas dos sequentes).

ps: Minha resposta é principalmente da perspectiva teórica da complexidade da prova. Você pode querer verificar outras perspectivas, como a teoria da prova estrutural .

Referências:

Kaveh
fonte
Obrigado pela sua resposta. Vejo como Uday está dizendo coisas semelhantes, mas descobri que poderia seguir sua resposta com mais facilidade.
precisa
@VijayD, claro, não há problema. :)
Kaveh