| Assigned: | October 7 |
| Due: | October 21 |
Propositional logic is an elementary form of logic that only uses true and false values. (You do not talk about numbers or anything else.)
A propositional variable is a variable that can only stand for true or false. Variables are written as letters such as P or Q here. A formula is an expression written using propositional variables and operators including the unary negation operator (written ! here) and binary operators or (written \/ here), and (written /\ here) and implication (written => here).
For example, (P \/ Q) => R is a formula. It says that, if either of P or Q are true then R is true.
The meanings of the operators are as follows.
!P is true if and only if P is false.
P /\ Q is true if and only if both P and Q are true.
P \/ Q is true if and only if at least one of P and Q is true.
P => Q is true if and only if (!P \/ Q) is true.
By convention ! has highest precedence, then /\, then \/, and => has lowest precedence. Use parentheses to override precedence.
A formula is valid if it is true for all values of the variables. For example, P => P is valid since it is true for both values true and false for P. Formula (P => (Q => P)) is also valid. It is true no matter which values (true or false) you choose for P and Q.
Use lists to represent formulas in Scheme. For a variable, use a symbol such as P or Q. For !A, use (not A). For (A /\ B), use (and A B). Forms (or A B) and (implies A B) finish out what you need. For example, formula (P => (Q => P)) is represented by list (implies P (implies Q P)).
A sequent has the form (L |- R) where L and R are lists of formulas. For example, (P, P => Q |- Q \/ P, Q) is a sequent with two formulas on the left-hand side of |- and two on the right-hand side.
Sequent (L |- R) means " if all of the formulas in list L are true then at least one of the formulas in list R is true." Equivalently, sequent (L |- R) is true if at least one of the formulas in list L is false or at least one of the formulas in list R is true.
An empty list on the left-hand side is thought of as automatically true. An empty list on the right-hand side is thought of as automatically false. So sequent ( |- R) is true only if at least one of the sequents in list R is true. Sequent (L |- ) is true if at least one of the formulas in list L is false.
A sequent is valid if it is true for all possible values of the variables. For example, sequent (P |- P, Q) is valid.
You can represent a sequent in Scheme as a pair of lists of formulas. For example, sequent (P \/ Q |- Q, P) is represented as list (((or P Q)) (Q P)). Generally, if L and R are lists of formulas then (L R) represents sequent (L |- R).
A sequent is basic if there is a formula that is on both the left-hand side and the right-hand side of the sequent. For example, sequent (Q, P |- P, R) is basic since formula P occurs on both sides. Sequent (P /\ Q, Q => R |- P /\ Q, Q) is also basic since it has formula P /\ Q on both sides.
Every basic sequent is valid. Suppose that formula A occurs on both sides. If all of the formulas on the left-hand side are true, then A must be true. Since A also occurs on the right-hand side, there is clearly at least one formula on the right (namely A) that is true.
There are some simple rules for proving that a sequent is valid. The first is, of course, the rule that every basic sequent is valid. Page 256 of the book shows a collection of eight rules for proving sequents valid, provided you have already proved other sequents valid. Problem 24.7 offers additional explanation.
Look at rule (\/R). It tells you that, if you have already proved that sequent (X, Y |- A, B, U, V) is valid, then you can conclude that sequent (X, Y |- A \/ B, U, V) is also valid.
The rules implicitly allow you to reorder the formulas on the right-hand side or on the left-hand side. So rule (\/R) also says that, if you have proved that sequent (X, Y |- A, U, B, V) is valid, then you can conclude that sequent (X, Y |- A \/ B, U, V) is also valid. It is just a matter or reordering the right-hand side to bring A and B together.
Sometimes, in order to prove that one sequent is valid, you need to prove two other sequents first. Look at rule (/\R), for example. It tells you that, if you have proved both (X, Y |- A, U, V) and (X, Y |- B, U, V) to be valid, then you can conclude that sequent (X, Y |- A /\ B, U, V) is also valid.
You can interpret the proof rules backwards. For example, rule (\/R) tells you, if you want to prove (X, Y |- A \/ B, U, V), then you should prove (X, Y |- A, B, U, V).
Similarly, rule (/\R) says that, if you want to prove (X, Y |- A /\ B, U, V) then you should prove both (X, Y |- A, U, V) and (X, Y |- B, U, V)
In a goal-directed proof, you keep a list of goals that you need to prove. Think of it as a todo-list. In order to finish, you need to prove all of the sequents in the goal list to be valid.
To do the proof, select the first goal. If it is basic, you can put it aside, since it is obviously valid. But if it is not basic, you will need to use one of the rules to prove it. Find a formula, either on the left or the right, that has an operator. (That is, it is not just a variable). There is a rule for proving that seqeuent that either asks you to prove one or two other sequents. Add that one sequent or two sequents to the goal list. Continue the process.
If you encounter a goal that is not basic that only has variables (no operators), then that sequent can never be proved. You conclude that you cannot prove this goal list.
For example, suppose that you want to prove sequent ( |- (P => (Q => P /\ Q))). You create goal list [( |- (P => (Q => P /\ Q)))]. Rule (=>R) says to replace the first goal by one new goal, (P |- Q => P /\ Q)), so the new goal list is [(P |- Q => P /\ Q))]. Using (=>R) again yields goal list [(P, Q |- P /\ Q)]. Rule (/\R) tells you to replace the first goal by two goals, and the new goal list is [(P, Q |- P), (P, Q |- Q)]. Both sequents in this goal list are basic. Removing them leaves you with an empty list of goals. When the goal list is empty, you are done.
The proof just done can be summarized by showing the sequence of goal lists that it goes through.
[( |- (P => (Q => P /\ Q)))] [(P |- Q => P /\ Q))] [(P, Q |- P /\ Q)] [(P, Q |- P), (P, Q |- Q)] [(P, Q |- Q)] []
Write a Scheme program that contains a function (valid? A) that takes a formula A as a parameter. It should return #t if A is a valid formula and #f if not. You run this using the Scheme top-level interaction, writing an expression to be evaluated. There is no need to write a function to read and write information.
Here is a suggestion for some functions to write.
(basic? S) returns #t if S is a basic sequent. You might find the Scheme function member convenient to use. (member x L) returns the suffix of L starting at the first occurrence of x, or returns #f if x does not occur in L.
(get-structured L) takes a list of formulas L and returns one of two things.
(remove A L) returns the result of removing the first occurrence of A from L.
(new-goals-left A L R) returns a list of (one or two) new goals needed to prove sequent (A, L |- R), where A is a non-variable formula and L and R are lists of formulas. (There will be four cases, depending on the main operator in A.)
(new-goals-right A L R) returns a list of (one or two) new goals needed to prove sequent (L |- A, R), where A is a non-variable formula and L and R are lists of formulas.
(new-goals S) takes a sequent S and returns one of the following.
(prove G) takes a list of goals G and returns #t if G can be proved valid, #f if not. (The difference between prove and valid? is that the parameter of prove is a list of sequents, where the parameter of valid? is just one formula.
Here are some cases.
(valid? A) is just a matter of running (prove G) where goal list G contains only one sequent, namely ( |- A).
Some information about Scheme is in the book. You can also consult the Scheme Report for a more definitive and complete source of information.
To use Scheme, you will find Dr. Scheme convenient. You have the following options.
Use Dr. Scheme under Linux in the lab. It is called drscheme. (Currently not available; hopefully installed soon.)
Dr. Scheme offers options for beginners. Do not use them. You need to set the language to full scheme, not the stripped down versions that are available. Use the menu to select the "Revised(5) report on Scheme" (R5RS) version.
Use Dr. Scheme in the Windows lab. You should be able to find it in the start menu under PLT Scheme.
Get Dr. Scheme for yourself. (It is part of a larger package called PLT Scheme.) You can get it from www.plt-scheme.org.
Please call your program logic.scm. Submit it using the following command on one of the Linux machines such as login.cs.ecu.edu.
~abrahamsonk/3675/bin/submit 4 logic.scmBe sure that your name is in your program.
If you run your prover on some small formulas you will probably find that it runs fairly quickly. It can run quickly on some larger formulas as well, even some with a lot of variables. But for some larger formulas it will take a long time.
Problems can be classified according to how much time their solutions take, as a function of the size of the input. A problem is said to be solvable in polynomial time if there is an integer k so that the problem has an algorithm that solves inputs of size n in time nk. For example, a problem that can be solved in time n2, where n is the size of the input, is certainly solvable in polynomial time.
There are other classifications of problems. The problem of telling whether a propositional formula is valid belongs to a class of problems called the CoNP-complete problems. It is conjectured (but not known) that no CoNP-complete problem can be solved in polynomial time. If the conjecture is true, then every algorithm to tell whether a propositional formula is valid takes time more than n1000, for example, for infinitely many formulas, where n is the size of the formula.
Determining whether the conjecture about CoNP-complete problems is right or wrong is one of the biggest unanswered questions in the theory of computing. It turns out that, if you show that the validity problem for propositional logic is not solvable in polynomial time, then you will have proved that every CoNP-complete problem cannot be solved in polynomial time. So the whole conjecture lies within the status of this one problem.