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)

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 languageEnglish
Title of host publicationIntelligent Information and Database Systems.
PublisherSpringer
Publication date2022
Pages390–402
ISBN (Print)978-3-031-21742-5
DOIs
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

Conference

Conference14th Asian Conference on Intelligent Information and Database Systems
Number14
LocationRex Hotel Saigon
Country/TerritoryViet Nam
CityHo Chi Minh City
Period28/11/202230/11/2022
SeriesLecture Notes in Computer Science
Volume13757
ISSN0302-9743

Keywords

  • Logic
  • Automated Reasoning
  • Isabelle Proof Assistant

Fingerprint

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

Cite this