Система Буцефал: комбинирование дедуктивных процедур и описание стратегий поиска доказательств (Запись № 204829)

Подробности
000 -МАРКЕР
контрольное поле 01488nam0a2200337 4500
001 - ИДЕНТИФИКАТОР ЗАПИСИ
контрольное поле RU\NLR\bibl\40402
005 - ИДЕНТИФИКАТОР ВЕРСИИ
контрольное поле 20260409074752.0
021 ## - НОМЕР ГОСУДАРСТВЕННОЙ РЕГИСТРАЦИИ
Код страны Российская Федерация
Номер 99-19537
Номер Листа государственной регистраци 952
035 ## - ДРУГИЕ СИСТЕМНЫЕ НОМЕРА
Идентификатор записи (NLR Aleph) 000039404
100 ## - ДАННЫЕ ОБЩЕЙ ОБРАБОТКИ
Данные общей обработки 19990728d1998 u y0rusy50 ca
101 0# - ЯЗЫК РЕСУРСА
Язык текста, звукозаписи и т.д. русский
Язык резюме английский
102 ## - СТРАНА ПУБЛИКАЦИИ ИЛИ ПРОИЗВОДСТВА
Страна публикации Российская Федерация
105 ## - ПОЛЕ КОДИРОВАННЫХ ДАННЫХ: ТЕКСТОВЫЕ МАТЕРИАЛЫ, МОНОГРАФИЧЕСКИЕ
Кодированные данные о монографическом текстовом документе y |||||||||
200 1# - ЗАГЛАВИЕ И СВЕДЕНИЯ ОБ ОТВЕТСТВЕННОСТИ
Основное заглавие Система Буцефал: комбинирование дедуктивных процедур и описание стратегий поиска доказательств
Параллельное заглавие System Butsephalas: defining proof-search strategies and combining deductive procedures
Первые сведения об ответственности А.Е.Рязанов
Язык параллельного заглавия английский
210 ## - ПУБЛИКАЦИЯ, РАСПРОСТРАНЕНИЕ И ДР.
Место издания, распространения и т.д. Новосибирск
Имя издателя, распространителя и т. д. ИСИ
Дата издания, распространения и т.д. 1998
215 ## - ФИЗИЧЕСКАЯ ХАРАКТЕРИСТИКА
Специфическое обозначение материала и объем 42 с.
Размеры 20
225 1# - СЕРИЯ
Основное заглавие серии Препринт
Сведения об ответственности Рос. акад. наук. Сиб. отд-ние, Ин-т систем информатики им. А.П.Ершова
Обозначение тома 50
300 ## - ОБЩИЕ ПРИМЕЧАНИЯ
Текст примечания Авт. также на англ.яз.: A.E.Ryazanov
300 ## - ОБЩИЕ ПРИМЕЧАНИЯ
Текст примечания Рез. на англ.яз.
320 ## - ПРИМЕЧАНИЯ О НАЛИЧИИ В ДОКУМЕНТЕ БИБЛИОГРАФИИ / УКАЗАТЕЛЯ
Текст примечания Библиогр.: с.42
510 0# - ПАРАЛЛЕЛЬНОЕ ЗАГЛАВИЕ
Параллельное заглавие System Butsephalas: defining proof-search strategies and combining deductive procedures
Язык заглавия английский
606 ## - НАИМЕНОВАНИЕ ТЕМЫ КАК ПРЕДМЕТ
Наименование темы Программы (компьют.)
Тематический подзаголовок Верификация
Идентификатор авторитетной/нормативной записи RU\NLR\auth\661327565
Системный номер авторитетной/нормативной записи 2209898
686 ## - ИНДЕКСЫ ДРУГИХ КЛАССИФИКАЦИЙ
Индекс З973.2-018-07
700 #1 - ИМЯ ЛИЦА - ПЕРВИЧНАЯ ОТВЕТСТВЕННОСТЬ
Начальный элемент ввода Рязанов
Часть имени, кроме начального элемента ввода А. Е.
Код отношения Автор
801 #0 - ИСТОЧНИК ЗАПИСИ
Страна Российская Федерация
Организация NLR
Дата составления 19990728
Правила каталогизации PSBO
801 #1 - ИСТОЧНИК ЗАПИСИ
Страна Российская Федерация
Организация NLR
Дата составления 19990728
852 ## - МЕСТОНАХОЖДЕНИЕ И ШИФР ХРАНЕНИЯ
Идентификатор организации NLR
Шифр хранения (Call Number) 99-4/5532
942 ## - ДОПОЛНИТЕЛЬНЫЕ ЭЛЕМЕНТЫ ЗАПИСИ (АБИС)
Тип экземпляра АБИС Книга
980 ## - КОЛЛЕКЦИЯ
Название коллекции Национальная библиография
Экземпляры
Тип экземпляра Дата поступления Библиотека постоянного хранения Библиотека текущего хранения Место хранения Шифр хранения Штрих-код Статус экземпляра
Книга 26.10.2013 РНБ (Московский) РНБ (Московский) Русский книжный фонд: издания с 1957 года 99-4/5532 39404-10