Experimental Prover for Tope Logic

SCAN 2023 — Workshop on Semantical and Computational Aspects of Non-Classical Logics, Moscow, Russia · June 16, 2023

An experimental decision procedure for the tope layer of Riehl–Shulman type theory with shapes. The prover underpins type checking of cube/tope expressions in rzk and is also packaged as the standalone simple-topes tool.

Download PDF

Code: fizruk/simple-topes, rzk-lang/rzk

Kudasov, N. (2023). "Experimental prover for Tope logic." SCAN 2023 abstracts, p. 37.