BZPEERReading, trust and collaboration for researchDiscover
Workspaces
Network
Opportunities
Account
Researcher profile
Predrag Janičić contributes to research discovery and scholarly infrastructure.
Trust snapshot
Actions
Research graph
Inspect adjacent work, topics, institutions and collaborators without jumping out to a separate graph page.
BZPEER is loading the nearby papers, people, topics and institutions for this page.
Published work
We report on a new, simple, modular, and flexible approach for automated generation of illustrations for (readable) synthetic geometry proofs. The underlying proofs are generated using the Larus automated prover for coherent logic, and corresponding illustrations are generated in the GCLC language. Animated illustrations are also supported.
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).
We describe our ongoing project of formalization of algebraic methods for geometry theorem proving (Wu's method and the Groebner bases method), their implementation and integration in educational tools. The project includes formal verification of the algebraic methods within Isabelle/HOL proof assistant and development of a new, open-source Java implementation of the algebraic methods. The project should fill-in some gaps still existing in this area (e.g., the lack of formal links between algebraic methods and synthetic geometry and the lack of self-contained implementations of algebraic methods suitable for integration with dynamic geometry tools) and should enable new applications of theorem proving in education.