CS 378 Assignment 5: Program Synthesis by Deduction

Due: April 2, 2024.

Files:

The purpose of this assignment is to experiment with deductive synthesis of programs that consist of calls to subroutines from a library, similar to the programs synthesized by Amphion (Stickel et al.).

Axioms are written that describe what each library subroutine does. Programs are specified by stating a set of facts, such as the types of inputs, then stating the goal of the program. Proof of the goal results in a series of function calls that compute the goal from the inputs; the proof can then be converted into a program. Deduction converts the specification of what the program should do into a plan for how to do it; the axioms represent codified symbolic knowledge about the functions in the program library.

For this assignment, we will use as our deduction engine a backchaining prover for first-order logic written in Clojure. A set of axioms for a library of navigation programs is contained in the file unify.clj .

For our application domain, we will use the domain of navigation on a plane (including local areas on Earth), which can be considered to be a simpler version of the Amphion astronomical navigation domain. There are many different ways of specifying positions and movements on the plane; library subroutines are provided to convert representations, model movements, and calculate distances and directions. Deductive synthesis allows us to produce programs that work with a variety of data forms.

The data formats that we will use include:

Several operations and computations are defined:

A program is produced by the call:

(fnfor fn vars goal facts rules)
fnfor calls the backchaining prover to infer a method of achieving the goal, then converts the proof into a Clojure function and calls eval to define it.
(def nav1 '( ((xy-data (a)))    ; type of input var a is xy-data
             ((rth-data (b)))   ; type of input var b is rth-data
             ))

(fnfor 'test1 '(a b) '(distance (a) (b) z) nav1 navr)
                     ; distance from a to b is z
In this example, the types of two input variables of the program, (a) and (b), are declared as facts. In the logic notation, the input variables such as b are written using parentheses, i.e. (b), which represent constants (functions of no variables) in logic. The two input variables are treated as constants for the logic form since they are inputs. The goal declares that z is the result if z is the distance between input variables (a) and (b). Proving the goal by backchaining results in the predicate
(distance (a) (b) (euclidist (a) (rth2xy (b))))
This is converted into the function:
(defn test1 [a b] (euclidist a (rth2xy b)))
This function can now be used on data:
user=> (test1  '(10 10) (list 30 (/ Math/PI 6)))

16.74469341998643
Several example program specifications are shown in the file nav.clj . The file unify.clj has rules that describe what the navigation library functions do; these functions are in the files navfns.clj and utmtrans.clj .

Assignment:

The file navload.clj has the function (navload) to load the necessary files. Edit this function as needed for your files.

The file nav.clj contains stubs for each program specification; use the input variable names as shown in the stubs.

  1. Examine the rules and code in navfns.clj and try the examples test1 to test3 as shown in comments in nav.clj .
  2. Fill in the stubs in the file nav.clj and turn in the completed file.
  3. Make test4 to find the distance between two cities. Use the program to find the distance (in meters) from austin to dallas.
  4. Make test5 to find the distance between a range-bearing point and a distance-direction point. Use the program to find the distance between (10 60) and (12 ne).
  5. A trip starts at a city and travels a specified distance-direction. Find the bearing from the resulting position to another city: test6. Use the program to find the bearing to San Antonio after starting at Austin and traveling 70000 meters w.
  6. A helicopter starts at Austin and flies 80000 meters at bearing 20 to pick up a clue; then it flies 100000 meters nw and picks up a treasure. Find the range and bearing to take the treasure to Dallas. Make a program test7 for problems of this type, then use it to solve the problem.
  7. test8 should find the range and bearing from one city to another. Find the range and bearing from Austin to Waco and Austin to Dallas.