Proof generators use heuristics to guide the search for a proof of their input proposition. The most notable recent work in this area is OTTER [36]. OTTER uses resolution applied to first-order logic with equality. Operating in autonomous mode, OTTER decides reads the input (clauses/formulas) and decides on inference rules and strategies. This frequently fails to produce useful output, so the user is given the option of setting the initial conditions and strategies for proof. If OTTER fails to find a proof in a reasonable amount of time, the user can start over with different initial conditions and hope that it fares better. It is not capable of induction or higher order logic, which are required for proving theorems in other interesting domains.
An instance of a program generator being used in practice is NASA's Amphion project [32]. Amphion automatically produces fortran programs from problem specifications. It has been applied to numerical aerodynamical simulation, space shuttle flight planning and solar system kinematics. It is claimed that the time taken by users to develop a specification in Amphion is typically an order of magnitude less than it would to write and debug a program to perform the same tasks by traditional methods.
|
|
|