CENG Take Home Exam 2 Solution

INTRODUCTION

Wang’s Algorithm is used to prove theorems in propositional calculus. So, for example, it is possible to start with three promises

P ! Q;Q ! R;:R

and prove the proposition :P .

To begin proving a theorem with Wang’s algorithm, all premises are written on the left-hand side of an arrow that we may call the sequent arrow ()). Note that the sequent arrow is di erent then then implication arrow. The desired conclusion is written to the right of the sequent arrow. Thus we have:

P !Q;Q!R;:R):P

This string of symbols is is called a sequent. This particular sequent contains four top-level formulas; there are three on the left and on on the right (it contains more than four formulas if we count embedded ones such as the formula P in P ! Q.)
Successively, we apply transformations to the sequent that break it down into simpler ones.

The general form of a sequent is:

F1; : : : ; Fm ) Fm+1; : : : ; Fm+n

where each Fi is a formula. Intuitively, this sequent may be thought of as representing a larger formula,
F1 ^    ^ Fm ! Fm+1 _    _ Fm+n



Here are the transformation (R1 through R5) and termination (R6 and R7) rules:

R1 : If one of the top-level formulas of a sequent has the form :2, we may drop the negation and move 2 to the other side of the sequent arrow. Here 2 is any formula, e.g., (P _ :Q). If the negation is to the left of the sequent arrow, we call the transformation NOT on the left; otherwise it is NOT on the right.

R2 : If a top-level formula on the left of the arrow has the form 2 ^ 4, or on the right of the arrow has the form 2 _ 4, the connective may be replaced by a comma. The two forms of this rule are called AND on the left and OR on the right, respectively.

R3 : If a top-level formula on the left has the form 2 _ 4, we may replace the sequent with two new sequents, one having 2 substituted for the occurrence of 2 _ 4, and the other having 4 substituted. This is called splitting on the left or OR on the left.

R4 : If the form 2 ^ 4 occurs on the right, we may also split the sequent as in Rule R3. This is splitting on the right or AND on the right.

R5 : A formula (at any level) of the form 2 ! 4 may be replaced by :2 _ 4, thus eliminating the implication connective.

R6 : A sequent is considered proved if some top-level formula 2 occurs on both the left and right sides of the sequent arrow. Such a sequent is called an axiom. No further transformations are needed on this sequent, although there may remain other sequents to be proved. (The original sequent is not proved until all the sequents obtained from it have been proved.)

R7 : A sequent is proved invalid if all formulas in it are individual proposition symbols (i.e., no connectives), and no symbol occurs on both sides of the sequent arrow. If such a sequent is found, the algorithm terminates; the original conclusion does not follow logically from the premises.

Wang’s algorithm always converges on a solution to the given problem. Every application of a transformation makes some progress either by eliminating a connective and thus shortening a sequent (even though this may create a new sequent as in the case of R3), or by eliminating the connective \!". The order in which rules are applied has some bearing on the length of a proof or refutation, but not on the outcome itself.




We may now proceed with the proof for our example. We label the sequents generated, starting with S1 for the initial one.

Label
Sequent
Comment



S1:
P !Q; Q!R; :R):P
Initial sequent.
S2:
:P _Q; :Q_R; :R):P
Two applications of R5.
S3:
:P _Q; :Q_R):P; R
Rl.
S4:
:P; :Q_R):P; R
S4 and S5 are obtained from S3 with


R3. Note that S4 is an axiom since P


appears on both sides of the sequent ar-

Q; :Q_R):P; R
row at the top level.
S5:

The other sequent generated by the ap-

Q; :Q):P; R
plication of R3.
S6:

S6 and S7 are obtained from S5 using

Q; R):P; R
R3.
S7:

This is an axiom.
S8:
Q):P; R; Q
Obtained from S6 using R1.  S8 is an


axiom.  The original sequent is now


proved, since it has successfully been


transformed into a set of three axioms


with no unproved sequents left over.




PROBLEM

You are expected to write a program that reads a sequent from the input, in a single line. Then applying the Wang’s algorithms determines whether it is proved (valid) or disproved (proved invalid), and prints a T or F, respectively.

Any binary operation, namely !, _, ^ will always be given enclosed in parenthesis. This is not so for the unary pre x operator of negation ‘:’.
Here is the BNF representation for the input.

hsequenti
::=  hlhsi # hrhsi
hlhsi
::=
hformula listi j "
hrhsi
::=
hformula listi j "
hformula listi
::=
hformulai j hformulai , hformula listi
hformulai
::=
hletteri j - hformulai j ( hformulai hin xopi hformulai )
hin xopi
::=  & j | j >
hletteri
::=  A j B j : : : j Z

The semantic is:



Symbol
Meaning







-
:

|
_

&
^

>
!




Though the input will not contain whitespaces, you are free to make your implementation insen-sitive to blanks.

The above given example of:

P !Q; Q!R; :R):P

would be input as:

(P>Q),(Q>R),-R#-P

The expected output for this input would be:

T

SPECIFICATIONS

This is a string manipulation task. So, you are expected to do dynamic allocations for the modi ed strings (of course free the unused as well).

The maximum length of an input is 200 characters. There will be no erroneous input.

struct usage is not allowed. This is not a dynamic data structure task (wait till the3). Do not even think about randomized output generation (with a hope of a %50 hit). We
will inspect your code for this.




























 I wish everyone good health amid the Covid-19 Pandemic.