Golf egzystencjalny

22

Matematyka ma wiele symboli. Niektórzy mogą powiedzieć zbyt wiele symboli. Zróbmy więc matematykę ze zdjęciami.

Zróbmy papier, z którego będziemy czerpać. Aby rozpocząć papier jest pusty, powiemy, że jest to odpowiednik lub .prawdatrue

Jeśli napiszemy na papierze inne rzeczy, one również będą prawdziwe.

Na przykład

P i Q

Wskazuje, że twierdzenia i są prawdziwe.QPQ

Powiedzmy teraz, że jeśli narysujemy okrąg wokół jakiegoś stwierdzenia, to stwierdzenie jest fałszywe. To logiczne nie.

Na przykład:

nie P i Q

Wskazuje, że jest fałszem, a jest prawdą.QPQ

Możemy nawet umieścić koło wokół wielu instrukcji podrzędnych:

nie (P i Q)

Ponieważ część wewnątrz koła zwykle czyta się jako , umieszczając wokół niego okrąg, oznacza to . Możemy nawet zagnieżdżać kręginie  ( P  i  Q )P and Qnot (P and Q)

nie (nie P i Q)

Odczytuje to jako .not ((not P) and Q)

Jeśli narysujemy okrąg, w którym nic nie ma, oznacza to lub . fałszfałszywe

Fałszywe

Ponieważ pusta przestrzeń była prawdziwa, negacja prawdy jest fałszywa.

Teraz za pomocą tej prostej metody wizualnej możemy właściwie przedstawić dowolne zdanie w logice zdań.

Dowody

Następnym krokiem po przedstawieniu oświadczeń jest możliwość ich udowodnienia. W przypadku dowodów mamy 4 różne reguły, których można użyć do przekształcenia wykresu. Zawsze zaczynamy od pustego arkusza, który jak wiemy jest pustą prawdą, a następnie używamy tych różnych reguł, aby przekształcić nasz pusty arkusz papieru w twierdzenie.

Naszą pierwszą zasadą wnioskowania jest wstawianie .

Wprowadzenie

Nazwę liczby negacji między pod wykresem a najwyższym poziomem nazywamy „głębią”. Wstawienie pozwala nam wprowadzić dowolne oświadczenie, które chcemy na dziwnej głębokości.

Oto przykład przeprowadzania wstawiania:

Przykład wstawiania

Tutaj wybraliśmy , ale równie dobrze moglibyśmy wybrać dowolne oświadczenie, które chcieliśmy.P.

Skasowanie

Następna reguła wnioskowania to Kasowanie . Erasure mówi nam, że jeśli mamy stwierdzenie, które jest na równej głębokości, możemy je całkowicie usunąć.

Oto przykład zastosowania kasowania:

Przykład skasowania

Tutaj usunęliśmy , ponieważ było zagnieżdżone poziomy. Nawet gdybyśmy tego chcieli, nie moglibyśmy usunąć ponieważ jest on zagnieżdżony na poziomie.2 P 1Q2)P.1

Podwójne cięcie

Podwójne cięcie jest równoważne. Co oznacza, że ​​w przeciwieństwie do poprzednich wniosków można go również odwrócić. Double Cut mówi nam, że możemy narysować dwa koła dookoła dowolnego pod-wykresu, a jeśli są dwa koła dookoła pod-wykresu, możemy je usunąć.

Oto przykład z Double Cut używany

Przykład podwójnego cięcia

Tutaj używamy Double Cut na .Q

Iteracja

Iteracja jest również równoważna. 1 Odwrotność nazywa się Deiteracją. Jeśli mamy instrukcję i wycięcie na tym samym poziomie, możemy skopiować to wyrażenie wewnątrz wycięcia.

Na przykład:

Przykład iteracji

Deiteration pozwala nam odwracać iteracji . Instrukcja może zostać usunięta przez Deiteration, jeśli istnieje jej kopia na wyższym poziomie.


Ten format przedstawienia i dowodu nie jest moim własnym wynalazkiem. Są one niewielką modyfikacją logiki schematycznej zwanej Alpha Existential Graphs . Jeśli chcesz przeczytać więcej na ten temat, nie ma mnóstwo literatury, ale powiązany artykuł to dobry początek.


Zadanie

Twoim zadaniem będzie udowodnienie następującego twierdzenia:

Łukasiewicz - Tarksi Axiom

To po przetłumaczeniu na tradycyjną symbolikę logiczną jest

((ZA(bZA))(((¬do(re¬mi))((do(refa))((mire)(mifa))))sol))(H.sol).

Znany również jako aksjomat Łukasiewicza-Tarskiego .

Może się to wydawać zaangażowane, ale wykresy egzystencjalne są bardzo wydajne, jeśli chodzi o długość dowodu. Wybrałem to twierdzenie, ponieważ uważam, że jest to odpowiednia długość dla zabawnej i wymagającej układanki. Jeśli masz problemy z tym jednym polecam próbuje niektóre bardziej podstawowe twierdzenia pierwszy się zawiesić system. Ich listę można znaleźć na dole postu.

To jest więc twój wynik będzie całkowitą liczbą kroków w twoim proofie od początku do końca. Celem jest zminimalizowanie twojego wyniku.

Format

Format tego wyzwania jest elastyczny można przesłać odpowiedź w dowolnym formacie, który jest wyraźnie czytelny, w tym ręcznie rysowane lub świadczonych formatach. Jednak dla jasności sugeruję następujący prosty format:

  • Reprezentujemy nacięcie w nawiasach, bez względu na to, co wycinamy, jest ono wstawiane do parens. Puste cięcie byłoby po prostu ()na przykład.

  • Reprezentujemy atomy tylko ich literami.

Przykładem jest tutaj instrukcja celu w tym formacie:

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

Ten format jest fajny, ponieważ jest czytelny zarówno dla ludzi, jak i dla maszyn, więc umieszczenie go w poście byłoby przyjemne.

L.ZAT.miX

Wypróbuj online!

Jeśli chodzi o twoją rzeczywistą pracę, zalecam ołówek i papier podczas ćwiczeń. Uważam, że tekst nie jest tak intuicyjny jak papier, jeśli chodzi o wykresy egzystencjalne.

Przykładowy dowód

W tym przykładowym dowodzie udowodnimy następujące twierdzenie:

Prawo przeciwwskazań

(ZAb)(¬b¬ZA)

Dowód:

Przykład dowodu 1

Ćwicz twierdzenia

Oto kilka prostych twierdzeń, których można użyć do ćwiczenia systemu:

Drugi aksjomat Łukasiewicza

Drugi aksjomat Łukasiewicza

Aksjomat Meredith

Aksjomat Meredith

1: Większość źródeł używa bardziej wyrafinowanej i wydajniejszej wersji Iteracji , ale dla uproszczenia tego wyzwania korzystam z tej wersji. Są funkcjonalnie równoważne.

Kreator pszenicy
źródło
Wydaje mi się, że to pytanie lepiej pasuje do zagadek
Conor O'Brien
4
@ ConorO'Brien Dlaczego? Zagadki dotyczą głównie odpowiadania, a nie optymalizacji. Odpowiedź na to pytanie jest bardzo łatwa, co czyni je głównie wyzwaniem golfowym.
Wheat Wizard
Zagadki mogą bardzo dotyczyć optymalizacji. Wydaje mi się, że to wyzwanie może znaleźć lepszy dom na zagadkę, ale to oczywiście tylko moja opinia
Conor O'Brien
4
@connorobrien proof-golf jest od dawna częścią tej społeczności i niech będzie długo.
Nathaniel
1
Oto strona z zabawnym interaktywnym apletem Flash o tego rodzaju wyrażeniach: markability.net
Woofmao

Odpowiedzi:

7

19 kroków

  1. (()) [podwójne cięcie]
  2. (AB()(((G)))) [wprowadzenie]
  3. (AB(A)(((G)))) [iteracja]
  4. (((AB(A)))(((G)))) [podwójne cięcie]
  5. (((AB(A))(((G))))(((G)))) [iteracja]
  6. (((AB(A))(((G))))((H(G)))) [wprowadzenie]
  7. (((AB(A))(((G)(()))))((H(G)))) [podwójne cięcie]
  8. (((AB(A))(((DE()(C)(F))(G))))((H(G)))) [wprowadzenie]
  9. (((AB(A))(((DE(C)(DE(C))(F))(G))))((H(G)))) [iteracja]
  10. (((AB(A))(((DE(CD(F))(DE(C))(F))(G))))((H(G)))) [iteracja]
  11. (((AB(A))(((E(CD(F))(DE(C))(F)((D)))(G))))((H(G)))) [podwójne cięcie]
  12. (((AB(A))(((E(CD(F))(DE(C))(E(D))(F))(G))))((H(G)))) [iteracja]
  13. (((AB(A))(((G)((CD(F))(DE(C))(E(D))((E(F)))))))((H(G)))) [podwójne cięcie]
  14. (((AB(A))(((G)((CD(F))(DE(C))(((E(D))((E(F)))))))))((H(G)))) [podwójne cięcie]
  15. (((AB(A))(((G)((C((D(F))))(DE(C))(((E(D))((E(F)))))))))((H(G)))) [podwójne cięcie]
  16. (((AB(A))(((G)((DE(C))(((C((D(F))))(((E(D))((E(F)))))))))))((H(G)))) [podwójne cięcie]
  17. (((AB(A))(((G)((D(C)((E)))(((C((D(F))))(((E(D))((E(F)))))))))))((H(G)))) [podwójne cięcie]
  18. (((AB(A))(((G)(((C)((D((E)))))(((C((D(F))))(((E(D))((E(F)))))))))))((H(G)))) [podwójne cięcie]
  19. (((A((B(A))))(((G)(((C)((D((E)))))(((C((D(F))))(((E(D))((E(F)))))))))))((H(G)))) [podwójne cięcie]

Przećwicz twierdzenia

Drugi aksjomat Łukasiewicza: 7 kroków

  1. (()) [podwójne cięcie]
  2. (A()(B)(C)) [wprowadzenie]
  3. (A(A(B))(B)(C)) [iteracja]
  4. (A(AB(C))(A(B))(C)) [iteracja]
  5. ((AB(C))(A(B))((A(C)))) [podwójne cięcie]
  6. ((AB(C))(((A(B))((A(C)))))) [podwójne cięcie]
  7. ((A((B(C))))(((A(B))((A(C)))))) [podwójne cięcie]

Aksjomat Meredith: 11 kroków

  1. (()) [podwójne cięcie]
  2. (()(D(A)(E))) [wprowadzenie]
  3. ((D(A)(E))((D(A)(E)))) [iteracja]
  4. ((D(A)(E))((D(A)(E(A))))) [iteracja]
  5. ((D(A)(E))(((E(A))((D(A)))))) [podwójne cięcie]
  6. (((E)((D(A))))(((E(A))((D(A)))))) [podwójne cięcie]
  7. (((E)((C)(D(A))))(((E(A))((D(A)))))) [wprowadzenie]
  8. (((E)((C)(D(A)(C))))(((E(A))((D(A)))))) [iteracja]
  9. (((E)((C)((A)(C)((D)))))(((E(A))((D(A)))))) [podwójne cięcie]
  10. (((E)((C)((A)(((C)((D)))))))(((E(A))((D(A)))))) [podwójne cięcie]
  11. (((E)((C)((A(B))(((C)((D)))))))(((E(A))((D(A)))))) [wprowadzenie]

Wyszukiwarka dowodów Haskell

(Myślałeś, że zrobię to ręcznie? :-P)

To tylko próbuje wstawić, wprowadzenie podwójnego cięcia i iteracji. Nadal możliwe jest pokonanie tych rozwiązań za pomocą skasowania, podwójnej eliminacji lub deiteracji.

{-# 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)
Anders Kaseorg
źródło
4

22 kroki

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

(((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))))


Kilka rzeczy, których nauczyłem się podczas układania tej układanki:

  • Zmniejsz przedstawioną reprezentację. Obejmuje to odwracanie podwójnych cięć i iteracji. Na przykład ten aksjomat redukuje się do (((AB(A))(((C)DE)(CD(F))(E(D))(E(F)))(G))H(G))po cofnięciu podwójnych cięć i (((AB(A))(()CDE(F)))H(G)))po odwróceniu iteracji.

  • Szukaj zbłąkanych atomów. Na przykład H jest używane jako zmienna fikcyjna, a zatem można go wstawić w dowolnym momencie.


Przećwicz rozwiązania twierdzeń:

Rozwiązanie drugiego aksjomatu Łukasiewicza: [8 kroków]

(())

(()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))))))

Rozwiązanie dla aksjomatu Meredith: [12 kroków]

(())

(()(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
źródło
Zaktualizowałem, aby uwzględnić moje pełne rozwiązanie. Zabawna łamigłówka! Daj mi znać, jak mogę poprawić swój post.
Logikable
Zasadniczo odpowiedzi tutaj nie są ukryte - przy założeniu, że czytanie odpowiedzi oznacza „spoiler” dla rozwiązania. Mamy też MathJax, który \$jako początek / koniec, który moim zdaniem znacznie ułatwi czytanie. Mam nadzieję, że miło
spędzasz
Zaktualizowałem liczbę używanych reguł (dowód pozostaje ten sam). Czy ktoś, kto jest dobry w formatowaniu, może pomóc poprawić moją odpowiedź?
Logikable