CS 378 Assignment 5: Program Synthesis by Deduction
Due: April 8, 2021.
Files:
 navload.clj Function (navload) to load files
 cs378.clj CS 378 functions
 utmtrans.clj Functions for UTM translation
 navfns.clj Navigation functions
 unify.clj Unification and Backchaining
 nav.clj File with test cases for this assignment
 navresult.txt Example results
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 firstorder 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:
 xydata is a list (x y). The corresponding predicate is
cartesian:
(cartesian p q) means that q
is the Cartesian equivalent of p.
 rthdata is a list (r theta) where r is
a distance and theta is
in radians, measured counterclockwise from the x axis. The corresponding
predicate is polar: (polar p q) means that q
is the polar equivalent of p.
 rbdata is a list (range bearing) where
range is a distance and
bearing is in degrees, measured clockwise from north.
 dddata is a list (distance direction) where
direction is a compass direction such as n, s, e, w, ne, etc.
 latlong is a list (latitude longitude) where the values
are in floating degrees; negative longitude denotes west longitude.

UTM
or Universal Transverse Mercator is a way of representing
positions on Earth that locally maps locations to a flat, Cartesian xy grid.
UTM is a list (easting northing) where the values
are in meters. northing is meters north of the equator and
easting is meters east of the center of a sixdegree strip
of longitude, plus 500000.
 city is a symbol, such as austin.
Several operations and computations are defined:
 (distance a b d) means that d is the distance
between point a and point b.
 (bearing a b d) means that d is the bearing
from point a to point b.
 (rangebearing a b d) means that d is the
range and bearing from point a to point b.
 (movefrom a b c) means that point c is the result
of moving from point a by an amount b.
Usually you will make all the arguments of movefrom be constants
(functions of no arguments), e.g.,
(movefrom (a) (b) (zzz)) says that point (zzz) is the
result of moving from point (a) by an amount (b).
Most constants in the logic forms correspond to input variables in the
program.
A program is produced by the call:
(fnfor fn vars goal facts rules)
 fn is the name of the desired function.
 vars is a list of input variables.
 goal is a predicate stating the goal of the program.
 facts is a list of facts, such as input variable types.
 rules is the set of navigation rules, navr .
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 '( ((xydata (a))) ; type of input var a is xydata
((rthdata (b))) ; type of input var b is rthdata
))
(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.
 Examine the rules and code in navfns.clj and try
the examples test1 to test3 as shown in comments
in nav.clj .
 Fill in the stubs in the file nav.clj and turn in the
completed file, as descibed below.
 Make test4 to find the distance between two cities.
Use the program to find the distance (in meters) from
austin to dallas.
 Make test5 to find the distance between a rangebearing point
and a distancedirection point. Use the program to find the distance
between (10 60) and (12 ne).
 A trip starts at a city and travels a specified distancedirection.
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.
 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.
 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.