;; We assume that minlog, scheme and emacs is installed. Everything after ';;' are comments
;; Open this file using the minlog or emacs command.
;; (For more info see MINLOG-FOLDER/doc/tutor.pdf and for even more info MINLOG-FOLDER/doc/ref.pdf)
;; It is recommended to use two windows. If your window is not split then these may help:
;; Ctrl-x 2, or
;; Ctrl-x 3, to split your window
;; Ctrl-x o, to switch between windows
;; Ctrl-x b, (then type name of the buffer and enter) to change buffer, e.g. to *scheme* or ueb00.scm
;; For and emacs cheatsheet see e.g. https://www.gnu.org/software/emacs/refcards/pdf/refcard.pdf
;; your *scheme* buffer should look similar to this:
;; Chez Scheme Version 9.5
;; Copyright 1984-2017 Cisco Systems, Inc.
;;
;;
;; Minlog loaded successfully
;; If the *scheme* buffer does not exist then scheme is not running, do:
;; Alt-x, type
;; run-scheme, press enter
;; If run-scheme doesn't exist, you didn't install scheme properly.
;; you can evaluate commands by placing the cursor behind the closing parantheses and pressing Ctrl-x Ctlr-e
;; Evaluate this (pp for 'pretty print', pf for 'parse formula')
(pp (pf "Pvar"))
;; If this throws and error, then minlog is not loaded, in that case, eval:
(load "~/git/minlog/init.scm")
;; (your path to the init.scm might be different)
;; you can also mark a whole bunch of commands and eval them all by using Ctrl-c Ctrl-r:
;; Some Propositional Logic
;; we add some names for props (predicate variables with empty arity)
(add-pvar-name "A" "B" "C" (make-arity))
;; we can formulate some statements (the arrow is written -(minus)>(greater))
(pp (pf "A -> B"))
(pp (pf "(A -> B -> C) -> (A -> B) -> A -> C"))
;; we can prove some things ('set-goal' sets a new target to prove)
(set-goal "(A -> B -> C) -> (A -> B) -> A -> C")
;; -----------------------------------------------------------------------------
;; ?_1:(A -> B -> C) -> (A -> B) -> A -> C
;; Minlog tells you the current goal: ?_1:(A -> B -> C) -> (A -> B) -> A -> C
;; Proofs are backwards, we use 'assume' which corresponds to imp-intro
(assume 1)
(assume 2)
(assume 3)
;; you can undo the last n commands by '(undo n)'
(undo 3)
;; you can assume all things at once and also use proper names
(assume "u" "v" "w")
;; we need to prove '?_2:C'. We use the 'use' command which corresponds to imp-elim. We need to provide somethings which ends in the goal formula. The only thing is 'u:A -> B -> C'
(use "u")
;; u:A -> B -> C
;; v:A -> B
;; w:A
;; -----------------------------------------------------------------------------
;; ?_3:A
(use "w")
(use "v")
(use "w")
;; done
;; we can check proofs for correctness with the 'cdp' (check and display proof) command
(cdp)
;; we can display the proof as a lambda-term with the 'proof-to-expr-with-formulas' command
(proof-to-expr-with-formulas)
;; Falsity is written 'bot'
(set-goal "A -> (A -> bot) -> bot")
(assume "u" "v")
(use "v")
(use "u")
(proof-to-expr-with-formulas)
;; That was just an instance of imp-elim ...
(set-goal "A -> (A -> B) -> B")
(assume "u" "v")
(use-with "v" "u")
;; 'save' saves a proven theorem under the name given. Can 'use' it to prove other things
(save "ModusPonens")
(set-goal "A -> (A -> bot) -> bot")
(use "ModusPonens")
;; More examples
(set-goal "A -> B -> A")
(set-goal "(A -> B -> C) -> B -> A -> C")
(set-goal "(A -> B) -> (B -> C) -> A -> C")
;; andd is conjunction
(set-goal "(A -> B -> C) -> A andd B -> C")