Пакет: coq-theories (8.12.0-3 и другие) [debports]

[ Источник:  ]

интерактивное программное средство доказательства теорем логики высшего порядка (теории)

Coq — интерактивное программное средство доказательства теорем логики высшего порядка, которое позволяет разрабатывать компьютерные программы в соответствии с их формальной спецификацией. Оно создано с использованием Objective Caml и Camlp5.

Пакет предоставляет существующие теории, на которых могут основываться новые доказательства, включая теории арифметики и булевых значений.

Другие пакеты, относящиеся к coq-theories

• dep: coq-8.12.0+4.11.1

  виртуальный пакет, предоставляемый coq

• rec: coq (>= 8.0)

  интерактивное программное средство доказательства теорем для логики высшего порядка (интерактивная среда и компилятор)

Загрузка coq-theories

Загрузить для всех доступных архитектур

Архитектура	Версия	Размер пакета	В установленном виде	Файлы
alpha (неофициальный перенос)	8.12.0-3+b3	23 361,0 Кб	166 285,0 Кб	[список файлов]
hppa (неофициальный перенос)	8.12.0-3+b3	23 358,5 Кб	166 204,0 Кб	[список файлов]
ia64 (неофициальный перенос)	8.12.0-3+b3	23 359,0 Кб	166 286,0 Кб	[список файлов]
sh4 (неофициальный перенос)	8.12.0-3+b3	23 351,6 Кб	166 203,0 Кб	[список файлов]
sparc64 (неофициальный перенос)	8.12.0-3+b3	23 359,8 Кб	166 286,0 Кб	[список файлов]
x32 (неофициальный перенос)	8.12.0-3+b3	23 356,3 Кб	166 203,0 Кб	[список файлов]