29 citations · 56 across the 17 of their papers we have counts for
5 papers · 1 filter
Learning Rules Explaining Interactive Theorem Proving Tactic Prediction
Liao Zhang, David M. Cerna, Cezary Kaliszyk
Formally verifying the correctness of mathematical proofs is more accessible than ever, however, the learning curve remains steep for many of the state-of-the-art interactive theor…
Automated Strategy Invention for Confluence of Term Rewrite Systems
Liao Zhang, Fabian Mitterwallner, Jan Jakubuv +1
Term rewriting plays a crucial role in software verification and compiler optimization. With dozens of highly parameterizable techniques developed to prove various system propertie…
Tableaux for Automated Reasoning in Dependently-Typed Higher-Order Logic (Extended Version)
Johannes Niederhauser, Chad E. Brown, Cezary Kaliszyk
Dependent type theory gives an expressive type system facilitating succinct formalizations of mathematical concepts. In practice, it is mainly used for interactive theorem proving…
Experiments with Choice in Dependently-Typed Higher-Order Logic
Daniel Ranalter, Chad E. Brown, Cezary Kaliszyk
Recently an extension to higher-order logic -- called DHOL -- was introduced, enriching the language with dependent types, and creating a powerful extensional type theory. In this…
Conway Normal Form: Bridging Approaches for Comprehensive Formalization of Surreal Numbers
Karol Pąk, Cezary Kaliszyk
The proper class of Conway's surreal numbers forms a rich totally ordered algebraically closed field with many arithmetic and algebraic properties close to those of real numbers, t…