Экзистенциальный Гольф

22

Математика имеет много символов. Некоторые могут сказать слишком много символов. Итак, давайте сделаем немного математики с картинками.

Давайте иметь бумагу, на которой мы будем рисовать. Для начала бумага пуста, мы скажем, что эквивалентно или true .true

Если мы напишем на бумаге другие вещи, они тоже будут правдой.

Например

P и Q

Указывает, что претензии и Q верны.PQ

Теперь давайте скажем, что если мы рисуем круг вокруг некоторого утверждения, то это утверждение является ложным. Это логично, что нет.

Например:

не P а Q

Указывает, что ложно, а Q верно.PQ

Мы даже можем поместить круг вокруг нескольких вложенных утверждений:

нет (P и Q)

P and Qnot (P and Q)

нет (не P и Q)

not ((not P) and Q)

false

Ложь

Так как пустое пространство было истиной, то отрицание истины ложно.

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

Доказательств

Следующим шагом после того, как вы сможете представлять заявления, будет возможность доказать их. Для доказательства у нас есть 4 различных правила, которые можно использовать для преобразования графа. Мы всегда начинаем с пустого листа, который, как мы знаем, является бессодержательной истиной, а затем используем эти разные правила, чтобы превратить наш пустой лист бумаги в теорему.

Наше первое правило вывода - вставка .

вставка

Мы будем называть количество отрицаний между подграфом и верхним уровнем «глубиной». Вставка позволяет нам вводить любое утверждение на любой глубине.

Вот пример того, как мы выполняем вставку:

Пример вставки

P

подчистка

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

Вот пример применения стирания:

Пример стирания

Q2P1

Двойной разрез

Double Cut - это эквивалентность. Это означает, что, в отличие от предыдущих выводов, его также можно изменить. Double Cut говорит нам, что мы можем нарисовать два круга вокруг любого подграфа, и если есть два круга вокруг подграфа, мы можем удалить их оба.

Вот пример Double Cut используется

Пример Double Cut

Q

итерация

Итерация также является эквивалентностью. 1 Обратное называется Deiteration. Если у нас есть оператор и разрез на одном уровне, мы можем скопировать этот оператор в разрез.

Например:

Пример итерации

Deiteration позволяет нам полностью изменить Итерацию . Выписка может быть удалена с помощью Deiteration, если на следующем уровне существует ее копия.


Этот формат представления и доказательства не является моим собственным изобретением. Они представляют собой незначительную модификацию схематической логики и называются альфа-экзистенциальными графами . Если вы хотите прочитать больше об этом, литературы не много, но ссылка на статью - хорошее начало.


задача

Ваша задача будет доказать следующую теорему:

Лукасевич - Аксиома Таркси

Это при переводе на традиционную логическую символику

((A(BA))(((¬C(D¬E))((C(DF))((ED)(EF))))G))(HG),

Также известен как аксиома Лукасевича-Тарского .

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

Это поэтому ваш счет будет общим количеством шагов в вашей проверке от начала до конца. Цель состоит в том, чтобы минимизировать ваш счет.

Формат

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

  • Мы представляем разрез с круглыми скобками, все, что мы режем, помещается в скобки. Пустой разрез будет просто ()для примера.

  • Мы представляем атомы только их буквами.

В качестве примера приведем формулировку цели в этом формате:

(((A((B(A))))(((((C)((D((E)))))(((C((D(F))))(((E(D))((E(F))))))))(G))))((H(G))))

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

LATEX

Попробуйте онлайн!

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

Пример доказательства

В этом примере доказательства мы докажем следующую теорему:

Закон противоположностей

(AB)(¬B¬A)

Доказательство:

Пример доказательства 1

Теоремы о практике

Вот несколько простых теорем, которые вы можете использовать для практики системы:

Лукасевич Вторая аксиома

Лукасевич Вторая аксиома

Аксиома Мередит

Аксиома Мередит

1: Большинство источников используют более сложную и мощную версию Итерации , но для упрощения этой задачи я использую эту версию. Они функционально эквивалентны.

Мастер пшеницы
источник
Я чувствую, что этот вопрос лучше подходит для головоломок
Конор О'Брайен
4
@ ConorO'Brien Почему? Пазл в основном касается ответов, а не оптимизации. На этот вопрос очень легко ответить, что делает его главным образом проблемой для игры в гольф.
Пшеничный волшебник
Недоумение может быть очень связано с оптимизацией. Я чувствую, что этот вызов может найти лучший дом для загадок, но это, конечно, только мое мнение
Конор О'Брайен
4
@connorobrien proof-golf является давней частью этого сообщества, и долго может продолжаться.
Натаниэль
1
Вот сайт с забавным интерактивным Flash-апплетом об этих видах выражений: markability.net
Woofmao

Ответы:

7

19 шагов

  1. (()) [двойной разрез]
  2. (AB()(((G)))) [Вставка]
  3. (AB(A)(((G)))) [Итерационный]
  4. (((AB(A)))(((G)))) [двойной разрез]
  5. (((AB(A))(((G))))(((G)))) [Итерационный]
  6. (((AB(A))(((G))))((H(G)))) [Вставка]
  7. (((AB(A))(((G)(()))))((H(G)))) [двойной разрез]
  8. (((AB(A))(((DE()(C)(F))(G))))((H(G)))) [Вставка]
  9. (((AB(A))(((DE(C)(DE(C))(F))(G))))((H(G)))) [Итерационный]
  10. (((AB(A))(((DE(CD(F))(DE(C))(F))(G))))((H(G)))) [Итерационный]
  11. (((AB(A))(((E(CD(F))(DE(C))(F)((D)))(G))))((H(G)))) [двойной разрез]
  12. (((AB(A))(((E(CD(F))(DE(C))(E(D))(F))(G))))((H(G)))) [Итерационный]
  13. (((AB(A))(((G)((CD(F))(DE(C))(E(D))((E(F)))))))((H(G)))) [двойной разрез]
  14. (((AB(A))(((G)((CD(F))(DE(C))(((E(D))((E(F)))))))))((H(G)))) [двойной разрез]
  15. (((AB(A))(((G)((C((D(F))))(DE(C))(((E(D))((E(F)))))))))((H(G)))) [двойной разрез]
  16. (((AB(A))(((G)((DE(C))(((C((D(F))))(((E(D))((E(F)))))))))))((H(G)))) [двойной разрез]
  17. (((AB(A))(((G)((D(C)((E)))(((C((D(F))))(((E(D))((E(F)))))))))))((H(G)))) [двойной разрез]
  18. (((AB(A))(((G)(((C)((D((E)))))(((C((D(F))))(((E(D))((E(F)))))))))))((H(G)))) [двойной разрез]
  19. (((A((B(A))))(((G)(((C)((D((E)))))(((C((D(F))))(((E(D))((E(F)))))))))))((H(G)))) [двойной разрез]

Практические теоремы

Вторая аксиома Лукасевича: 7 шагов

  1. (()) [двойной разрез]
  2. (A()(B)(C)) [Вставка]
  3. (A(A(B))(B)(C)) [Итерационный]
  4. (A(AB(C))(A(B))(C)) [Итерационный]
  5. ((AB(C))(A(B))((A(C)))) [двойной разрез]
  6. ((AB(C))(((A(B))((A(C)))))) [двойной разрез]
  7. ((A((B(C))))(((A(B))((A(C)))))) [двойной разрез]

Аксиома Мередит: 11 шагов

  1. (()) [двойной разрез]
  2. (()(D(A)(E))) [Вставка]
  3. ((D(A)(E))((D(A)(E)))) [Итерационный]
  4. ((D(A)(E))((D(A)(E(A))))) [Итерационный]
  5. ((D(A)(E))(((E(A))((D(A)))))) [двойной разрез]
  6. (((E)((D(A))))(((E(A))((D(A)))))) [двойной разрез]
  7. (((E)((C)(D(A))))(((E(A))((D(A)))))) [Вставка]
  8. (((E)((C)(D(A)(C))))(((E(A))((D(A)))))) [Итерационный]
  9. (((E)((C)((A)(C)((D)))))(((E(A))((D(A)))))) [двойной разрез]
  10. (((E)((C)((A)(((C)((D)))))))(((E(A))((D(A)))))) [двойной разрез]
  11. (((E)((C)((A(B))(((C)((D)))))))(((E(A))((D(A)))))) [Вставка]

Haskell поисковик

(Что, ты думал, что я собираюсь сделать это вручную? :-P)

Это только попытка вставки, двойного введения и итерации. Таким образом, все еще возможно, что эти решения могут быть побеждены, используя стирание, устранение двойного сокращения или deiteration.

{-# LANGUAGE ViewPatterns #-}

import Control.Applicative hiding (many)
import Data.Char
import Data.Function hiding ((&))
import qualified Data.Map as M
import Data.Maybe
import qualified Data.MultiSet as S
import qualified Data.PQueue.Prio.Min as Q
import System.IO
import Text.ParserCombinators.ReadP

type Var = Char

data Part
  = Var Var
  | Not Conj
  deriving (Eq, Ord)

instance Show Part where
  show (Var s) = [s]
  show (Not c) = "(" ++ show c ++ ")"

newtype Conj = Conj
  { parts :: S.MultiSet Part
  } deriving (Eq, Ord)

instance Show Conj where
  show (Conj (S.toAscList -> [])) = ""
  show (Conj (S.toAscList -> g:gs)) =
    show g ++ concat ["" ++ show g1 | g1 <- gs]

true :: Conj
true = Conj S.empty

not_ :: Conj -> Conj
not_ = Conj . S.singleton . Not

(&) :: Conj -> Conj -> Conj
Conj as & Conj bs = Conj (S.union as bs)

intersect :: Conj -> Conj -> Conj
intersect (Conj as) (Conj bs) = Conj (S.intersection as bs)

diff :: Conj -> Conj -> Conj
diff (Conj as) (Conj bs) = Conj (S.difference as bs)

splits :: Conj -> [(Conj, Conj)]
splits =
  S.foldOccur
    (\a o bcs ->
       [ (Conj (S.insertMany a o1 bs), Conj (S.insertMany a (o - o1) cs))
       | (Conj bs, Conj cs) <- bcs
       , o1 <- [0 .. o]
       ])
    [(true, true)] .
  parts

moves :: Bool -> Conj -> [(Conj, String)]
moves ev a =
  (do (b, c) <- splits a
      andMoves ev b c) ++
  (do (p, _) <- S.toOccurList (parts a)
      partMoves ev p (Conj (S.delete p (parts a))))

andMoves :: Bool -> Conj -> Conj -> [(Conj, String)]
andMoves ev a b = [(a, "insertion") | not ev]

partMoves :: Bool -> Part -> Conj -> [(Conj, String)]
partMoves ev (Not a) b =
  [(a1 & b, why) | (a1, why) <- notMoves ev a] ++
  [ (not_ (diff a d) & b, "iteration")
  | (d, _) <- splits (intersect a b)
  , d /= true
  ]
partMoves _ (Var _) _ = []

notMoves :: Bool -> Conj -> [(Conj, String)]
notMoves ev a =
  (case S.toList (parts a) of
     [Not b] -> [(b, "double cut")]
     _ -> []) ++
  [(not_ a1, why) | (a1, why) <- moves (not ev) a]

partSat :: Part -> Bool -> M.Map Var Bool -> [M.Map Var Bool]
partSat (Var var) b m =
  case M.lookup var m of
    Nothing -> [M.insert var b m]
    Just b1 -> [m | b1 == b]
partSat (Not c) b m = conjSat c (not b) m

conjSat :: Conj -> Bool -> M.Map Var Bool -> [M.Map Var Bool]
conjSat c False m = do
  (p, _) <- S.toOccurList (parts c)
  partSat p False m
conjSat c True m = S.foldOccur (\p _ -> (partSat p True =<<)) [m] (parts c)

readConj :: ReadP Conj
readConj = Conj . S.fromList <$> many readPart

readPart :: ReadP Part
readPart =
  Var <$> satisfy isAlphaNum <|> Not <$> (char '(' *> readConj <* char ')')

parse :: String -> Maybe Conj
parse s = listToMaybe [c | (c, "") <- readP_to_S readConj s]

partSize :: Part -> Int
partSize (Var _) = 1
partSize (Not c) = 1 + conjSize c

conjSize :: Conj -> Int
conjSize c = sum [partSize p * o | (p, o) <- S.toOccurList (parts c)]

data Pri = Pri
  { dist :: Int
  , size :: Int
  } deriving (Eq, Show)

instance Ord Pri where
  compare = compare `on` \(Pri d s) -> (s + d, d)

search ::
     Q.MinPQueue Pri (Conj, [(Conj, String)])
  -> M.Map Conj Int
  -> [[(Conj, String)]]
search (Q.minViewWithKey -> Nothing) _ = []
search (Q.minViewWithKey -> Just ((pri, (a, proof)), q)) m =
  [proof | a == true] ++
  uncurry search (foldr (addMove pri a proof) (q, m) (moves True a))

addMove ::
     Pri
  -> Conj
  -> [(Conj, String)]
  -> (Conj, String)
  -> (Q.MinPQueue Pri (Conj, [(Conj, String)]), M.Map Conj Int)
  -> (Q.MinPQueue Pri (Conj, [(Conj, String)]), M.Map Conj Int)
addMove pri b proof (a, why) (q, m) =
  case M.lookup a m of
    Just d
      | d <= d1 -> (q, m)
    _
      | null (conjSat a False M.empty) ->
        ( Q.insert (Pri d1 (conjSize a)) (a, (b, why) : proof) q
        , M.insert a d1 m)
    _ -> (q, m)
  where
    d1 = dist pri + 1

prove :: Conj -> [[(Conj, String)]]
prove c = search (Q.singleton (Pri 0 (conjSize c)) (c, [])) (M.singleton c 0)

printProof :: [(Conj, String)] -> IO ()
printProof proof = do
  mapM_
    (\(i, (a, why)) ->
       putStrLn (show i ++ ". `" ++ show a ++ "`  [" ++ why ++ "]"))
    (zip [1 ..] proof)
  putStrLn ""
  hFlush stdout

main :: IO ()
main = do
  Just theorem <- parse <$> getLine
  mapM_ printProof (prove theorem)
Андерс Касеорг
источник
4

22 шага

(((())(())))

(((AB())(CDE(F)()))H(G))

(((AB(A))(CDE(F)(CD(F)))(G))H(G))

(((A((B(A))))(((((C))DE(F)(C((D(F)))))(G))))((H(G))))

(((A((B(A))))(((((C)DE)DE(F)(C((D(F)))))(G))))((H(G))))

(((A((B(A))))(((((C)((D((E)))))((((((D))E(F)))(C((D(F)))))))(G))))((H(G))))

(((A((B(A))))(((((C)((D((E)))))((((((D)E)E(F)))(C((D(F)))))))(G))))((H(G))))

(((A((B(A))))(((((C)((D((E)))))((((((D)E)((E(F)))))(C((D(F)))))(G))))))((H(G))))


Несколько вещей, которые я узнал из этой головоломки:

  • Уменьшите предоставленное представление. Это включает в себя реверс двойных разрезов и итераций. Например, эта аксиома сводится к (((AB(A))(((C)DE)(CD(F))(E(D))(E(F)))(G))H(G))после реверсирования двойных резов и (((AB(A))(()CDE(F)))H(G)))после реверсирования итераций.

  • Ищите беспризорные атомы. Например, H используется в качестве фиктивной переменной и, следовательно, может быть вставлен в любую точку.


Практика Теорема Решения:

Решение для второй аксиомы Лукасевича: [8 шагов]

(())

(()AB(C))

((AB(C))AB(C))

((A((B(C))))A((B))(C))

((A((B(C))))A(A(B))(C))

((A((B(C))))(((A(B))((A(C))))))

Решение для аксиомы Мередит: [12 шагов]

(())

(()(A)D(E))

(((A)D(E))(A)D(E(A)))

(((((A)D))(E))(A)D(E(A)))

(((((A(B))D)(C))(E))(A)D(E(A)))

(((((A(B))(C)D)(C))(E))(A)D(E(A)))

(((((A(B))(((C)((D)))))(C))(E))(((((A)D))(E(A)))))

Logikable
источник
Я обновил, чтобы включить мое полное решение. Веселая головоломка! Пожалуйста, дайте мне знать, как я могу улучшить свой пост.
Logikable
Обычно здесь ответы не скрываются - предполагается, что чтение ответа подразумевает «спойлер» решения. Также у нас есть MathJax, использующий \$в качестве начала / конца, который, я думаю, сделает ваше решение намного проще для чтения. Я надеюсь, что вы хорошо
проведете
Я обновил количество используемых правил (доказательство осталось прежним). Может ли кто-нибудь, кто хорош в форматировании, помочь улучшить мой ответ?
Logikable