Working with first-order proofs and provers
Logic in Computer Science
2019-04-10 v2
Abstract
Verifying software correctness has always been an important and complicated task. Recently, formal proofs of critical properties of algorithms and even implementations are becoming practical. Currently, the most powerful automated proof search tools use first-order logic while popular interactive proof assistants use higher-order logic. We present our work-in-progress set of tools that aim to eventually provide a usable first-order logic computer-assisted proof environment.
Cite
@article{arxiv.1904.01079,
title = {Working with first-order proofs and provers},
author = {Michael Raskin and Christoph Welzel},
journal= {arXiv preprint arXiv:1904.01079},
year = {2019}
}
Comments
4 pages. Accepted at European Lisp Symposium 2019