Math 314 Logic Computer Lab IDr. HolmesFebruary 3, 20111 IntroductionIn these labs, you will use Marcel, a program written by me, to prove state-ments in propositional and quantifier logic. Marcel implements a style ofreasoning very similar to the style I have been describing in the notes (thereare minor differences which I will point out). Marcel will not prove yourtheorems for you, but it will not allow you to make mistakes: if you enterMarcel commands you will correctly execute proof strategies of the kind Iam teaching.In both the paper and computerized logical reasoning segments of thiscourse, I am also learning from you about how best to teach this kind ofmaterial. If you have ideas from your perspective about how things mightbe done better, they might be of interest to me: in particular, I have madeseveral changes to the software directly motivated by student experiences.The Lab I problems are due next Friday at midnight; you turn in yourwork by saving log files and emailing them to me. I am not writing paperhomework for this Friday; a paper assignment might appear next Monday orWednesday due the following Monday or Wednesday, though.2 Setting UpIf you want to install Marcel on your own computer, it is possible and I haveassisted students to do it. Not a few students have managed to do it on theirown. You need to install Moscow ML (there is a link on the Marcel page, towhich there is a link at the top of my web page), then put the Marcel sourcefiles in the right place relative to your Moscow ML installation. It is dead1easy to do this on Windows, not too bad on Linux, and it is possible on aMac (using the underlying Linux).Marcel is a program written in the computer language Standard ML, ofwhich Moscow ML is an implementation, and it runs in the Moscow MLinterpreter window.Setting up to do this on the MG104 machines involves the following steps.You are most welcome to try this before the lab on Friday and see if you canget set up, but we will be spending time on this in lab as well.open a terminal: Click the background and select Open Terminal.copy the Marcel source into your home directory: In the terminal win-dow type the following command:cp /home/public/holmes/marcel.sml .The standalone period at the end is not a typo! This copies the sourcefile for Marcel into your home directory.start the Moscow ML interpreter: Type mosml in your terminal win-dow. You should get messages on your screen about the Moscow MLversion and a new prompt (a hyphen).It is useful to be aware that everything you type in the Moscow MLwindow is a Moscow ML command. Be aware that a command alwaysends in a semicolon. If you hit return and you haven’t finished typinga command, you can continue typing it (for example, you can supply amissing semicolon). Exception: you cannot hit return in the middle ofa string. If you get into an ML error condition, just hit Ctrl-C – youwill interrupt out of the error condition, and your Marcel proof will notbe damaged.Everything in ML and Marcel is case sensitive: lowercase and uppercaseletters are always different.compile Marcel: You only need to do this the first time you use Marcel, orif I give you an updated version for some reason. This has been knownto happen; I have a hands-on approach to servicing software!At the hyphen prompt, typecompile "marcel.sml";2You will get lots of messages. When it quiets down it will have compiledMarcel.start Marcel: You will need to execute these ML commands to start Marcelevery time you use it.At the hyphen prompt, typeload "marcel"; open marcel;Notice that there are two commands here; you could issue them sepa-rately but you do have to issue them in that order.A lot of output follows these commands; you can ignore it.At this point you have the Marcel prover in front of you.3 Marcel NotationThe notation of Marcel is not the same as the notation we use in the notesor on the board. The problem is that we need to use ASCII symbols sincewe are in a text interface. The symbols used are fairly natural, though.propositional letters: These are of the form P1, P2, P3, and so forth.Other letters will not work. Lowercase p will not work.negation: What is usually written ¬P we will write ∼P1 in Marcel.conjunction: What is usually written P ∧ Q we will write P1 & P2 in Mar-cel.disjunction: What is usually written P ∨ Q is written P1 v P2 in Marcel.The symbol is a lowercase v.implication: What is usually written P → Q is written P1 -> P2 in Marcel.The implication arrow is a hyphen followed by a greater than sign.biconditional: What is usually written P ↔ Q is written P1 == P2 inMarcel.parentheses and order of operations: You can use parentheses to makesure your sentence has the correct structure. Marcel uses order ofoperations (the same as the ones I stated in class) and when it displays3a formula it does not show parentheses that are not needed. I wouldencourage you to put in as many parentheses as you think are needed.4 Marcel CommandsA Marcel command is actually a function in the ML programming language.A function with no inputs gets an input anyway (because Marcel insists): thecommand r for example just means “apply a proof strategy to the conclusionof the current argument” and needs no input, but when it is issued it gets adummy input (a pair of parentheses) so we typer();to issue this command (remember that an ML line always ends with asemicolon).Inputs to other Marcel commands are sometimes strings (all logical ex-pressions are treated as strings) which need to be enclosed in quotes, andsometimes integers, which are just entered as usual (without quotes).The very first command we show you is start or s, which takes a singlequoted logical expression as input and sets up the environment to prove thatexpression.- s "P1 -> P1";Line number 1:|-1: P1 -> P1> val it = () : unit-This is how the environment looks when we start proving the theorem P1-> P1. s "P1 -> P1"; is the command we entered; the rest is the computer’sresponse. The line > val it = () : unit you can ignore completely; it isjust ML interpreter chatter.4Each line of the proof shows us a statement we want to prove (our goal)below the symbol |- and a list of statements we are locally allowed to assume(use) above this symbol. Right now we have no assumptions at all.- r();Line number 2:1: P1|-1: P1I should mention that we are writing vertically a notation (called sequentnotation) which is usually written horizontally: the assumptions would nor-mally b e