Task 4 - EN - Monkey and banana

This exercise aims at knowledge representation, reasoning and planning in first-order logic. You will apply situation calculus in order to plan in a dynamic task in terms of first-order logical deductions.

Monkey-banana problem is a simple task in which a monkey is in a room. A banana hangs from the ceiling. The monkey stands just below the banana but it is beyond the monkey's reach. The monkey is able to walk, move and climb objects. The room is just the right height so that the monkey can move a box, climb it and grasp the banana. The goal is to generate this plan (i.e., a sequence of simple actions) automatically.

The problem will be solved in Prover9 system. Utilize the situation calculus formalism to resolve the following subtasks:

1. propose a simple and efficient solution disregarding the formal issues – axioms do not have to be general, assume that there is just one active agent (monkey) and one movable object available in a corner of the room (box), the plan will be as simple as outlined in the problem description (walk to the box, move the box below the banana, climb the box, grasp the banana),
2. improve and generalize the solution so that it can deal with more objects that can be movable or unmovable and climbable or unclimbable (a toilet can be climbed but cannot be moved, a picture can be moved but cannot be climbed), the objects will be at different places in the initial world (in the corner, near the window, at the door),
3. improve and generalize the solution so that it can deal with more active agents/animals, all the animals can walk, but some of them cannot move objects, others cannot climb objects (let us say that cats can climb but cannot move objects and dogs can move objects and cannot climb them), work with more agents at once, try to find general plans (is there any agent that can reach banana?) or plans for the individual agents (can the cat reach the banana?),
4. the generalized solution must implement frame axioms, do not forget that an agent cannot move an object while standing on it, the agent cannot even walk before climbing down, however, keep the world qualitative (do not consider features such as animal height in inches, object weight in pounds or friction forces),
5. the final solution should allow to easily add new agents, objects and change their properties, concern scalability of the proposed solution with respect to this parameters.

Monday 7.5.2018 23:59 CEST

Submit in the upload system, submit a zip file that contains three different solution files (keep the names mentioned below, do not use folders):

1. monkey_efficient.in … the efficient simple solution described in Assignment 1 above (monkey and the box only), exits with a proof when run,
2. monkey_formal.in … the formal solution described in Assignments 2-5, work with 2 animals (dog and cat) and 3 objects (one of them is both movable and climbable), exits with a proof when run,
3. monkey_formal_no_proof.in … nearly the same theory as in monkey_formal.in, only change the initial conditions (the dog stands on an object), the proof cannot be found this time.

Notes on efficiency and generality

• An efficient solution minimizes the number of predicates and maximizes the number of their arguments.
• On the contrary, a formal solution tries to decompose the problem, structure it and introduces explicit frame and effect axioms for particular predicates.
• In troubles, when not knowing what is wrong, try to decompose the problem and run simple goals leading to simple proofs.
• The theory could be considered sound and complete, if all the goals get answered correctly (not only the goals required in the assignment).
• It makes sense to submit an incomplete solution which does not tackle all the issues if there is a chance to obtain at least 5 points and pass the task.

10 point assignment, min 5 points needed to pass it.

Employ the concept of situation calculus, the solutions that ignore it cannot pass the threshold. The grading is as follows: 2 points for the simple solution, 5 points for principled use of situation calculus in the formal solution, 3 points for its complete coherence (the objects cannot copy, the complete set of frame axioms, etc.).

The existence of proofs themselves helps to evaluate the solutions but it is not directly graded. Do not try to reach them at any cost (intentional mistakes that make Prover9 exit as expected).