Modern Symbolic AI and Automated Reasoning

(CIS 700 (a Special Topics course) at Syracuse U)

Note: parts of this syllabus are subject to change with adequate notice to students.

The goal of this course is to give students a broad survey of the research landscape in modern symbolic artificial intelligence and automated reasoning/deduction. The course will involve three programming projects and will conclude with a final lecture delivered by student groups and accompanying set of notes.

Grading

• 40% – Programming Projects
• 30% – Final project presentation and notes
• 20% – Lead a paper discussion
• 10% – Participation, Paper Discussion, and Course Notes
• +5% – Bonus Take-Home Midterm

Programming Projects (40%)

Programming projects may be done in groups of up to three. Projects may be done in any language, though the professor may provide starter code. Projects will be distributed via the course website.

Projects are due in class two weeks from their assignment date. There will be reasonable exceptions made in reasonable circumstances (e.g., big paper deadline): if you need more time please write me in advance and articulate when can complete the project, being mindful you cannot put it of indefinitely.

Group Lecture Presentation (30%)

In groups of 3-4 students (three groups for the whole class), you will study a new topic and you will prepare a lecture. Details on this will be announced at the end of the course, along with sample topics recommended by the instructor. Essentially, your group will read several papers in a state-of-the-art area and will assemble a presentation. Your presentation must be in the form of a lecture that spans at least 60 minutes, accounting for questions. You should include examples, exercises, and discussion–if you would like, you may assign at most one paper for the class to read and discuss as part of your lecture–but this paper discussion may not take up more than 30 minutes of your prepared lecture.

In Lieu of a final exam, you will turn a detailed set of notes on your topic, chronicling the related work you read and proving numerous examples along with example code.

Lead a Paper Discussion (20%)

You must lead at least one paper discussion–students are permitted to do this in pairs if they would like. For this paper discussion, you must bring slides or well-typed notes which give several examples that you could walk through, and you are responsible for ensuring you have enough to say about the paper so that we can fill a class full, although I will help. You must understand the paper to the best of your ability. If you do not understand it fully, dedicate time to reading it and clearly articulate your confusion when you present it–we will try to clear it up together.

Do not wait to start doing this–presenting is a key part of being a researcher, and one I want you to practice. I will not grade too harshly–think of this mostly as participation points, as long as you put forth good effort and lead a good discussion, I am happy to give you feedback you can use to improve.

Participation, Paper Discussion, and Course Notes (10%)

Each week we will have a Google Groups thread on the week’s material and paper we are reading. You are required to write at least one substantive response, in the form of either (a) a set of course notes for the week (in PDF form), providing at least one example (preferably two or more). Or (b) you may offer a detailed critique and commentary on a paper.

Essentially: you must make at least one substantive comment on the class Google Group each week. Be thoughtful and treat this as professional discourse, rigorously engaging with the ideas of the course. At the end of the course, I will make all notes public–if you would prefer I not use your name, please let me know.

I will grade your weekly participation / your comments as follows: 0%, .5%, or 1%. If you do not participate, I will assign you a 0. If you participate, but less than I intend to see / your commentary is not substantive enough, I will give you a .5%. I will give you a 1% if I think you are making satisfactory and susbtantive engagement with the course.

Bonus Take-Home Midterm (up to +5% bonus)

In mid-October, I (Kris) will be traveling. I will give a bonus take-home midterm, consisting of detailed questions based on papers from the class, along with open-ended problems for you to solve. You can earn at most 5% bonus in the course from this written midterm. I will be canceling class to allow you to work on the midterm that day.

Topics

The following is a nonexhaustive list of topics. Topics will follow papers and may change based on student interest or course direction.

• Classical and intuitionistic propositional logic
• Proof theory / natural deduction
• First-Order Logic
• SAT
• SMT
• DPLL
• CDCL
• Resolution-based theorem proving
• Equality saturation
• Higher-order logic
• Temporal logic
• Hyperproperties
• Integrity
• Security type systems
• Product programs
• Interactive theorem proving

Collaboration and the Honor Code

• Please do not cheat in the course.

• Collaboration is explicitly allowed on many assignments, except for where otherwise noted. All work that a student represents as their own must be completed by the student (with allowed help). Using ChatGPT is permissible–if you use it, you must describe how you used it and convince me you didn’t use it to generate junk.

Student Support

Syracuse University values diversity and inclusion; we are committed to a climate of mutual respect and full participation. There may be aspects of the instruction or design of this course that result in barriers to your inclusion and full participation in this course. I invite any student to meet with me to discuss strategies and/or accommodations (academic adjustments) that may be essential to your success and to collaborate with the Office of Disability Services (ODS) in this process.

If you would like to discuss disability-accommodations or register with ODS, please visit their website at http://disabilityservices.syr.edu. Please call (315) 443-4498 or email disabilityservices@syr.edu for more detailed information.

ODS is responsible for coordinating disability-related academic accommodations and will work with the student to develop an access plan. Since academic accommodations may require early planning and generally are not provided retroactively, please contact ODS as soon as possible to begin this process.

Student Mental Health

Mental health and overall well-being are significant predictors of academic success. As such it is essential that during your college experience you develop the skills and resources effectively to navigate stress, anxiety, depression and other mental health concerns. Please familiarize yourself with the range of resources the Barnes Center provides (https://ese.syr.edu/bewell) and seek out support for mental health concerns as needed. Counseling services are available 24/7, 365 days a year, at 315.443.8000.

Discrimination and Harassment

The University does not discriminate and prohibits harassment or discrimination related to any protected category including creed, ethnicity, citizenship, sexual orientation, national origin, sex, gender, pregnancy, disability, marital status, age, race, color, veteran status, military status, religion, sexual orientation, domestic violence status, genetic information, gender identity, gender expression or perceived gender.

Any complaint of discrimination or harassment related to any of these protected bases should be reported to Sheila Johnson-Willis, the Universitys Chief Equal Opportunity & Title IX Officer. She is responsible for coordinating compliance efforts under various laws including Titles VI, VII, IX and Section 504 of the Rehabilitation Act. She can be contacted at Equal Opportunity, Inclusion, and Resolution Services, 005 Steele Hall, Syracuse University, Syracuse, NY 13244-1120; by email: titleix@syr.edu; or by telephone: 315-443-0211.

If you notice any incidents of harassment or discrimination, however minor, please email me. You may wish to use an anonymous email service such as https://anonymousemail.me/. Please feel free to tell me as much as you feel comfortable. I am a mandatory Title IX reporter and must report incidents such as sexual harassment, relationship violence, stalking, etc…