descriptionPublicationkeyboard_double_arrow_right Article , Conference object , Preprint , Other literature type 01 Jan 2019Embargo end date: 01 Jan 2019Publisher:arXivJournal:arXiv: Logic in Computer ScienceFunded by:EC | PaVeS

Authors: Raskin, Mikhail; Welzel, Christoph;

doi: 10.48550/arxiv.1904.01079 , 10.5281/zenodo.2633989 , 10.5281/zenodo.2633990

arXiv: http://arxiv.org/abs/1904.01079

Working with first-order proofs and provers

- Summary
- Subjects
- Metrics

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.

4 pages. Accepted at European Lisp Symposium 2019

Related Organizations

Technical University of Munich
Germany

Keywords

FOS: Computer and information sciences, Computer Science - Logic in Computer Science, verification, automated reasoning, computer-aided proofs, first-order logic, Logic in Computer Science (cs.LO)

Impact byBIP!

	citations This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).	0
	popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.	Average
	influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).	Average
	impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.	Average