Book chapter · Conference paper
On Verified Automated Reasoning in Propositional Logic
As the complexity of software systems is ever increasing, so is the need for practical tools for formal verification. Among these are automatic theorem provers, capable of solving various reasoning problems automatically, and proof assistants, capable of deriving more complex results when guided by a mathematician/programmer.
In this paper we consider using the latter to build the former. In the proof assistant Isabelle/HOL we combine functional programming and logical program verification to build a theorem prover for propositional logic. Finally, we consider how such a prover can be used to solve a reasoning task without much mental labor.
Language: | English |
---|---|
Publisher: | Springer |
Year: | 2022 |
Pages: | 390-402 |
Proceedings: | 14<sup>th</sup> Asian Conference on Intelligent Information and Database Systems<br/> |
Series: | Lecture Notes in Computer Science |
Journal subtitle: | 14th Asian Conference, Aciids 2022, Ho Chi Minh City, Vietnam, November 28–30, 2022, Proceedings, Part I |
ISBN: | 303121742X , 303121742x , 3031217438 , 9783031217425 and 9783031217432 |
ISSN: | 03029743 and 16113349 |
Types: | Book chapter and Conference paper |
DOI: | 10.1007/978-3-031-21743-2_31 |
ORCIDs: | Villadsen, Jørgen |