Cet ensemble de propositions peut-il être représenté et prouvé dans Haskell?

Question

J'ai utilisé un ensemble de déclarations de langage naturel et leur formalisation à partir de Gries et Schneider. J'ai tenté de transformer les propositions en équations de Haskell. Par exemple, pour S0: $ a land w rightarrow p $ La conjonction a été divisée $ a rightarrow p $ et $ w rightarrow p $ Et puis la règle contrapositive a été appliquée en donnant $ neg p rightarrow neg a $ et $ neg p rightarrow neg w $. J'ai ensuite traduit ces propositions en équations conditionnelles de Haskell.

La représentation de Haskell est-elle une transformation raisonnable? Y a-t-il une relation entre l'exécution de l'expression de Haskell not e Une preuve de théorème $ neg e $?

Langue naturelle

Si Superman était capable et disposé à empêcher le mal, il le ferait. Si Superman n'était pas en mesure d'empêcher le mal, il serait inefficace; S'il ne voulait pas empêcher le mal, il serait malveillant. Superman n'empêche pas le mal. Si Superman existe, il n'est ni inefficace ni malveillant. Par conséquent, Superman n'existe pas.

Formaliser

$ a $: Superman est capable d'empêcher le mal.

$ w $: Superman est prêt à empêcher le mal.

$ i $: Superman est inefficace.

$ m $: Superman est malveillant.

$ p $: Superman empêche le mal.

$ e $: Superman existe.

S0: $ a land w rightarrow p $

S1: $ ( neg a rightarrow i) land ( neg w rightarrow neg m) $

S2: $ neg p $

S3: $ e rightarrow neg i land neg m $

module SUPERMAN where
 a::Bool
 w::Bool
 i::Bool
 p::Bool
 e::Bool

 a | (not p) = False  -- S0a
 w | (not p)  = False -- S0b
 i | (not a) = True   -- S1a
 m | (not w) = True   -- S1b
 p = False            -- S2
 e | (i || m) = False -- S3
-- Theorems (not e), (i || m), and (i && a) all hold