Prikladnoj logicheskij analiz

Logicheskij formalizm ispol'zuetsq w kachestwe instrumenta dlq formulirowki i resheniq soderzhatel'nyh zadach. Voznikaüschie pri ätom problemy analiziruütsq s logicheskih pozicij. V swqzi s ätim issleduütsq dwa podhoda: semanticheskij ¿ ustanowlenie wypolnimosti, i sintaxicheskij ¿ postroenie wywodow w sekwencial'nyh ischisleniqh. V chastnosti, opisywaütsq procedury ustanowleniq wypolnimosti logicheskih formul i dokazuemosti w sekwencial'nyh ischisleniqh, kotorye mogut ispol'zowat'sq pri awtomaticheskom poiske reshenij. S cel'ü unifikacii mehanizma poiska reshenij wwoditsq kanonicheskaq forma wywodow, pozwolqüschaq opredelit' regulqrnuü proceduru poiska. Dlq logicheskih formul opredelqetsq ih matrichnoe predstawlenie i operacii nad matricami, chto daet wozmozhnost' uwidet' suschestwennye swojstwa logicheskih formul, kotorye pri obychnom podhode ne proqwlqütsq. Vwodqtsq tak nazywaemye lokal'nye zadachi, obladaüschie prostymi procedurami ustanowleniq wypolnimosti i dokazuemosti.