Deductive Synthesis of Numerical Simulation Programs from
Networks of Algebraic and Ordinary Differential Equations


Thomas Ellman and Takahiro Murata
Department of Computer Science
Hill Center for Mathematical Sciences
Rutgers University, Piscataway, New Jersey 08855
{ellman,murata}@cs.rutgers.edu


Presenter: Thomas Ellman


Computational science and engineering design can benefit from software
tools that facilitate construction of programs for simulating physical
systems.  Our research adapts the methodology of deductive program
synthesis to the problem of constructing numerical simulation
codes. We have focused on simulators that can be represented as second
order functional programs composed of numerical integration and root
extraction routines. Synthesis of second order programs might appear
to present a problem for deductive systems that operate in first order
logic.  Nevertheless, we have developed a system that uses first order
Horn logic to solve this problem.  Our system uses a representation in
which domain specific functions are encoded as lambda expressions.  It
includes a knowledge base of axioms defining term equality in the
lambda calculus. It also includes axioms defining the semantics of
numerical integration and root extraction routines.  Our system uses
depth bounded SLD resolution to construct proofs and synthesize
programs.  It has successfully constructed numerical simulators for
computational design of jet engine nozzles and sailing yachts, among
others.