Вопросы с тегом «model-theory»

38
Есть ли логика без индукции, которая захватывает большую часть P?

Теорема Иммермана-Варди утверждает, что PTIME (или P) - это именно тот класс языков, который может быть описан предложением логики первого порядка вместе с оператором с фиксированной точкой над классом упорядоченных структур. Оператор с фиксированной точкой может быть либо с наименьшей...

18
Можно ли проверить, является ли вычислимое число рациональным или целым?

Можно ли алгоритмически проверить, является ли вычисляемое число рациональным или целым? Другими словами, возможно ли для библиотеки, которая реализует вычислимые числа, предоставлять функции isIntegerили isRational? Я предполагаю, что это невозможно, и что это как-то связано с тем, что невозможно...

17
Неоднозначность и логика

В теории автоматов (конечных автоматов, автоматов с выталкиванием, ...) и в сложности существует понятие «неоднозначность». Автомат является неоднозначным, если существует слово по крайней мере, с двумя различными принимающими сериями. Машина является неоднозначной, если для каждого слова принятого...

17
Какое минимальное расширение FO охватывает класс регулярных языков?

Контекст: отношения между логикой и автоматами Теорема Бучи гласит, что монадическая логика второго порядка над строками (MSO) охватывает класс регулярных языков. Фактически доказательство показывает, что экзистенциальный MSO ( или EMSO ) над строками достаточен для захвата обычных языков. Это...

16
В какой степени математика Реалов может быть применена к вычислимым Реалам?

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

15
Поддержание порядка в списке в за раз

Задача обслуживания заказа (или «поддержание заказа в списке») заключается в поддержке операций: singleton: создает список с одним элементом, возвращает указатель на него insertAfter: дает указатель на элемент, вставляет новый элемент после него, возвращает указатель на новый элемент delete: дает...

15
Как показать, что тип в системе с зависимыми типами не заселен (то есть формула не доказуема)?

Для систем без зависимых типов, таких как система типов Хиндли-Милнера, типы соответствуют формулам интуиционистской логики. Там мы знаем, что ее модели являются гейтинговыми алгебрами, и, в частности, чтобы опровергнуть формулу, мы можем ограничиться одной гейтинговой алгеброй, где каждая формула...

11
Нахождение конечной модели

Я знаю, что вопрос «имеет ли формула первого порядка модель» вообще неразрешим.φϕ\phi Может ли кто-нибудь дать мне ссылку или книгу, которая даст ответ для конечных моделей. Если у меня есть формула первого порядка , можно ли имеет ли конечную модель? Я почти уверен, что вопрос хорошо известен, но...

9
Языки запросов к базе данных для эффективных запросов

Похоже, что в популярных языках запросов для реляционных баз данных можно создавать запросы, для ответа на которые потребуется много ресурсов. На практике администраторы базы данных управляют этим, ограничивая объем памяти на запрос и проверяя наличие длительных запросов на предмет замедления в...

9
FO-форма AC0 с некоторым предикатом

Мой вопрос касается теории конечных моделей / описательной сложности, поэтому будет означать «первый порядок по конечным двоичным словам с использованием предикатов Rs и унарного предиката P true в позиции 1 в слове».FO ( R )FО(р)FO(R) Я хотел бы знать, есть ли какая-либо характеристика с R любым...

9
Понимание логики с наименьшей фиксированной точкой

Чтобы лучше понять статью, я пытаюсь получить краткое представление о логике с наименьшей фиксированной точкой. Есть несколько моментов, в которых я застрял. Если G=(V,E)G=(V,E)G = (V,E) это график и Φ(P) = { ( a , b ) ∣G⊨E( а , б)∨P( а , б )∨∃z(E( а,z)∧P(z, б ) ) }Φ(п)знак...