On Verified Automated Reasoning in Propositional Logic

Simon Tobias Lund, Jørgen Villadsen

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

187 Downloads (Pure)


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 languageEnglish
Title of host publicationIntelligent Information and Database Systems.
Publication date2022
ISBN (Print)978-3-031-21742-5
Publication statusPublished - 2022
Event14th Asian Conference on Intelligent Information and Database Systems
- Rex Hotel Saigon, Ho Chi Minh City, Viet Nam
Duration: 28 Nov 202230 Nov 2022
Conference number: 14


Conference14th Asian Conference on Intelligent Information and Database Systems
LocationRex Hotel Saigon
Country/TerritoryViet Nam
CityHo Chi Minh City
SeriesLecture Notes in Computer Science


  • Logic
  • Automated Reasoning
  • Isabelle Proof Assistant


Dive into the research topics of 'On Verified Automated Reasoning in Propositional Logic'. Together they form a unique fingerprint.

Cite this