Диссертация (1149226), страница 33
Текст из файла (страница 33)
Данные о количестве решенных задач с различнымрейтингом ILTP позволяют судить о степени сложности этих задач: чем вышерейтинг ILTP, тем меньше программ АЛВ для интуиционистской логикиспособны решить задачу.223Таблица Г.2. Сводные данные о решенных задачахПараметрЗадач решеноПроцент решенных задачДоказаноОпровергнутоЗадач решено за 0–1 секундуЗадач решено за 1–10 секундЗадач решено за 10–100 секундКоличество решенных задач с рейтингом ILTP, равным 0Количество решенных задач с рейтингом ILTP 0,01–0,33Количество решенных задач с рейтингом ILTP 0,33–0,67Количество решенных задач с рейтингом ILTP 0,68–1Значение81131,862119066059922079593416В таблице Г.3 приведено количество задач, решенных программойWhaleProver в разных доменах ILTP.Таблица Г.3.
Распределение решенных задач по доменам ILTPКод доменаILTPALGCOMGEJGEOGPJHALKRSLCLMGTNLPPUZSETSWCSWVSYJSYNTOPНазвание доменаАлгебраТеория алгоритмовГеометрия в аксиоматике Яна вон ПлатоГеометрияТеория группГомологическая алгебраПредставление знанийЛогические исчисленияТеория управленияОбработка естественного языкаГоловоломкиТеория множествСинтез ПОВерификация ПОРазнотипные задачи для интуиционистскихпрограмм АЛВРазнотипные задачиТопологияКоличестворешенных задач6311813191321764391791542092.