В чем разница между арифом и пребургером в Изабель?

Каждая цель, с которой я столкнулся в Isabelle до сих пор, которую можно было решить с помощью arith, также можно было решить с помощью presburger и наоборот, например.

lemma "odd (n::nat) ⟹ Suc (2 * (n div 2)) = n"
by presburger (* or arith *)

В чем разница между двумя решателями? Было бы неплохо привести примеры целей, которые может решить один, но не может решить другой.

Редактировать: мне удалось придумать лемму, доказанную arith, с которой presburger не может справиться. Похоже, это как-то связано с реальными числами:

lemma "max i (i + 1) > (i::nat)" by arith       -- ✔
lemma "max i (i + 1) > (i::nat)" by presburger  -- ✔

lemma "max i (i + 1) > (i::real)" by arith      -- ✔
lemma "max i (i + 1) > (i::real)" by presburger -- ✘

solver theorem-proving isabelle
person curiousleo    schedule 21.02.2015    source источник
comment
Я мало что знаю об этих пруверах, но похоже, что presburger не может работать с реальной арифметикой, а arith может. Я думаю, что presburger — это просто реализация хорошо известной процедуры принятия решений для арифметики Пресбургера, а arith — это набор различных процедур принятия решений для арифметики. Также есть linarith; Я не знаю, как это вписывается.   -  person Manuel Eberl    schedule 21.02.2015
comment
Спасибо, я даже не слышал о linarith раньше (есть ли где-нибудь исчерпывающий список методов Isabelle/HOL?)   -  person curiousleo    schedule 22.02.2015
comment
Разве lemma "(2 * i) div 2 = (i::real)" by presburger (что работает для меня) не является контрпримером к presburger, который не может справиться с реальной арифметикой?   -  person curiousleo    schedule 22.02.2015
comment
Ну, я не совсем уверен. Но если вы внимательно посмотрите на свою лемму, то увидите, что она нуждается в приведениях. Ваше утверждение в основном real (2 * i div 2) = real i, которое легко сокращается до 2 * i div 2 = i. Причина, по которой Изабель вставляет эти приведения, заключается в том, что div не определено для вещественных чисел, поэтому Изабель по умолчанию использует int и вставляет приведения, чтобы типы работали.   -  person Manuel Eberl    schedule 23.02.2015

Ответы (1)


arrow_upward
9
arrow_downward

Я только что спросил Тобиаса Нипкова, и вот что он мне сказал:

  • presburger – это процедура принятия решения для арифметики Пресбургера, то есть линейной арифметики натуральных и целых чисел, а также некоторых предварительная обработка, поэтому ваше утверждение с real также может быть доказано (поскольку оно сводится к проблеме с целыми числами). Он может обрабатывать квантификаторы. Алгоритм, лежащий в его основе, известен как алгоритм Купера.
  • linarith выполняет исключение Фурье-Моцкина для решения задач линейной арифметики на вещественных числа. Он также может доказать эти свойства на натуральных числах и целых числах, но только если они также верны для всех действительных чисел. Он не может обрабатывать квантификаторы.
  • arith можно охарактеризовать как комбинацию presburger и linarith.

Для полноты картины я хотел бы добавить, что существуют более специализированные методы доказательства для интересных классов утверждений:

  • algebra использует базы Грёбнера для решения задач, которые можно доказать, переставляя термины в алгебраических структурах, таких как группы и кольца.
  • approximate вычисляет вложения для конкретных терминов, используя интервальную арифметику
  • sos может доказывать многомерные полиномиальные неравенства, такие как (x :: real) ≥ 2 ⟹ y ≥ 2 ⟹ x + y ≤ x * y, используя сертификаты суммы квадратов
  • sturm, который был написан мной, может подсчитать количество действительных корней в заданном интервале и доказать некоторые одномерные действительные полиномиальные неравенства.
  • regexp может доказывать утверждения об отношениях, подобных (r ∪ s⁺)* = (r ∪ s)*, с помощью регулярных выражений.
person Manuel Eberl    schedule 23.02.2015