|
|
Nezadovoljivost i dokazi pobijanjem-poluodlučivost
Zatvorena formula A je zadovoljiva ako postoji interpretacija u kojoj jr A tačna . Formula A je zadovoljiva ako ima model. Formula A je nezadovoljiva ako ne postoji mode. Skup S zatvorenih formula je zadovoljiv ako je zadovoljiva konjunkcija svih formula iz S. Skup S je nezadovoljiv ako je nezadovoljiva konjunkcija svih formula iz S. Valjanost i nezadovoljivost su dualni: formula je valjana akko je njena negacija nezadovoljiva. Umesto dokazvanja valjanosti može se dokazivati nezadovoljivost negacije date formule. Metode dokazivanja nezadovoljivosi datog skupa formula zovu se metode pobijanja(opovrgavanja). Iz egzistencije konačne procedure koja daje odgovor u slučaju kada je formula valjana, sledi egzistencija konačne procedure za utvrdjivanje da je negacija formule nezadovoljiva.