-
Rubi integration rules where mentioned, but here is a list of other open-source Mathematica rules: https://github.com/corywalker/expreduce/tree/master/expreduc...
-
InfluxDB
InfluxDB – Built for High-Performance Time Series Workloads. InfluxDB 3 OSS is now GA. Transform, enrich, and act on time series data directly in the database. Automate critical tasks and eliminate the need to move data externally. Download now.
-
Wide context.
But to be a bit more specific, I've been involved in the egraphs community https://github.com/philzook58/awesome-egraphs and we don't currently have a shared database of rewrite rules for benchmarking, nor do we collect the rules from different projects. Seeing the actual files is helpful.
On a slightly different front, I'm also trying to collect rules or interesting theories up in my python interactive theorem prover Knuckledragger https://github.com/philzook58/knuckledragger . Rewrite rule or equational theory looking things are easier to work with than things with deeply nested notions of quantifiers or tons of typeclass / mathematical abstraction like you find when you try to translate out of Coq, Lean, Isabelle.
There are also different approaches to declarative rewrite rules in major compilers. GCC, LLVM, and cranelift have their own declarative rewrite rule systems for describing instruction selection and peephole optimizations but also of course lots of code that programatically does this. I also want to collate these sorts of things. Working on fun clean systems while not confronting the ugly realities of the real and useful world is ultimately empty feeling. Science is about observing and systematizing. Computer science ought to include occasionally observing what people actually do or need.
-
Wide context.
But to be a bit more specific, I've been involved in the egraphs community https://github.com/philzook58/awesome-egraphs and we don't currently have a shared database of rewrite rules for benchmarking, nor do we collect the rules from different projects. Seeing the actual files is helpful.
On a slightly different front, I'm also trying to collect rules or interesting theories up in my python interactive theorem prover Knuckledragger https://github.com/philzook58/knuckledragger . Rewrite rule or equational theory looking things are easier to work with than things with deeply nested notions of quantifiers or tons of typeclass / mathematical abstraction like you find when you try to translate out of Coq, Lean, Isabelle.
There are also different approaches to declarative rewrite rules in major compilers. GCC, LLVM, and cranelift have their own declarative rewrite rule systems for describing instruction selection and peephole optimizations but also of course lots of code that programatically does this. I also want to collate these sorts of things. Working on fun clean systems while not confronting the ugly realities of the real and useful world is ultimately empty feeling. Science is about observing and systematizing. Computer science ought to include occasionally observing what people actually do or need.
