Automated Propositional Logic Solver using GPT-4 Generated C++ Code

        Below are all generated by CartGPT4.

        This project showcases an implementation of a backward chaining algorithm for propositional logic using C++ code entirely generated by the GPT-4 language model (including this summary). The solver processes a given knowledge base and a query, determining if the query follows from the knowledge base using logical inference. While acknowledging the presence of minor bugs, the project successfully passed 46 out of 50 test cases.

Details:

GPT-4 as a code generator:

        In this project, GPT-4 was employed to generate code for solving logic programming problems, specifically targeting backward chaining algorithms. The generated code demonstrated impressive performance, passing 46 out of 50 test cases. However, there were some bugs in the backward_chaining function, which were not resolved due to the limitations of the GPT-4 system.
        It's important to note that the project was constrained by GPT-4's usage limitations, which allowed only 25 questions per 3 hours, and the overall development timeframe of 3 days. These constraints may have contributed to the inability to fully debug and optimize the code.
        Numerous strategies can be employed when generating code using GPT-4. For instance, you can inquire about the necessary components to create the desired code. Additionally, you can request GPT-4 to only generate modified code, eliminating the need for constant "continue" prompts. It is also beneficial to ask GPT-4 to construct classes and functions incrementally, rather than requesting large-scale tasks right away. Providing test cases and highlighting potential bugs in certain functions can further assist GPT-4 in debugging the code.

Handling logical expressions:

        The GPT-4 generated code includes data structures and functions for working with logical expressions, such as Logic and Clause classes, conversion to CNF representation using the to_cnf function, and a parser for reading input sentences. A print_expression function allows for displaying logical expressions in a human-readable format.

Backward chaining algorithm:

        The core of the project is the GPT-4 generated backward chaining algorithm, implemented in the KB (Knowledge Base) class. The algorithm contains helper methods like is_variable, apply_substitution, unify, and unify_goal_with_clause. Despite minor bugs, the algorithm searches for a proof of the negation of the query by unifying it with clauses in the knowledge base and recursively applying the substitution to the remaining goals.