Galois: A Language for Proofs Using Galois Connections and Fork Algebras

摘要: Galois is a domain specific language supported by the Galculator interactive proof-assistant prototype. uses an equational approach based on connections with indirect equality as additional inference rule. allows for specification of different theories in point-free style using fork algebras, extension relation algebras expressive power first-order logic. The offers sub-languages to derive proof rules from connections, express tactics, and organize axioms theorems into modular definitions. In this paper, we describe how algebraic theory underlying proof-method drives design language. We provide syntax semantics important fragments show they are hierarchically combined complete