ISAIM 2016 will feature several special sessions:
- Boolean and pseudo-Boolean Functions
- Computational Approaches to Proof Construction
- Integrating Constraint Programming and Operations Research
The special session on Mathematical Theories of Natural Language Processing has been cancelled.
Boolean and pseudo-Boolean Functions
Organizers: Endre Boros and Yves Crama
Boolean and pseudo-Boolean functions are pervasive today in all areas of mathematics, computer science, operations research, various sciences and engineering. An ever increasing number and areas of applications demand new results from both structural and algorithmic points of views. The special sessions aim at bringing together researchers from all walks of science to discuss the latest results and the most important open problems.
Computational Approaches to Proof Construction
Organizer: Vijay Ganesh
In recent years there has been dramatic progress in the usability and power of interactive theorem provers (aka proof assistants), so much so that there is a sea change in the acceptance of these tools by mainstream mathematicians. For example, the Coq ahd HOL proof assistants are now being used by leading mathematicians to settle longstanding conjectures that have otherwise resisted solution by human effort alone (e.g., the Kepler conjecture). Furthermore, ideas developed in this context are now being applied to develop completely new foundations for mathematics, e.g., Homotopy Type Theory. This confluence of the power of proof assistants and their social acceptance is unique in the history of computer-aided reasoning tools, possibly heralding a new wave of research and application of proof assistants. This special session aims to showcase leading proof assistants, and new results obtained using them in recent years.
Integrating Constraint Programming and Operations Research
Organizer: John Hooker
Optimization methods from constraint programming (CP) and operations research (OR) have complementary strengths, as well as an underlying unity. Research over the last two decades has demonstrated how they can be profitably integrated, from both a modeling and a solution perspective. This session will cover the latest research and applications that combine ideas from CP and OR domains, including but not limited to integer and nonlinear programming, finite-domain and continuous constraint solving, continuous and global optimization, satisfiability algorithms and satisfiability modulo theories, dynamic programming and optimal control, decision diagrams and other graphical structures, local search and heuristic methods, and modeling languages.