The SymbolicData GEO records -- a public repository of geometry theorem proof schemes Formalized proof schemes are the starting point for testing, comparing, and benchmarking of different geometry theorem proving approaches and provers. To automatize such tests it is desirable to collect a common data base of proof schemes, and to develop tools to extract examples, prepare them for input to different provers, and run them “in bulk”. The main drawback so far of special collections, e.g., Chou’s collection with more than 500 examples of proof schemes, was their restricted availability and interoperability. We report about first experience with a generic proof schemes language, the GeoCode language, that was invented to store more than 300 proof schemes in a publicly available repository, and tools to prepare these generic proof schemes for input to different target provers. The work is part of the SymbolicData project.

References in zbMATH (referenced in 29 articles , 1 standard article )

Showing results 1 to 20 of 29.
Sorted by year (citations)

1 2 next

  1. Berčič, Katja; Vidali, Janoš: DiscreteZOO: a fingerprint database of discrete objects (2020)
  2. Decker, Wolfram; Eder, Christian; Levandovskyy, Viktor; Tiwari, Sharwan K.: Modular techniques for noncommutative Gröbner bases (2020)
  3. Levandovskyy, Viktor; Schönemann, Hans; Zeid, Karim Abou: \textscLetterplace-- a subsystem of \textscSingularfor computations with free algebras via letterplace embedding (2020)
  4. England, Matthew; Florescu, Dorian: Comparing machine learning models to choose the variable ordering for cylindrical algebraic decomposition (2019)
  5. Huang, Zongyan; England, Matthew; Wilson, David J.; Bridge, James; Davenport, James H.; Paulson, Lawrence C.: Using machine learning to improve cylindrical algebraic decomposition (2019)
  6. Kanwal, Shamsa; Pfister, Gerhard: Standard bases with special generators of the leading idea (2018)
  7. Giesbrecht, Mark; Heinle, Albert; Levandovskyy, Viktor: Factoring linear partial differential operators in (n) variables (2016)
  8. Gräbe, Hans-Gert: Semantic-aware fingerprints of symbolic research data (2016)
  9. Joswig, Michael; Mehner, Milan; Sechelmann, Stefan; Techter, Jan; Bobenko, Alexander I.: DGD Gallery: storage, sharing, and publication of digital research data (2016)
  10. Sperber, Wolfram: Mathematical research data and information services (2016)
  11. Heinle, Albert; Levandovskyy, Viktor: The \textscSDEvalbenchmarking toolkit (2015)
  12. Afzal, Deeba; Janjua, Faira Kanwal; Pfister, Gerhard; Steidel, Stefan: Solving via modular methods (2014)
  13. Chen, Xiaoyu: Representation and automated transformation of geometric statements (2014)
  14. Giesbrecht, Mark; Heinle, Albert; Levandovskyy, Viktor: Factoring linear differential operators in (n) variables (2014)
  15. Kredel, Heinz: Comprehensive Gröbner bases in a Java computer algebra system (2014)
  16. La Scala, Roberto; Levandovskyy, Viktor: Skew polynomial rings, Gröbner bases and the letterplace embedding of the free associative algebra. (2013)
  17. Levandovskyy, Viktor; Studzinski, Grischa; Schnitzler, Benjamin: Enhanced computations of Gröbner bases in free algebras as a new application of the letterplace paradigm (2013)
  18. Studzinski, Grischa: Implementation and applications of fundamental algorithms relying on Gröbner bases in free associative algebras. (2013)
  19. Gräbe, Hans-Gert: News from the SymbolicData project (2012) MathEduc
  20. Chen, Xiaoyu; Huang, Ying; Wang, Dongming: On the design and implementation of a geometric knowledge base (2011)

1 2 next

Further publications can be found at: