Skip to content

Instantly share code, notes, and snippets.

@hiredman

hiredman/gist:e9fd688cbf718529e06c

Created October 30, 2014 20:38
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save hiredman/e9fd688cbf718529e06c to your computer and use it in GitHub Desktop.
Save hiredman/e9fd688cbf718529e06c to your computer and use it in GitHub Desktop.
Download ZIP
Raw
gistfile1.el
(display-solutions
(run 10 (prove
'(¬ P)
'((⊃ (≡ L N) C)
(∨ (≡ L N) (⊃ P (¬ E)))
(⊃ (¬ E) C)
(¬ C))
nil)))
"
Proof 0:
(⊃ (mt (⊃ (≡ L N) C) (¬ C)) (¬ (≡ L N)))
(⊃ (ds (∨ (≡ L N) (⊃ P (¬ E))) (¬ (≡ L N))) (⊃ P (¬ E)))
(⊃ (hs (⊃ P (¬ E)) (⊃ (¬ E) C)) (⊃ P C))
(⊃ (mt (⊃ P C) (¬ C)) (¬ P))
Proof 1:
(⊃ (ds (∨ (≡ L N) (⊃ P (¬ E))) (¬ C)) (⊃ P (¬ E)))
(⊃ (hs (⊃ P (¬ E)) (⊃ (¬ E) C)) (⊃ P C))
(⊃ (mt (⊃ P C) (¬ C)) (¬ P))
Proof 2:
(⊃ (mt (⊃ (¬ E) C) (¬ C)) (¬ (¬ E)))
(⊃ (ds (∨ (≡ L N) (⊃ P (¬ E))) (¬ (¬ E))) (⊃ P (¬ E)))
(⊃ (mt (⊃ P (¬ E)) (¬ (¬ E))) (¬ P))
Proof 3:
(⊃ (mt (⊃ (¬ E) C) (¬ C)) (¬ (¬ E)))
(⊃ (ds (∨ (≡ L N) (⊃ P (¬ E))) (¬ (¬ E))) (⊃ P (¬ E)))
(⊃ (hs (⊃ P (¬ E)) (⊃ (¬ E) C)) (⊃ P C))
(⊃ (mt (⊃ P C) (¬ C)) (¬ P))
"
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment