Математическая логика и теория алгоритмов. Для изучающих компьютерные науки

Описанную процедуру можно свести в следующую схему, представленную на Рис. 4.1. Теперь доказательство формулы (4.28) восстанавливается, если |- (А v(B&C)) (А vB)&(A vC) fвведение ^ (А v(B&C)) \- (А vB)&(A vC) удаление v ^удаление v А\-(А VB)&(A VC) В&С \- (А vB)&(A vC) введение & введение & А \-AvB А \-AvC В&С \-AvB В&С \-А^ \ \ введение v введение v / введение v /введение v В&С \-В В&С V с / / удаление & удаление & Рис. 4.1. проделать все рассуждения на приведенной схеме, начиная снизу. Для того, чтобы задать исчисление предикатов в виде естественного вывода, на заданные правила накладываются некоторые ограничения и добавляют еще примерно столько же новых правил вывода. Данное исчисление похоже на исчисление секвенций, но есть существенное различие. В натуральной дедукции есть правила введения и исключения, а в исчислении секвенций только правила исключения. Поэтому натуральная дедукция менее удобна для автоматизации доказательств, ибо здесь рассуждения, хотя и естественны для рассуждений, но менее унифицированы. В натуральной дедукции можно построить исчисление предикатов введя правила работы с кванторами, см., например, [34]. § 20. Приложения дедуктивных теорий Первая аксиоматическая (дедуктивная) теория была представлена Евклидом в его произведении «Начала». Эта работа являлась на протяжении 140