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

Content Provider	Springer Nature Link
Author	Ellman, Thomas Murata, Takahiro
Copyright Year	1998
Abstract	Scientists and engineers face recurring problems of constructing, testing and modifying numerical simulation programs. The process of coding and revising such simulators is extremely time-consuming, because they are almost always written in conventional programming languages. Scientists and engineers can therefore benefit from software that facilitates 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. We have developed a system that uses first order Horn logic to synthesize numerical simulators built from these components. Our approach is based on two ideas: first, we axiomatize only the relationship between integration and differentiation. We neither attempt nor require a complete axiomatization of mathematical analysis. Second, our system uses a representation in which functions are reified as objects. Function objects are encoded as lambda expressions. Our knowledge base includes an axiomatization of term equality in the lambda calculus. It also includes axioms defining the semantics of numerical integration and root extraction routines. We use depth bounded SLD resolution to construct proofs and synthesize programs. Our system has successfully constructed numerical simulators for computational design of jet engine nozzles and sailing yachts, among others. Our results demonstrate that deductive synthesis techniques can be used to construct numerical simulation programs for realistic applications.
Starting Page	291
Ending Page	319
Page Count	29
File Format	PDF
ISSN	09288910
Journal	Automated Software Engineering
Volume Number	5
Issue Number	3
e-ISSN	15737535
Language	English
Publisher	Kluwer Academic Publishers
Publisher Date	1998-01-01
Publisher Place	Boston
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	Software Engineering/Programming and Operating Systems Artificial Intelligence (incl. Robotics)
Content Type	Text
Resource Type	Article
Subject	Software

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Characteristic sets for ordinary differential equations

Symbolic-numerical solution of systems of linear ordinary differential equations with required accuracy

Exact linearization of nonlinear ordinary autonomous differential equations

Automated Procedure Construction for Deductive Synthesis

Region analysis for deductive verification of C programs

Formal Solutions of Linear Ordinary Differential Equations Containing m-Hypergeometric Series

Towards deductive verification of C programs with shared data

Automated Synthesis of Numerical Programs for Simulation of Rigid Mechanical Systems in Physics-Based Animation

Symbolic solution of nonhomogeneous linear ordinary differential equations in terms of power series

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

Similar Documents

Characteristic sets for ordinary differential equations

Symbolic-numerical solution of systems of linear ordinary differential equations with required accuracy

Exact linearization of nonlinear ordinary autonomous differential equations

Automated Procedure Construction for Deductive Synthesis

Region analysis for deductive verification of C programs

Formal Solutions of Linear Ordinary Differential Equations Containing m-Hypergeometric Series

Towards deductive verification of C programs with shared data

Automated Synthesis of Numerical Programs for Simulation of Rigid Mechanical Systems in Physics-Based Animation

Symbolic solution of nonhomogeneous linear ordinary differential equations in terms of power series

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