In this paper we present the proof system, called the valuation graphs system, which is a new version of two proof procedures: Davis-Putnam and Stålmarck. The novelty is that in the rules we note which propositional variable occurring in some propositional formula does not determine the logical value of that formula. Due to Stålmarck, we define a notion of proof width, corresponding to the width of structure of valuation graph which is a number of applications of dilemma rule. The dilemma rule considers two cases, so the time of proof grows up exponentially.
Ta witryna wykorzystuje pliki cookies do przechowywania informacji na Twoim komputerze. Pliki cookies stosujemy w celu świadczenia usług na najwyższym poziomie, w tym w sposób dostosowany do indywidualnych potrzeb. Korzystanie z witryny bez zmiany ustawień dotyczących cookies oznacza, że będą one zamieszczane w Twoim komputerze. W każdym momencie możesz dokonać zmiany ustawień dotyczących cookies
Informacja
SZANOWNI CZYTELNICY!
UPRZEJMIE INFORMUJEMY, ŻE BIBLIOTEKA FUNKCJONUJE W NASTĘPUJĄCYCH GODZINACH:
Wypożyczalnia i Czytelnia Główna: poniedziałek – piątek od 9.00 do 19.00