COSC-3450: Artificial Intelligence

Project 2
Spring 2024

Due: F 2/23 @ 5 PM ET
10 points

For this project, you will implement a resolution theorem prover for propositional logic.

I have divided the project into three phases:

1. For the first phase, write the classes and methods necessary to read, parse, store, and output propositional well-formed formulas (wffs). Formulas must be stored internally as expression trees.

   The following grammar specifies the syntax for wffs.

   formula ::= '(' proposition ')'
            | '(' 'not' formula-or-proposition ')'
            | '(' 'or' formula-or-proposition formula-or-proposition ')'
            | '(' 'and' formula-or-proposition formula-or-proposition ')'
            | '(' 'cond' formula-or-proposition formula-or-proposition ')'
   
   formula-or-proposition ::= formula | proposition
   
   proposition ::= letter letters-and-digits
   
   letters-and-digits ::= letter-or-digit letters-and-digits | \epsilon
   
   letter-or-digit ::= letter | digit
   
   letter ::= 'a'..'z' | 'A'..'Z'
   
   digit ::= '0'..'9'
   

   Examples of wffs written in this syntax are:

   • Wishes are horses provided that horses cannot fly.
   • \( \neg\mbox{HF} \rightarrow \mbox{W} \)
   • (cond (not hf) w)
   • If it is not the case that both beggars ride and wishes are nonequine, then horses can fly.
   • \( \neg (\mbox{BRD} \; \& \; \neg\mbox{W}) \rightarrow \mbox{HF} \)
   • (cond (not (and brd (not w))) hf)

   To support development, I put some starter code on cs-class. To get started, log on to cs-class and copy over the following zip file:

   cs-class-1% cd
   cs-class-1% cp ~maloofm/cosc3450/p2.zip ./
   cs-class-1% unzip p2.zip
   

   In the p2 directory, you will find a class implementation for Tokenizer and a partial implementation for Formula. The Tokenizer class demonstrates how to configure Scanner to tokenize propositional logic formulae based on our grammar. In Utils, there is a method that makes deep clones using serialization. You can see its use in Formula.clone(). Use Node to form the nodes of expression trees. Type defines the types for these nodes.

   The directory also contains files for the two proofs we discussed in lecture, Example 1 and the proof that beggars do not ride horses. As you can see in the files, comments begin with a forward slash, formulas begin with a left parenthesis, and both are confined to a single physical line. By convention, the last formula in the file is the conclusion.

   In addition to the these proofs, you must find two additional proofs from reputable sources consisting of at least three formulas and three propositions. Include these proof files with your submission to Autolab. Naturally, I will test your program on my own set of proofs.

   For this first phase, you must extend the partial implementation of the Formula class by implementing the methods

   • public void set( String s ), which constructs an expression tree from the specified string s
   • public String toString(), which returns a string representation of the expression tree

   When you submit to Autolab, the autograder will call these two methods along with the default constructor. Naturally, you will need to implement additional methods to convert strings into expression trees and vice versa.

2. For the second phase, implement the classes and routines to convert wffs to clausal form. A clause must be stored internally as expression trees or more precisely a linked list of literals. The following grammar specifies the syntax for clauses.

   clause ::= '{' literals '}'
   
   literals ::= literal literals-comma-separated | \epsilon
   
   literals-comma-separated ::= ',' literal literals-comma-separated | \epsilon
   
   literal ::= proposition
            | '(' 'not' proposition ')'
   

   You must implement

   • public void Formula.cnf(), which converts a formula to conjunctive normal form. (The prover does not use this method, but it is useful for development and testing.)
   • public class Clause, which is similar to Formula
   • public Clause()
   • public String Clause.toString(), which returns the string representation of a clause
   • public class Clauses, which must extend ArrayList<Clause>
   • public Clauses()
   • public Clauses Formula.getClauses(), which converts a formula to clausal form and returns the resulting clauses

   The transformations must preserve the order of literals. For example, (cond p q) should be written in CNF as ((not p) q), not as (q (not p)); (cond p q) should be written as the clause {(not p), q}, not as {q, (not p)}.

3. Finally, implement the routines required to conduct proofs using linear resolution. For this final phase, you must implement Main.java so it takes a file name as a command-line argument (e.g., java Main lecture.txt), reads the formulas in the file, negates the conclusion, converts the formulas to clauses, and conducts a proof using linear resolution. Main.main should print the formulas, the converted clauses, and a message indicating whether the conclusion follows from the premises.

   You must implement

   • public void Clause.set( String ), which sets the Clause to the clause that the specified String
   • public Clauses Clauses.resolve( Clause clause ), which resolves all of the clauses in Clauses with the Clause clause and returns them. If there are no resolvents, then resolve returns an empty clause.
   • public static boolean LinearResolution.prove( Clauses ), which returns true if prove derives the empty set from the set of clauses and returns false otherwise
   • public static boolean LinearResolution.prove( String filename ), which returns true if the conclusion follows from the premises and returns false otherwise
   • Note that these methods produce no output. Output for this project is limited to Main.main.

Use of AI tools for code generation, refinement, and debugging

OpenAI's terms of use for their systems including ChatGPT stipulate that users “must own their queries.” To me, this seems like a sound guiding principle for the use of large-language models for this class. The challenge is, you and I do not own much of course material. The material in the textbook is protected by copyright. From the preface:

Copyright © 2021, 2010, 2003 by Pearson Education, Inc. or its affiliates, 221 River Street, Hoboken, NJ 07030. All Rights Reserved. Manufactured in the United States of America. This publication is protected by copyright, and permission should be obtained from the publisher prior to any prohibited reproduction, storage in a retrieval system, or transmission in any form or by any means, electronic, mechanical, photocopying, recording, or otherwise. For information regarding permissions, request forms, and the appropriate contacts within the Pearson Education Global Rights and Permissions department, please visit www.pearsoned.com/permissions/

The algorithms in my lecture notes are based primarily on the textbook's. Consequently, they also are protected by the publisher's copyright. I have made my own modifications, but since they are minor modifications, the algorithms in my lecture notes are derivative works. It would be difficult for me to argue that they are new works. Crucially, I can not use these algorithms as queries to ChatGPT because it would violate OpenAI's terms of use, Georgetown's Acceptable Use Policy, and copyright law.

One could (try to) argue that we can submit information from the book to ChatGPT under the fair-use provision of the copyright law. In order for the fair-use provision to apply there must be a transformative use. What constitutes a transformative use is complex, and I am not a lawyer, but I am fairly certain that copying material from the textbook or my lecture notes and submitting it to ChatGPT is not a transformative use. Furthermore, OpenAI's stipulation that you “own” your queries stymies the argument that a query consisting of someone else's intellectual property is transformative. How much transformation would be required before their intellectual property becomes yours?

The textbook's authors are nice enough to distribute the algorithms for the book without a fee, but these algorithms are protected by copyright or by the Creative Commons Attribution 4.0 International License. While the so-called CC BY 4.0 is much less restrictive than the protections afforded by copyright law, it does not grant ownership. It is designed primarily to give credit to the originator through modifications and redistribution of the work.

Given all of this, I think the best way to proceed with using AI tools for the class assignments is to paraphrase. Rather than copying protected material such as an algorithm and then pasting it into an AI tool, you should learn how the algorithm works and then query the AI tool based on your understanding. For example, you can ask ChatGPT to generate an implementation of the A* algorithm in Java. ChatGPT and other large-language models were trained on all the algorithms and implementations that we are studying. You can use ChatGPT's implementation to help you understand the algorithm from class. You can use the algorithm from class to help you understand ChatGPT's implementation, including its possible flaws. With this understanding, you can use ChatGPT to refine its algorithm, or you can refine the implementation yourself.

Ultimately, I think you want to use your brain to devise queries based on your understanding of the material. This way the majority of the flow of information will be from ChatGPT to you and your project solution. While this may seem like a convoluted process, it should help you avoid break any rules.

Finally, as I said in class, this is new territory for me, and I am eager to learn from your experiences and perspectives. If you have other ideas for how to use AI tools for software development while navigating around the legal issues, it should make for an interesting class discussion.

Instructions for Electronic Submission

In accordance with the class policies and Georgetown's Honor System,
I certify that, with the exceptions of the class resources and those
items noted below, I have neither given nor received any assistance
on this project.

Name
NetID

When you are ready to submit your project for grading, put your source files, Makefile, proof files, transcript, and honor statement in a zip file named submit.zip. Upload the zip file to Autolab using the assignment p2. Make sure you remove all debugging output before submitting.

Plan B

Copyright © 2024 Mark Maloof. All Rights Reserved. This material may not be published, broadcast, rewritten, or redistributed.