Golfe Existencial

22

A matemática tem muitos símbolos. Alguns podem dizer muitos símbolos. Então, vamos fazer algumas contas com fotos.

Vamos ter um papel, no qual iremos desenhar. Para começar, o papel está vazio, diremos que é equivalente a ou .true

Se escrevermos outras coisas no papel, elas também serão verdadeiras.

Por exemplo

P e Q

Indica que as reivindicações e são verdadeiras.QPQ

Agora, digamos que, se desenharmos um círculo em torno de alguma afirmação, essa afirmação é falsa. Isso representa não lógico.

Por exemplo:

não P e Q

Indica que é falso e é verdadeiro.QPQ

Podemos até colocar o círculo em torno de várias sub-declarações:

não (P e Q)

Como a parte dentro do círculo costuma ser lida como , colocando um círculo ao redor, significa . Podemos até aninhar círculosnão  ( P  e  Q )P and Qnot (P and Q)

não (não P e Q)

É exibido como .not ((not P) and Q)

Se desenharmos um círculo sem nada, isso representa ou . falsofalse

Falso

Como o espaço vazio era verdadeiro, a negação do verdadeiro é falsa.

Agora, usando esse método visual simples, podemos realmente representar qualquer afirmação na lógica proposicional.

Provas

O próximo passo depois de poder representar declarações é poder prová-las. Para provas, temos 4 regras diferentes que podem ser usadas para transformar um gráfico. Começamos sempre com uma folha vazia que, como sabemos, é uma verdade vazia e, em seguida, usamos essas regras diferentes para transformar nossa folha de papel vazia em um teorema.

Nossa primeira regra de inferência é Inserção .

Inserção

Vamos chamar o número de negações entre um subgráfico e o nível superior de "profundidade". A inserção nos permite introduzir qualquer declaração que desejamos em uma profundidade ímpar.

Aqui está um exemplo de como realizamos a inserção:

Exemplo de inserção

P

Erasure

A próxima regra de inferência é Erasure . O apagamento nos diz que, se tivermos uma declaração em uma profundidade uniforme, podemos removê-la completamente.

Aqui está um exemplo de apagamento sendo aplicado:

Exemplo de apagamento

Q2P1

Double Cut

Double Cut é uma equivalência. O que significa que, diferentemente das inferências anteriores, ele também pode ser revertido. O Double Cut nos diz que podemos desenhar dois círculos em torno de qualquer subgrafo e, se houver dois círculos em torno de um subgrafo, podemos remover os dois.

Aqui está um exemplo do Double Cut sendo usado

Exemplo de corte duplo

Q

Iteração

A iteração também é uma equivalência. 1 O contrário é chamado Deiteração. Se temos uma declaração e um corte no mesmo nível, podemos copiá-la dentro de um corte.

Por exemplo:

Exemplo de Iteração

A deiteração nos permite reverter uma iteração . Uma instrução pode ser removida por meio da Deiteração se existir uma cópia dela no próximo nível.


Esse formato de representação e prova não é de minha própria invenção. Eles são uma pequena modificação de uma lógica diagramática, denominados Gráficos Existenciais Alfa . Se você quiser ler mais sobre isso, não há muita literatura, mas o artigo vinculado é um bom começo.


Tarefa

Sua tarefa será provar o seguinte teorema:

Łukasiewicz - Tarksi Axiom

Isso, quando traduzido para a simbolização lógica tradicional, é

((UMA(BUMA))(((¬C(D¬E))((C(DF))((ED)(EF))))G))(HG).

Também conhecido como Axioma Łukasiewicz-Tarski .

Pode parecer envolvido, mas os gráficos existenciais são muito eficientes no que diz respeito ao tamanho da prova. Selecionei esse teorema porque acho que é um comprimento apropriado para um quebra-cabeça divertido e desafiador. Se você está tendo problemas com este, eu recomendaria tentar alguns teoremas mais básicos primeiro para entender o sistema. Uma lista desses pode ser encontrada na parte inferior da postagem.

Isso é portanto sua pontuação será o número total de etapas da prova do início ao fim. O objetivo é minimizar sua pontuação.

Formato

O formato deste desafio é flexível. Você pode enviar respostas em qualquer formato claramente legível, incluindo formatos desenhados à mão ou renderizados. No entanto, para maior clareza, sugiro o seguinte formato simples:

  • Representamos um corte entre parênteses, o que quer que estejamos cortando é colocado dentro dos parênteses. O corte vazio seria apenas ()por exemplo.

  • Representamos átomos apenas com suas letras.

Como exemplo, aqui está a declaração de objetivo neste formato:

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

Esse formato é bom porque é legível por humanos e por máquinas, portanto, incluí-lo em sua postagem seria bom.

euUMATEX

Experimente online!

Quanto ao seu trabalho real, recomendo lápis e papel ao trabalhar. Acho que o texto não é tão intuitivo quanto o papel quando se trata de gráficos existenciais.

Prova de exemplo

Nesta prova de exemplo, provaremos o seguinte teorema:

Lei dos contra-positivos

(UMAB)(¬B¬UMA)

Prova:

Exemplo de Prova 1

Teoremas da Prática

Aqui estão alguns teoremas simples que você pode usar para praticar o sistema:

Segundo Axioma de Łukasiewicz

Segundo Axioma de Łukasiewicz

Axioma de Meredith

Axioma de Meredith

1: A maioria das fontes usa uma versão mais sofisticada e poderosa da iteração , mas, para manter esse desafio simples, estou usando esta versão. Eles são funcionalmente equivalentes.

Assistente de Trigo
fonte
Eu sinto que esta questão é mais adequada para intrigante #
Conor O'Brien
4
@ ConorO'Brien Por quê? O intrigante preocupa-se principalmente em responder, em vez de otimizar. Esta pergunta é muito fácil de responder, tornando-se principalmente um desafio no golfe.
Assistente de trigo
Intrigante pode se preocupar muito com a otimização. Eu sinto que este desafio pode encontrar uma casa melhor em intrigante, mas isso é, naturalmente, apenas minha opinião
Conor O'Brien
4
O @connorobrien proof-golf é uma parte estabelecida há muito tempo dessa comunidade e que pode continuar por muito tempo.
Nathaniel
1
Aqui está um site com uma divertida aplicação interativa em Flash sobre estes tipos de expressões: markability.net
Woofmao

Respostas:

7

19 passos

  1. (()) [corte duplo]
  2. (AB()(((G)))) [inserção]
  3. (AB(A)(((G)))) [iteração]
  4. (((AB(A)))(((G)))) [corte duplo]
  5. (((AB(A))(((G))))(((G)))) [iteração]
  6. (((AB(A))(((G))))((H(G)))) [inserção]
  7. (((AB(A))(((G)(()))))((H(G)))) [corte duplo]
  8. (((AB(A))(((DE()(C)(F))(G))))((H(G)))) [inserção]
  9. (((AB(A))(((DE(C)(DE(C))(F))(G))))((H(G)))) [iteração]
  10. (((AB(A))(((DE(CD(F))(DE(C))(F))(G))))((H(G)))) [iteração]
  11. (((AB(A))(((E(CD(F))(DE(C))(F)((D)))(G))))((H(G)))) [corte duplo]
  12. (((AB(A))(((E(CD(F))(DE(C))(E(D))(F))(G))))((H(G)))) [iteração]
  13. (((AB(A))(((G)((CD(F))(DE(C))(E(D))((E(F)))))))((H(G)))) [corte duplo]
  14. (((AB(A))(((G)((CD(F))(DE(C))(((E(D))((E(F)))))))))((H(G)))) [corte duplo]
  15. (((AB(A))(((G)((C((D(F))))(DE(C))(((E(D))((E(F)))))))))((H(G)))) [corte duplo]
  16. (((AB(A))(((G)((DE(C))(((C((D(F))))(((E(D))((E(F)))))))))))((H(G)))) [corte duplo]
  17. (((AB(A))(((G)((D(C)((E)))(((C((D(F))))(((E(D))((E(F)))))))))))((H(G)))) [corte duplo]
  18. (((AB(A))(((G)(((C)((D((E)))))(((C((D(F))))(((E(D))((E(F)))))))))))((H(G)))) [corte duplo]
  19. (((A((B(A))))(((G)(((C)((D((E)))))(((C((D(F))))(((E(D))((E(F)))))))))))((H(G)))) [corte duplo]

Teoremas da prática

Segundo axioma de Łukasiewicz: 7 passos

  1. (()) [corte duplo]
  2. (A()(B)(C)) [inserção]
  3. (A(A(B))(B)(C)) [iteração]
  4. (A(AB(C))(A(B))(C)) [iteração]
  5. ((AB(C))(A(B))((A(C)))) [corte duplo]
  6. ((AB(C))(((A(B))((A(C)))))) [corte duplo]
  7. ((A((B(C))))(((A(B))((A(C)))))) [corte duplo]

Axioma de Meredith: 11 passos

  1. (()) [corte duplo]
  2. (()(D(A)(E))) [inserção]
  3. ((D(A)(E))((D(A)(E)))) [iteração]
  4. ((D(A)(E))((D(A)(E(A))))) [iteração]
  5. ((D(A)(E))(((E(A))((D(A)))))) [corte duplo]
  6. (((E)((D(A))))(((E(A))((D(A)))))) [corte duplo]
  7. (((E)((C)(D(A))))(((E(A))((D(A)))))) [inserção]
  8. (((E)((C)(D(A)(C))))(((E(A))((D(A)))))) [iteração]
  9. (((E)((C)((A)(C)((D)))))(((E(A))((D(A)))))) [corte duplo]
  10. (((E)((C)((A)(((C)((D)))))))(((E(A))((D(A)))))) [corte duplo]
  11. (((E)((C)((A(B))(((C)((D)))))))(((E(A))((D(A)))))) [inserção]

Pesquisador à prova de Haskell

(O que você achou que eu faria isso manualmente? :-P)

Isso apenas tenta inserção, introdução de corte duplo e iteração. Portanto, ainda é possível que essas soluções possam ser vencidas usando apagamento, eliminação de corte duplo ou deiteração.

{-# 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
fonte
4

22 Passos

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

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


Algumas coisas que aprendi ao concluir este quebra-cabeça:

  • Reduza a representação fornecida. Isso envolve a reversão de cortes e iterações duplos. Por exemplo, esse axioma reduz para (((AB(A))(((C)DE)(CD(F))(E(D))(E(F)))(G))H(G))depois de reverter cortes duplos e (((AB(A))(()CDE(F)))H(G)))depois de reverter iterações.

  • Procure átomos dispersos. Por exemplo, H é usado como uma variável dummy e, portanto, pode ser inserido em qualquer ponto.


Soluções para Teoremas da Prática:

Solução para o segundo axioma de Łukasiewicz: [8 etapas]

(())

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

Solução para o axioma de Meredith: [12 etapas]

(())

(()(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
fonte
Atualizei para incluir minha solução completa. Quebra-cabeça divertido! Informe-me como posso melhorar minha postagem.
Logikable
Geralmente aqui as respostas não são ocultas - a suposição é que a leitura da resposta implica um "spoiler" para a solução. Também temos o MathJax aqui, usando \$como início / fim, o que acho que tornaria sua solução muito mais fácil de ler. Espero que você tenha um bom tempo aqui :)
FryAmTheEggman
Atualizei o número de regras usadas (a prova permanece a mesma). Alguém que é bom em formatação pode ajudar a melhorar minha resposta?
Logikable