Grafik pembatasan teori untuk Bukti dalam Teori Kompleksitas Bukti

Kompleksitas bukti adalah area paling dasar dari teori kompleksitas komputasi. Tujuan utama dari area ini adalah untuk membuktikan , yaitu, setiap prover tidak dapat memberikan bukti ketidakpuasan formula input yang diberikan. $NP\neq coNP$

Grafik adalah salah satu model bukti formal. Pertanyaan saya adalah tentang pembatasan lebih lanjut untuk model ini.

Suatu bukti direpresentasikan sebagai DAG. Node dengan fan-in 0 memiliki label aksioma. Node unik dengan fan-out 0 sesuai dengan "false." Untuk aturan input deduksi yang diberikan, setiap node yang memiliki derajat dan derajat memiliki label yang mewakili proposisi.

Pertanyaanku adalah:

Apakah ada sistem pembuktian dan penelitian terkait dalam hal bahwa kelas pembuktian-DAG dibatasi? Makalah, survei, dan catatan kuliah dipersilakan.

Apakah Sistem Bukti yang sebelumnya dipelajari seperti Nullstellensatz, Resolution, LS, AC0 Frege, RES (k), Polinomial Caluculus, dan Cutting Planes, memiliki beberapa grafik karakterisasi teoritik ??

Pembatasan paling alami pada bukti DAG adalah bahwa itu adalah pohon - yaitu, "lemma" (kesimpulan perantara) tidak digunakan lebih dari sekali. Properti ini disebut "mirip pohon". Resolusi umum secara eksponensial lebih kuat daripada resolusi seperti pohon, seperti yang ditunjukkan misalnya oleh Ben-Sasson, Impagliazzo dan Wigderson . Konsep ini juga telah dipertimbangkan untuk sistem pembuktian lainnya - cukup cari "pohon seperti X", di mana X adalah sistem pembuktian yang menarik bagi Anda. Dalam kasus resolusi tertentu, ada batasan lain yang dapat dipertimbangkan. Lihat misalnya makalah Alekhnovich, Johannsen, Pitassi dan Urquhart tentang resolusi reguler.

Resolusi mirip pohon sangat penting karena implementasi tradisional DPLL sesuai dengan penolakan resolusi seperti pohon. Teknik pembelajaran klausa, yang penting dalam praktik, sesuai dengan memungkinkan DAG umum. Oleh karena itu struktur DAG bukti juga sangat bergantung pada algoritma yang menghasilkannya.

Studi Müller dan Szeider Bukti resolusi di mana DAG bukti telah membatasi lebar pohon atau lebar jalur terbatas (untuk ekstensi yang sesuai dari langkah-langkah kompleksitas grafik ini ke grafik langsung.)

Mereka menunjukkan bahwa lebar jalur DAG pada dasarnya sama dengan kompleksitas ruang dari bukti, dan mendefinisikan gagasan umum tentang ruang bukti yang setara dengan lebar pohon.

Untuk sistem pembuktian yang cukup kuat, representasi grafik dari pembuktian dalam sistem tampaknya kurang penting, karena (seperti yang sudah dikomentari Joshua Grochow), bukti Frege yang mirip DAG dan yang mirip pohon setara secara polinomi (lihat monografi Krajicek 1995 untuk bukti fakta ini. ).

Untuk sistem bukti yang lebih lemah seperti resolusi, seperti pohon secara eksponensial lebih lemah daripada bukti seperti DAG (seperti yang dijelaskan Yuval Filmus di atas).

Beckmann dan Buss [1] (mengikuti Beckmann [2] ) dianggap membatasi ketinggian (ekuivalen, kedalaman) dari grafik-bukti dari bukti Frege-kedalaman-konstan dan menyelidiki hubungan antara DAG-like, ukuran-pohon dan tinggi kedalaman-konstan Bukti Frege. (Catat perbedaan antara membatasi kedalaman grafik bukti dan membatasi kedalaman sirkuit yang muncul di jalur bukti).

Mungkin juga ada pemisahan antara bukti Nullstellensatz (dan kalkulus polinomial) seperti-pohon dan DAG-seperti, yang saat ini saya tidak ingat.