swMATH ID: 4621
Software Authors: Gräbe, Hans-Gert
Description: 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.
Homepage: http://www.symbolicdata.org/
Keywords: Theorem proving
Related Software: SINGULAR; SDeval; SageMath; Plural; Magma; Maple; RegularChains; GEOTHER 1.1; GAP; Letterplace; polymake; PoSSo; BERGMAN; ApCoCoA; OpenDreamKit; OEIS; DLMF; homalg; MetiTarski; REDLOG
Cited in: 29 Documents
Further Publications: http://symbolicdata.org/wiki/Publications

Citations by Year