Простий пошук
Розширений пошук
Алфавітні покажчики

Бази даних

Реферативна база даних - результати пошуку

Віртуальна довідка
Тематичний інтернет-навігатор
Наукова електронна бібліотека
Автореферати дисертацій
Реферативна база даних
Книжкові видання та компакт-диски
Журнали та продовжувані видання
Mozilla Firefox Для швидкої роботи та реалізації всіх функціональних можливостей пошукової системи використовуйте браузер
"Mozilla Firefox"
Вид пошуку
Сортувати знайдені документи за:
авторомназвоюроком видання
Формат представлення знайдених документів:
повнийстислий
 Знайдено в інших БД:Книжкові видання та компакт-диски (1)
Пошуковий запит: (<.>A=Вершинин К$<.>)
Загальна кількість знайдених документів : 2
Представлено документи з 1 до 2
      
Категорія:    
1.

Вершинин К. П. 
Алгоритм Очевидности и обработка формализованных математических текстов / К. П. Вершинин, А. И. Дегтярев, А. В. Лялецкий, М. К. Мороховец, А. Ю. Паскевич // Пробл. упр. и информатики. - 2002. - № 5. - С. 80-95. - Библиогр.: 24 назв. - рус.

Описано результати сучасних досліджень, проведених за програмою автоматизації доведень теорем, ініційованою В. М. Глушковим у 1960-х рр. і названою "Алгоритм Очевидності". Представлено засоби мовної та дедуктивної підтримки даної програми.


Індекс рубрикатора НБУВ: В124

Рубрики:
 Теорія доведень. Пошук виведення і розв'язності в логіці 

Шифр НБУВ: Ж26990 Пошук видання у каталогах НБУВ 
      
Категорія:    
2.

Асельдеров З. М. 
Языковые проблемы автоматизации доказательств теорем в формализованных теориях / З. М. Асельдеров, О. В. Байкалова, А. В. Лялецкий, А. Ю. Паскевич, К. П. Вершинин, А. И. Молчановский // Искусств. интеллект. - 2004. - № 3. - С. 608-613. - Библиогр.: 10 назв. - рус.

Представлено стислий опис теперішнього стану системи автоматизації дедукції (САД), а також проблеми, з якими стикаються під час роботи з цією системою. Більш докладно розглянуто мовні проблеми. Система автоматизації дедукції грунтується на принципах евіденційної парадигми автоматизації математичної діяльності. На цій парадигмі базується програма "Алгоритм очевидності" (Evidence Algorithm). Система САД призначена для інтелектуальної обробки математичних текстів, такої, як автоматичне доведення теорем і верифікація текстів, записаних на ForTheL, формальній математичній мові, яка є наближеною до природної мови математичних публікацій. На сьогодні систему САД можна використовувати для встановлення вивідності секвенцій у класичній логіці першого порядку, пошуку доведень теорем у ForTheL-середовищі та верифікації замкнених ForTheL-текстів.


Індекс рубрикатора НБУВ: В124 + З970.624

Рубрики:
 Теорія доведень. Пошук виведення і розв'язності в логіці 
 Розпізнавання текстової інформації 

Шифр НБУВ: Ж15477 Пошук видання у каталогах НБУВ 
 

Всі права захищені © Національна бібліотека України імені В. І. Вернадського