The Prop challenge has been solved

• poi

  3 136 5.8 Rust

  a pragmatic point-free theorem prover assistant (by advancedresearch)

  

Maybe you can take a look at Poi and see how this notation is used to integrate this form of encoding mathematical knowledge with theorem proving about standard algebraic problems. This is the main purpose of the Path Semantics project, to develop this syntax and make it work and understand it such that it can be applied.

• path_semantics

  12 160 8.6 Rust

  A research project in path semantics, a re-interpretation of functions for expressing mathematics

  

In topology, there is something called "point free theorem proving" style, which is almost usable in Coq or other provers like Lean, or even Cubical Type Theory. The problem is composition of normal paths. In e.g. Coq, you need a solution before you can compose. In order for normal paths to be completely painless, one use an "imaginary inverse" (paper). It is relatively easy to build your own language using an imaginary inverse to do point free theorem proving, but it also turns out that many proofs don't need types. However, adding full point free theorem proving to dependent types makes type checking undecidable.

• InfluxDB

  www.influxdata.com featured

  Power Real-Time Data Analytics at Scale. Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.

  

• prop

  6 58 8.0 Rust

  Propositional logic with types in Rust

  

Suggest a related project