The Coq mailing list

[Lawrence Paulson <lp15 AT cam.ac.uk>]

Special Issue—Journal of Automated Reasoning

NONLINEAR 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

http://www.andrew.cmu.edu/user/avigad/JAR_nonlinear.html
https://www.easychair.org/account/signin.cgi?conf=jarnonlinear