CS 378 Assignment 5: Program Synthesis by Deduction
Due: April 8, 2021.
- 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 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:
- xy-data is a list (x y). The corresponding predicate is
(cartesian p q) means that q
is the Cartesian equivalent of p.
- rth-data is a list (r theta) where r is
a distance and theta is
in radians, measured counter-clockwise from the x axis. The corresponding
predicate is polar: (polar p q) means that q
is the polar equivalent of p.
- rb-data is a list (range bearing) where
range is a distance and
bearing is in degrees, measured clockwise from north.
- dd-data is a list (distance direction) where
direction is a compass direction such as n, s, e, w, ne, etc.
- lat-long is a list (latitude longitude) where the values
are in floating degrees; negative longitude denotes west longitude.
or Universal Transverse Mercator is a way of representing
positions on Earth that locally maps locations to a flat, Cartesian x-y 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 six-degree 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.
- (range-bearing 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
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.
- 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 .
(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)))
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 .
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 range-bearing point
and a distance-direction point. Use the program to find the distance
between (10 60) and (12 ne).
- A trip starts at a city and travels a specified distance-direction.
Find the bearing from the resulting position to another city:
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.