*To*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*Subject*: [isabelle] CFP: Special Issue of the AMAI on the Formalization of Geometry, Automated and Interactive Geometric Reasoning*From*: Jacques Fleuriot <jdf at inf.ed.ac.uk>*Date*: Tue, 21 Feb 2017 21:08:43 +0000

Annals of Mathematics and Artificial Intelligence Special issue on Formalization of Geometry, Automated and Interactive Geometric Reasoning Geometry is a privileged field of investigation for various domains of computer science from image processing to geometric modeling via artificial intelligence in education and automated proof in geometry or semantic indexation of multimedia databases and so on. This special issue of AMAI is devoted to formal computational aspects of geometry. Formalizing geometry can be investigated in several different ways. At the beginning of the 1960s, the seminal work of Gelernter in the domain of automated proof was about synthetic geometry as taught in school. Then, in the late 1970s, a kind of revolution occurred with the work of Wu consisting in translating geometry into algebra and in using pseudo-division to perform proofs of a high-level theorem in both Euclidean and hyperbolic geometries. Subsequently, much work has been done continuing that geometry/algebra relation by considering other aspects of geometry, like differential geometry, distance geometry, discovering geometric theorems in figures with dynamic geometry software or from graphical figures, etc. Moreover, several researchers studied the foundations of geometry through various set of axioms; this way, the classical axiomatic approaches of Hilbert and Tarski have been formalized, as well as computational origami or incidence geometry. Outside the domain of automated proof, formalization of geometry is also encountered almost everywhere in geometric modeling --for instance with geometric constraint solving, declarative modeling or topological modeling-- and also in computational geometry or combinatorial geometry. Call-for-Papers For this special issue of AMAI, we are seeking original contributions on various aspects of formalization of geometry having in view computational applications mainly oriented to proof but also to modeling in geometry. Relevant topics include (but are not limited to): * Polynomial algebra, invariant and coordinate-free methods, probabilistic, synthetic, and logical approaches, techniques for automated geometric reasoning from discrete mathematics, combinatorics, and numerics; * Symbolic and numeric methods for geometric computation, geometric constraint solving, automated generation/reasoning and manipulation with diagrams; * Design and implementation of geometry software, special-purpose tools, automated theorem provers, experimental studies; * Applications of formalization of geometry to mechanics, geometric modeling, CAGD/CAD, computer vision, robotics, and education. Important dates: September 1, 2017: paper submission -- via website: www.editorialmanager.com/amai/ selecting issue: S688 Formalization of Geometry and Reasoning January 1, 2018: author notification March 1, 2018: revisions and camera-ready paper submission Guest Editors: Pascal Schreck <schreck at unistra.fr>, Tetsuo Ida <ida at cs.tsukuba.ac.jp>, Laura Kovacs <lkovacs at forsyte.tuwien.ac.at> -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.

- Previous by Date: Re: [isabelle] Code Generation with Locales that Fix Type Parameters
- Next by Date: Re: [isabelle] Standardized notation <# -> \<subset>#
- Previous by Thread: Re: [isabelle] Overlapping patterns in code export
- Next by Thread: [isabelle] Exception THM 0 raised (line 86 of tactic.ML)
- Cl-isabelle-users February 2017 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list