hi there,
Hope you're doing well.I am looking for someone who can help with answering some questions in a .ipynb notebook.
In this notebook, the basic code on how to check Logical Satisfiability and Entailment of a Propositional Logic knowledge base is already provided, and how to use this for modelling a game strategy for Schnapsen.
If there are any other questions, don't hesitate to contact me. I am looking forward to hear from you and thank you in advance.
__MACOSX/._schnapsen __MACOSX/schnapsen/._bots schnapsen/logicalagents.ipynb { "cells": [ { "cell_type": "markdown", "metadata": {}, "source": [ "# Intelligent Systems 2020: \n", "## Logical Agents\n", "\n", "\n", "### Learning objectives\n", "At the end of this exercise you should be able to work with logical agents on the Schnapsen platform\n", "\n", "1. Be able to apply a SAT solver to check for satisfiability and entailment (bots)\n", "2. Apply a SAT solver for build an knowledge-based agent for playing Schnapsen. \n", "3. Build own variants of a knowledge-based agent for Schnapsen. \n", "\n", "### Preliminaries\n", "\n", "In this worksheet we'll use Propositional Logic and a specific version of a Propositional Logic solver (SMT solver) to build a fully knowledge based agent playing Schnapsen. The idea is to represent the strategies humans apply to play the game and to apply logical reasoning to identify good, bad, safe or risky moves, whatever you wish to model. \n", "This kind of reasoning---setting up logical statements and proving unsatisfiability. \n", "\n", "First things first, let's deal with dependencies for using the kb bot, namely numpy and scipy. They should be installed fairly easily via \"pip install numpy\", \"pip install scipy\".\n", "\n", "\n", "### Practicalities\n", "\n", "Follow this Notebook step-by-step. \n", "\n", "Of course, you can do the exercises in any Programming Editor of your liking. But you do not have to. Feel free to simply write code in the Notebook. Please use your studentID+Assignment4.ipynb as the name of the Notebook. \n", "\n", "Note: unlike the courses dedicated to programming we will not evaluate the style of the programs. But we will, however, test your programs on other data that we provide, and your program should give the correct output to the test-data as well.\n", "\n", "As was mentioned, the assignment is graded as pass/fail. To pass you need to have either a full working code or an explanation of what you tried and what didn't work for the tasks that you were unable to complete (you can use multi-line comments or a text cell).\n", "\n", "## Initialising \n", "\n", "First, let us make sure the necessary packages are installed, and imported. Run the following code:" ] }, { "cell_type": "code", "execution_count": 1, "metadata": {}, "outputs": [], "source": [ "import sys\n", "from bots.kbbot.kb import KB, Boolean, Integer, Constant" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "## SAT solving and Entailment checking \n", "\n", "We will start with some exercises to use an existing SAT solver to check for satisfiability and entailment. " ] }, { "cell_type": "code", "execution_count": 2, "metadata": {}, "outputs": [], "source": [ "# Define our symbols\n", "A = Boolean('A')\n", "B = Boolean('B')\n", "C = Boolean('C')\n", "\n", "# Create a new knowledge base\n", "kb = KB()\n", "\n", "# Add clauses\n", "kb.add_clause(A, B, C)\n", "kb.add_clause(~A, B)\n", "kb.add_clause(~B, C)\n", "kb.add_clause(B, ~C)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "This file first defines the three boolean symbols we will use (A, B and C), creates an empty knowledge base, and then adds the four following clauses:\n", "> A or B or C \n", "> (not A) or B \n", "> (not B) or C \n", "> B or not C\n", "\n", "### Task 1\n", "Are there any models (assignments of values to these variables that make all clauses true)? Write down all the models of the knolwedge base in the following cell. " ] }, { "cell_type": "markdown", "metadata": {}, "source": [] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Now run the script and report the output in the cell after the code. Explain what it means. " ] }, { "cell_type": "code", "execution_count": 3, "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "{A: False, B: True, C: True}\n", "{A: True, B: True, C: True}\n", "True\n" ] } ], "source": [ "# Print all models of the knowledge base\n", "for model in kb.models():\n", " print(model)\n", "\n", "# Print out whether the KB is satisfiable (if there are no models, it is not satisfiable)\n", "print(kb.satisfiable())\n" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Now it is time to adapt your first knowledge-base, by adding stuff…. \n", "\n", "## Tasks 2: \n", "Add a clause to the knowledge base to that it becomes unsatisfiable. Report the line of code you added, and in a separate line, the result that you get from the SAT solver and your script. " ] }, { "cell_type": "raw", "metadata": {}, "source": [] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Now you can already to build your own knowledge base, and do reasoning/inferencing with it. For example, check satisfiability of one of the questions of the working group automatically. \n" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### Task 3:\n", "Let KB be the knowledge base introduced in Exercise 7 of the Worksheet on Logical Agents: KB=\n", "> (P v Q) ^ (Q -> R) ^ (R -> -P) \n", "> -(P <-> - Q)\n", "\n", "Write a new version of the script above to prove or disprove whether KB is satisfiable or not. You can put both the knowledge base construction (you will have to translate the axioms into CNF by hand before adding them to the KB), the printing of the model and the satisfiability check in the next cell. \n" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### Task 4: \n", "Exercise 9 of this week's work session on logical agents contained the following knowledge base KB:\n", "\n", ">-A -> B \n", "> B -> A \n", "> A -> (C ^ D)\n", "\n", "Convert it to clause normal form, and write a script that creates this knowledge base as you did before. There are different subtasks: \n", "1) Print out its models and report them. \n", "2) As seen in the exercise, the knowledge base entails A ^ C ^ D. Explain in your own words what this says about the possible models for the knowledge base?\n", "\n" ] }, { "cell_type": "markdown", "metadata": {}, "source": [] }, { "cell_type": "markdown", "metadata": {}, "source": [ "In the previous question, you have shown that A ^ C ^ D is entailed by KB semantically (following the definition of entailment), where you used the prover to give you all the models. Now let us see whether you can actually prove entailment using the SAT solver directly