Interactive Theorem Proving for Logic and Information

Jørgen Villadsen*, Asta Halkjær From, Alexander Birch Jensen, Anders Schlichtkrull

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingBook chapterResearchpeer-review

2 Downloads (Pure)

Abstract

Automated reasoning is the study of computer programs that can build proofs of theorems in a logic. Such programs can be either automatic theorem provers or interactive theorem provers. The latter are also called proof assistants because the user constructs the proofs with the help of the system. We focus on the Isabelle proof assistant. The system ensures that the proofs are correct, in contrast to pen-and-paper proofs which must be checked manually. We present applications to logical systems and models of information, in particular selected modal logics extending classical propositional logic. Epistemic logic allows intelligent systems to reason about the knowledge of agents. Public announcements can change the knowledge of the system and its agents. In order to account for this, epistemic logic can be extended to public announcement logic. An axiomatic system consists of axioms and rules of inference for deriving statements in a logic. Sound systems can only derive valid statements and complete systems can derive all valid statements. We describe formalizations of sound and complete axiomatic systems for epistemic logic and public announcement logic, thereby strengthening the foundations of automated reasoning for logic and information.
Original languageEnglish
Title of host publicationNatural Language Processing in Artificial Intelligence
Volume999
PublisherSpringer
Publication date2022
Pages25-48
ISBN (Print)978-3-030-90137-0
DOIs
Publication statusPublished - 2022
EventNatural Language Processing in Artificial Intelligence - Online Streaming
Duration: 4 Feb 20216 Feb 2021

Conference

ConferenceNatural Language Processing in Artificial Intelligence
LocationOnline Streaming
Period04/02/202106/02/2021
SeriesStudies in Computational Intelligence
Volume999
ISSN1860-949X

Keywords

  • Epistemic logic
  • Interactive theorem proving
  • Isabelle/HOL proof assistant
  • Propositional logic
  • Public announcement logic

Fingerprint

Dive into the research topics of 'Interactive Theorem Proving for Logic and Information'. Together they form a unique fingerprint.

Cite this