KEMBAR78
Assignment 2 | PDF
Scribd
Upload
40 views2 pages

Assignment 2

This document describes Assignment 2 for the course CS F214 Logic in CS. The objective is to develop a tool that verifies whether a proof of a given sequent is valid or not, using 5 specific proof rules: premise, AND introduction/elimination, OR introduction, IMPLIES elimination, and MT. The input and output formats are defined. Documentation requirements include Doxygen code documentation and HTML documentation of the algorithm. The assignment must be done in groups of up to 4 students in C or C++, with a demo scheduled after submission.

Uploaded by

chatgpt
Copyright
© © All Rights Reserved
We take content rights seriously. If you suspect this is your content, claim it here.
Available Formats
Download as PDF, TXT or read online on Scribd
40 views2 pages

Assignment 2

This document describes Assignment 2 for the course CS F214 Logic in CS. The objective is to develop a tool that verifies whether a proof of a given sequent is valid or not, using 5 specific proof rules: premise, AND introduction/elimination, OR introduction, IMPLIES elimination, and MT. The input and output formats are defined. Documentation requirements include Doxygen code documentation and HTML documentation of the algorithm. The assignment must be done in groups of up to 4 students in C or C++, with a demo scheduled after submission.

Uploaded by

chatgpt
Copyright
© © All Rights Reserved
We take content rights seriously. If you suspect this is your content, claim it here.
Available Formats
Download as PDF, TXT or read online on Scribd
You are on page 1/ 2

CS F214

Logic in CS
BITS Pilani, Hyderabad Campus
Assignment -2
Due Date : 7th December 2022 (by Midnight)
Total Marks: 30 (weightage : 10%)

Objective:

We have already seen that there are different applications which requires a logical framework to check the
proof of natural deduction in Propositional Logic/ Predicate Logic such as Flip
(https://staff.washington.edu/jon/flip/www/). In the first assignment, you have taken the first step towards
storing a well-formed propositional logic formula in a parse tree and do simple operations such as
evaluation, traversal etc.

In this assignment you will take the next step to develop a tool for verifying whether a certain proof of a
given sequent is valid or not. In order to keep it simple, in this assignment we will allow only the usage of
the following proof rules:

1. Premise [2]
2. AND introduction/elimination [5]
3. OR introduction [5]
4. IMPLIES elimination [5]
5. MT [5]

Definitions:
<statement> ::= p | ¬p | ¬(<statement>) | (<statement> ∧ <statement>) | (<statement> ∨ <statement>) |
(<statement> → <statement>)
<rule> ::= ∧i | ∧e1 | ∧e2 | ∨i1 | ∨i2 | →e |P

Input:
First line:
n (number of statements)
Next n lines:
<statement>/<rule>[ /line1[ /line2 ] ] (parameter in [] is optional whose existence will be determined
by <rule>)

Output:
Valid Proof (or) Invalid Proof

Assumptions:
1. Line number starts from 1.
2. <statement> should be perfectly parenthesized, e.g. ((a ∧ b) ∧ c) is valid, (a ∧ b) ∧ c is invalid, ((a ∧
b)) is invalid, (a ∧ b) is valid, (a ∧ b ∧ c) is invalid, p is valid, (p) is invalid.
3. ¬ can be succeeded by a literal or ‘(‘ only.
Sample test case:

Input:
3
a/P
b/P
(a ∧ b)/∧i/1/2

Output: Valid Proof

Documentation:

You will produce the following documents:


1. Documentation of the code using Doxygen. [3]
2. Documentation of the algorithm for making this tool. Discuss about the algorithm for the tool,
code design, example outputs, plan to extend it so that other rules can also be implemented. This
documentation will be made as HTML pages. [5]

General Instructions:

1. This assignment will be done in groups of max four students. You should maintain to work with the
same group.
2. Code must be written in C or C++ only.
3. There will be only one submission per group on the CMS.
4. The name of the file should be id1_LOGIC_A2.zip, where id1 refers to the BITS ID of the sender.
5. You can discuss with your friends but refrain from copying the code and submitting. Also
please do not use code downloaded from internet. Such codes will receive 0 credits.
6. You have to demo the code to the instructor/TAs on a scheduled date and timing after submission. It
is important to attend the demo, as absence from demo will amount to no credit for the
assignment. The tentative date for the Demo will be right after the submissions.

You might also like