[Om-announce] Call for papers: Nonlinear Reasoning

Lawrence Paulson lp15 at cam.ac.uk
Sat Feb 1 16:39:47 CET 2014

Special Issue—Journal of Automated Reasoning


A variety of mature techniques for analyzing systems of linear inequalities have been imported to the domain of automated reasoning. In contrast, techniques for nonlinear functions are still being developed and examined. Nonlinear functions may include polynomials, transcendental functions, solutions to differential equations, and many other classes of functions. Symbolic and numerical methods, and combinations of the two, have been considered.

The goal of this special issue is to provide a snapshot of the state of the subject today and the most promising research directions. We welcome submissions that break new ground, as well as those that clarify and explain the central challenges. Examples of suitable topics:

	• refinements of classical nonlinear decision methods: cylindrical algebraic decomposition, virtual term substitution, Groebner bases, Wu's method
	• decision procedures for both extensions and fragments of the theory of real closed fields
	• applications of nonlinear reasoning techniques in mathematics and formal verification
	• numeric methods, such as interval constraint propagation and homotopy continuation
	• symbolic-numeric methods
	• heuristic reasoning methods
	• integration of nonlinear methods with resolution theorem provers, interactive theorem provers, SMT solvers
Papers (no longer than 30 pages) should be submitted via easychair.

Special issue editors: Jeremy Avigad (avigad at cmu.edu) and Lawrence C. Paulson (lp15 at cam.ac.uk)

Deadline for submissions: 1 March 2014


More information about the Om-announce mailing list