Janičić, Predrag
Automated Completion of Statements and Proofs in Synthetic Geometry: an Approach based on Constraint Solving
Gonzalez, Salwa Tabet, Janičić, Predrag, Narboux, Julien
Automated theorem provers take as input the formal statement of a conjecture in a theory described by axioms and lemmas, and try to generate a proof or a counter-example for this conjecture. In the field of geometry, several efficient automated theorem proving approaches have been developed, including algebraic ones such as Wu's method, Gröbner bases method, and semi-synthetic methods such as the area method. In these approaches, typically, the conjecture and the axioms being considered are fixed. However, in mathematical practice, in the context of education and also in mathematical research, the conjecturing and proving activities are not separated but interleaved. The practitioner may try to prove a statement which is valid only assuming some implicit or unknown assumptions, while the list of lemmas and theorem which can be used may not be complete.
Proceedings of the 13th International Conference on Automated Deduction in Geometry
Janičić, Predrag, Kovács, Zoltán
Automated Deduction in Geometry (ADG) is a forum to exchange ideas and views, to present research results and progress, and to demonstrate software tools at the intersection between geometry and automated deduction. Relevant topics include (but are not limited to): polynomial algebra, invariant and coordinate-free methods; probabilistic, synthetic, and logic approaches, techniques for automated geometric reasoning from discrete mathematics, combinatorics, and numerics; interactive theorem proving in geometry; symbolic and numeric methods for geometric computation, geometric constraint solving, automated generation/reasoning and manipulation with diagrams; design and implementation of geometry software, automated theorem provers, special-purpose tools, experimental studies; applications of ADG in mechanics, geometric modelling, CAGD/CAD, computer vision, robotics and education. Traditionally, the ADG conference is held every two years. The previous editions of ADG were held in Nanning in 2018, Strasbourg in 2016, Coimbra in 2014, Edinburgh in 2012, Munich in 2010, Shanghai in 2008, Pontevedra in 2006, Gainesville in 2004, Hagenberg in 2002, Zurich in 2000, Beijing in 1998, and Toulouse in 1996. The 13th edition of ADG was supposed to be held in 2020 in Hagenberg, Austria, but due to the COVID-19 pandemic, it was postponed for 2021, and held online (still hosted by RISC Institute, Hagenberg, Austria), September 15-17, 2021 (https://www.risc.jku.at/conferences/adg2021).