CSCE Programing Assignment #3 Solution

Overview

The goal of this project is to write a C++ program to do logical proofs using Natural Deduction. We will use Sammy’s Sport Shop as an example, with a target inference to prove by Natural Deduction. You will have to write the propositional knowledge base (KB) for this problem, using a syntax to be defined. Code will be provided for reading in KBs and parsing sentences. You will then need to write functions for various propositional rules of inference (e.g Implication Elimination, Modus Ponens, Resolution, DeMorgan’s Laws…). Finally, you will apply these inference steps to sentences from your KB to produce a derivation of the target inference for this problem.

Sammy’s Sport Shop

You are the proprietor of Sammy’s Sport Shop. You have just received a shipment of three boxes filled with tennis balls. One box contains only yellow tennis balls, one box contains only white tennis balls, and one contains both yellow and white tennis balls. You would like to stock the tennis balls in appropriate places on your shelves. Unfortunately, the boxes have been labeled incorrectly; the manufacturer tells you that you have exactly one box of each, but that each box is definitely labeled wrong. One ball is drawn from each box and its color observed. Given the initial (incorrect) labeling of the boxes above, and the three observations, use Propositional Logic to derive the correct labeling of the middle box.














Use propositional symbols in the following form: O1Y means a yellow ball was drawn (observed) from box 1, L1W means box 1 was initially labeled white, C1W means box 1 contains (only) white balls, and C1B means box 1 actually contains both types of tennis balls.

The initial facts describing this particular situation are: {O1Y, L1W, O2W, L2Y, O3Y, L3B}

    1. Using these propositional symbols, write a propositional knowledge base (sammys.kb) that captures the knowledge in this domain (i.e. implications of what different observations or labels mean, as well as constraints inherent in this problem, such as that all boxes have different contents). Do it in a complete and general way, writing down all the rules and constraints, not just the ones needed to make the specific inference about the middle box. Do not include derived knowledge that depends on the particular labeling of this instance shown above.

    2. Prove that box 2 must contain white balls (C2W) using Natural Deduction.
3/4/2021 4:50 PM


Format for KB Files

To represent propositional files, we will use a ASCII-based syntax called ‘symbolic expressions’. In this syntax, there are only symbols and parentheses (for representing hierarchical/nesting structure).

    • Symbols include any sequence of characters or digits (or some special chars, like ‘_’). For example, ‘A12B’, ‘leftTurn’, ‘3.1415’, ‘not’, and ‘implies’ are symbols. These can be atomic sentences (propositions) by themselves; operator names are also symbols.

    • Logical operators are represented as lists using prefix notation, that is, a sequence of symbols or sublists surrounded by parentheses, with the operator listed first. For example, ‘(and P Q)’, ‘(not X)’, and ‘(or (not X) (and P Q))’. While the unary ‘not’ operator always has only 1 argument, ‘and’ and ‘or’ operators may have an arbitrary number of arguments (not restricted to binary).

    • Implications are written similarly as lists using the ‘implies’ operator, such as
“(implies (and P Q) R)”, with 2 arguments: antecedent, followed by consequent.

    • Extra white space doesn’t matter; also, we will assume the parser is case-insensitive.

    • KB files can also have blank lines, and lines beginning with ‘#’ are assumed to be comments.

Examples:    (implies (and L M) P)

(or 2b (not 2b))


Expr Class – Parser for Logic Sentences


The internal representation for sentences is based on the Expr class (provided in Github via Proj3/parser.cpp and .hpp). There are actually 2 kinds of Expr objects: an ATOM (represented by the string ‘sym’), and a LIST, represented by a vector of sub-expressions (vector<Expr*>) called ‘sub’. This hierarchical data structure is intended to mimic the nested structure of the sentence syntax, but without the parentheses.

class Expr
{
public:
EXPR_TYPE kind; // either ATOM or LIST
string sym;
vector<Expr*> sub;
int end;

Expr(string s);

Expr(vector<string> tokens,int start); Expr(Expr* e); // deep copy

Expr(vector<Expr*> L); // create new COMPLEX expression from list string toString();

};
3/4/2021 4:50 PM


Instances of the Expr class are chimerical objects, depending on the value of ‘kind’:

    • If kind==ATOM, then string sym is defined, and vector sub is undefined

    • If kind==LIST, then vector sub is defined, and string sym is undefined

To make things easy, there is a parse() function provided for you, that takes a sentence as a string, constructs an Expr object for it, and returns a pointer to it. There is also a toString() method which serializes and Expr object back out to a string for printing. Here is an example snippet of C++ illustrating the use of the parser:

Expr* s1=parse(“(implies P Q)”);
Expr* s2=parse(“P”)
cout << s1->toString(); // output: (implies P Q)

Here is a visualization of the object structure created for “(implies (and P Q) R)”:















If anything goes wrong during parsing, the parser code will throw an exception. There are two custom types of errors, derived from the C++ runtime_error class: SyntaxError, and RuleApplicationError (defined in parser.hpp). You can throw the latter exception if you are trying to apply an ROI to expression for which it doesn’t apply (for example, trying to apply double-negation elimination to “(not P)”). In main, you should probably catch these exceptions and print out the message. Something like this…

int main()
{
try {
vector<Expr*> KB=load_KB();
do_inference(KB);
} catch (runtime_error& e) { cout << e.what() << endl; }
}


There is also an auxiliary function for reading in a whole KB file and returning a vector of Expr* objects:

vector<Expr*> load_kb(string fname);
3/4/2021 4:50 PM


Implementing Rules of Inference

Propositional Rules of Inference (ROI) can be implemented as functions that take 1 or 2 sentences (as Expr* objects), and return a new sentence (or possibly a list of sentences as vector<Expr*>). Using the examples above, here is how to doing Modus Ponens looks like:

Expr* s3=ModusPonens(s1,s2); // args: P->Q, and P
cout << s3->toString(); // output: Q

The way the ModusPonens() function would work is to check that the s2 expression matches the antecedents of the rule (by extracting the second element of the list for s1 and doing a hierarchical comparison via tree traversal with s2 to confirm they are identical, and then extracting the third complement of s1 and returning a copy of it.) This means you have to write some functions to check for equality of Expr objects and make copies.

Here are some other rules (ROI) you will have to implement:

    • ModusPonens

    • ImplicationElimination

    • AndElimination

    • AndIntroduction

    • OrIntroduction

    • DoubleNegationElimination – this is an easy one: “(not (not P))” -> P

    • Resolution – this requires both input expressions to be disjunctions (‘or’s)

    • DeMorgan’s Law(s) – 2 forms (‘not’ over ‘or’, ‘not’ over ‘and’)

    • anything else you might want or need that is a sound ROI…


For each ROI you implement, include a test function, like the one shown above for Modus Ponens.
3/4/2021 4:50 PM


Doing a Natural Deduction Proof

A Natural Deduction proof can be done by reading in an initial set of sentences (premises) and then applying a sequence of ROI to generate new sentences, until you generate the one you are looking for. Determining which steps to perform is (admittedly) a manual process. (We will implement an automated proof search in a subsequent project). Consider the example shown in 7.16a in the textbook.

    • P→Q

    • L^M→P

    • B^L→M

    • A^P→L

    • A^N→L

    • A

    • B

Q should be entailed by this KB.  Here is one way to derive it using Nat Ded in C++:

example.kb:
# example from textbook, sentences 0 through 6:
(implies P Q)

(implies (and L M) P)
(implies (and B L) M)
(implies (and A P) L)
(implies (and A B) L)
A
B

inference_example.cpp
vector<Expr*> KB=load_KB(“example.kb”); // parses and pushes sentences 0-6
KB.push_back(AndIntro(vector<Expr*>({KB[5],KB[6]})));
// 7.
(and A B)
KB.push_back(ModusPonens(KB[4],KB[7]));
// 8.
L
KB.push_back(AndIntro(vector<Expr*>({KB[6],KB[8]})));
// 9.
(and B L)
KB.push_back(ModusPonens(KB[2],KB[9]));
// 10.
M
KB.push_back(AndIntro(vector<Expr*>({KB[8],KB[10]})));
// 11.
(and L M)
KB.push_back(ModusPonens(KB[1],KB[11]));
// 12.
P
KB.push_back(ModusPonens(KB[0],KB[12]));
// 13.
Q

If you print the final KB, here is what it looks like:
    0. (implies P Q)
    1. (implies (and L M) P)
    2. (implies (and B L) M)
    3. (implies (and A P) L)
    4. (implies (and A B) L)
    5. A
    6. B
    7. (and A B)
    8. L
    9. (and B L)
    10. M
    11. (and L M)
    12. P
    13. Q
3/4/2021 4:50 PM



What to Turn In

Create a subdirectory in your (private) Github project for the class (on the TAMU Github server)

called ‘Proj3’.  In Proj3/, you should have at least the following files:

    • README – should explain how your program works (e.g. command-line arguments), and any important parameters or constraints

    • makefile – we must be able to compile your C++ code on compute.cs.tamu.edu by simply calling ‘make’

    • KB file: sammys.kb

    • C++ files:

    o NatDed.cpp: contains your implementations of the Rules of Inference, to be linked into the main program below

        o sammys.cpp – this should each have a function that does a Natural Deduction proof for the target sentence by applying a sequence of Rules of Inference, and print out the final KB at the end

    • transcripts: sammys.txt – show the final set of generated sentences


The date you commit your files and push them to the TAMU Github server will be used to determine when it is turned in and whether any late penalties will be applied.

Grading

The materials you turn in will be graded according to the following criteria:

    • 25% - does it compile and run without problems on compute.cs.tamu.edu?

    • 25% - does the implementation (code) look correct? (e.g. Rules of Inference)

    • 25% - does the knowledge base file look correct? (all the right rules?)

    • 25% - does the transcript look correct? (desired proof)