Abstract
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.
Original language | English |
---|---|
Title of host publication | Intelligent Information and Database Systems. |
Publisher | Springer |
Publication date | 2022 |
Pages | 390–402 |
ISBN (Print) | 978-3-031-21742-5 |
DOIs | |
Publication status | Published - 2022 |
Event | 14th Asian Conference on Intelligent Information and Database Systems - Rex Hotel Saigon, Ho Chi Minh City, Viet Nam Duration: 28 Nov 2022 → 30 Nov 2022 Conference number: 14 |
Conference
Conference | 14th Asian Conference on Intelligent Information and Database Systems |
---|---|
Number | 14 |
Location | Rex Hotel Saigon |
Country/Territory | Viet Nam |
City | Ho Chi Minh City |
Period | 28/11/2022 → 30/11/2022 |
Series | Lecture Notes in Computer Science |
---|---|
Volume | 13757 |
ISSN | 0302-9743 |
Keywords
- Logic
- Automated Reasoning
- Isabelle Proof Assistant